Сколемовская нормальная форма





Определение. Формула G имеет сколемовскую нормальную форму (сокращенно: СНФ), если G=("x)…("xn)H,

где формула Н не содержит кванторов и имеет конъюнктивную нормальную форму.

Например, формула ("x)[P(x)Ú(P(y)&Q(x,y)] имеет сколемовскую нормальную форму, а формулы ("x)($y)Q(x,y), ("x)[P(x)&(P(y)ÚQ(x,y)] не имеют.В отличие от предыдущего случая предваренной нормальной формы мы здесь вначале рассмотрим алгоритм приведения к СНФ, а затем сформулируем теорему.

Алгоритм приведения к сколемовской нормальной форме

Шаг 1 – Шаг 3 – те же, что и в предыдущем алгоритме.

Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме (алгоритм описан в §5 темы 1).Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага имеем формулу F=($x)("y)($z)("u)($v)H(x,y,z,u,v),

где Н – не содержит кванторов. Предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле Н заменим х на с, z – на f(y), v заменим на g(y,u). Все кванторы существования вычеркнем. Получим формулу

G=("y)("u)H(c,y,f(y),u,g(g,u)).

Это и есть результат выполнения шага 5. Приведем пример приведения к СНФ. Пусть

F=($x)("y)[P(x,y)®($z)(Q(x,z)&R(y))].

Применяя законы 20 и 23, получаем формулу

 

F1=($x)("y) )($z)[ØP(x,y)Ú(Q(x,z)&R(y))].

 

Она имеет предваренную нормальную форму. Используя закон 12 приводим бескванторную часть к КНФ:

 

F2=($x)("y) )($z)[ØP(x,y)Ú(Q(x,z)&(ØP(x,y)Ú(R(y))].

 

Сделаем подстановку x=a, z=f(y), получим искомую формулу

 

G=("y)[(ØP(a,y)ÚQ(a, f(y)))&(ØP(a,y) )ÚR(y))].


Метод резолюции

Доказательство теорем сводится к доказательству того, что некоторая формула (гипотеза теоремы) является логическим следствием множества формул (допущений). Т.е. сама теорема может быть сформулирована следующим образом: "если истинны, то истинна и ". Такой метод доказательства теорем называется методом резолюций.

Для доказательства того, что формула G является логическим следствием множества формул , метод резолюций применяется следующим образом. Сначала составляется множество формул . Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул . Если из S нельзя вывести #, то G не является логическим следствием формул .
Рассмотрим пример доказательства методом резолюций. Пусть у нас есть следующие утверждения:

 

Машина Тьюринга

1)Маши́на Тью́ринга (МТ) — абстрактный исполнитель (абстрактная вычислительная машина). Была предложена Аланом Тьюрингом в 1936 году для формализации понятия алгоритма.

Машина Тьюринга является расширением конечного автомата и, согласно тезису Чёрча — Тьюринга, способна имитировать все другие исполнители (с помощью задания правил перехода), каким-либо образом реализующие процесс пошагового вычисления, в котором каждый шаг вычисления достаточно элементарен. В состав машины Тьюринга входит бесконечная в обе стороны лента (возможны машины Тьюринга, которые имеют несколько бесконечных лент), разделённая на ячейки, и управляющее устройство, способное находиться в одном из множества состояний. Число возможных состояний управляющего устройства конечно и точно задано.

2) Операции над машинами Тьюринга

Со­че­та­ния ал­го­рит­мов [Ма­те­ма­ти­че­с­кая,1977,т.1] - это на­зва­ние, уста­но­вив­ше­еся за ря­дом кон­крет­ных спо­со­бов кон­стру­иро­ва­ния но­вых ал­го­рит­мов из не­ско­ль­ких за­дан­ных.

Те­оре­мы о со­че­та­ни­ях ал­го­рит­мов со­став­ля­ют важ­ный раз­дел об­щей те­ории ал­го­рит­мов. Бу­ду­чи до­ка­зан­ны­ми однаж­ды, они по­зво­ля­ют в да­ль­ней­шем убеж­да­ть­ся в осу­ще­ст­ви­мо­сти слож­ных и гро­мо­зд­ких ал­го­рит­мов без фак­ти­че­с­ко­го вы­пи­сы­ва­ния опре­де­ля­ющих их схем.

Со­че­та­ния ал­го­рит­мов для ма­ши­ны Тью­рин­га опи­сы­ва­ют­ся опе­ра­ци­ями над ма­ши­на­ми Тью­рин­га.

1. Опе­ра­ция ком­по­зи­ции.

Пусть M1 и M2 - ма­ши­ны Тью­рин­га, име­ющие оди­на­ко­вый вне­шний ал­фа­вит A«{a0,a1,...,ap}. Обоз­на­чим мно­же­ст­ва их со­сто­яний со­от­ве­т­ст­вен­но Q1«{q0,q1,...,qn} и Q2«{q0',q1',...,qm'}.

 

 

4)Частично рекурсивная функция определяется аналогично примитивно рекурсивной, только к двум операторам суперпозиции и примитивной рекурсии добавляется ещё третий оператор — минимизации аргумента.

  • Оператор минимизации аргумента. Пусть f — функция от n натуральных переменных. Тогда результатом применения оператора минимума аргумента к функции f называется функция h от n − 1 переменной, задаваемая следующим определением:

, при условии

То есть функция h возвращает минимальное значение последнего аргумента функции f, при котором её значение равно 0.

В терминах императивного программирования — примитивно рекурсивные функции соответствуют программным блокам, в которых используется только арифметические операции, а также условный оператор и оператор арифметического цикла (оператор цикла, в котором число итераций известно на момент начала цикла). Если же программист начинает использовать оператор цикла while, в котором число итераций заранее неизвестно и, в принципе, может быть бесконечным, то он переходит в класс частично рекурсивных функций.

Частично рекурсивные функции для некоторых значений аргумента могут быть не определены, так как оператор минимизации аргумента не всегда корректно определён, так как функция f может быть не равной нулю ни при каких значениях аргументов. С точки зрения императивного программирования, результатом частично рекурсивной функции может быть не только число, но и исключение или уход в бесконечный цикл, соответствующие неопределённому значению.

 

 





Читайте также:
Романтизм как литературное направление: В России романтизм, как литературное направление, впервые появился ...
Социальное обеспечение и социальная защита в РФ: Понятие социального обеспечения тесно увязывается с понятием ...
Опасности нашей повседневной жизни: Опасность — возможность возникновения обстоятельств, при которых...
Своеобразие родной литературы: Толстой Л.Н. «Два товарища». Приёмы создания характеров и ситуаций...

Рекомендуемые страницы:



Вам нужно быстро и легко написать вашу работу? Тогда вам сюда...

Поиск по сайту

©2015-2021 poisk-ru.ru
Все права принадлежать их авторам. Данный сайт не претендует на авторства, а предоставляет бесплатное использование.
Дата создания страницы: 2016-02-16 Нарушение авторских прав и Нарушение персональных данных


Поиск по сайту:

Мы поможем в написании ваших работ! Мы поможем в написании ваших работ! Мы поможем в написании ваших работ!
Обратная связь
0.031 с.