Студопедия Главная Случайная страница Обратная связь

Разделы: Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Доказательство (Для случая L.) Г, ┐S├ F Г &┐S F - тавтология. Но




Г &┐S F = ┐(Г&┐S ) F = ┐(Г&┐S) = ┐Г S = Г S.

Имеем: Г S — тавтология Г ├ S.

Пустая формула не имеет никакого значения ни в какой интерпретации, в частности, не является истинной ни в какой интерпретации и, по определению, является противоречием. В качестве фор­мулы F при доказательстве от противного по методу резолюций принято использовать пустую формулу.

Метод резолюций работает с особой стандартной формой формул, которые называются предло­жениями. Предложение — это бескванторная дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений следующим образом (здесь знак используется для обозначения способа преобразования формул).

 

1. Элиминация импликации. Преобразование: А В А В. После первого этапа формула содержит только ┐, &, , , , .

2. Протаскивание отрицаний. Преобразования: ┐ x А x А, x A x А, ┐┐A A, (A B) A & В, (A& B) A В . После второго этапа формула содержит отрицания только перед атомами.

3. Разделение связанных переменных. Преобразование:

Q1 x A(. . . Q2 x B(. . . x. . . ). . . ) Q1 x A(. . . Q2 y B(. . . y. . . ). . . ) ,

где Q1 и Q2 — любые кванторы. После третьего этапа формула не содержит случайно совпадаю­щих связанных переменных.

4. Приведение к предваренной форме. Преобразования:

Q x A B Q x (A B), Q x A&B Q x (A&В),

где Q — любой квантор. После четвертого этапа формула находится в предваренной форме.

5. Элиминация кванторов существования (сколемизация). Преобразования:

x1 Q2 x2 . . . Qn xn A(x1,x2 , . . .,xn ) Q2 x2 . . . Qn xn A(a,x2 , . . .,xn ),

x1 . . . xi-1 xi Qi+1 xi+1. . . Qn xn A(x1,. . . ,xi , . . .,xn )

x1 . . . xi-1 xi Qi+1 xi+1. . . Qn xn A(x1,. . . ,f(x1 ,. . . ,xi-1 ), . . .,xn )

где а — новая предметная константа, f — новый функтор, a Q1, Q2, . . . , Qn — любые кванторы. После пятого этапа формула содержит только кванторы всеобщности.

6. Элиминация кванторов всеобщности. Преобразование: x А(х) А(х). После шестого этапа формула не содержит кванторов.

7. Приведение к конъюнктивной нормальной форме. Преобразование:

A (B&C) (A B)&(A C), (A&B) C (A C)&(B C).

После седьмого этапа формула находится в конъюнктивной нормальной форме.

8. Элиминация конъюнкции. Преобразование: A&В А, В. После восьмого этапа формула распа­дается на множество предложений.

Не все преобразования на этапах 1-8 являются логически эквивалентными.

Теорема 4.21. Если Г — множество предложений, полученных из формулы S, то S является проти­воречием тогда и только тогда, когда множество Г невыполнимо.

Доказательство.В доказательстве нуждается шаг 5 — сколемизация. Пусть

F= x1 . . . xi-1 xi Qi+1 xi+1. . . Qn xn A(x1,. . . ,xn ) .

Положим

F': = x1 . . . xi-1 xi Qi+1 xi+1. . . Qn xn A(x1,. . . ,f(x1 ,. . . ,xi-1 ),

xi+1, . . .,xn ).

Пусть F — противоречие, a F' — не противоречие. Тогда существует интерпретация I и набор зна­чений s = (a1, . . . ,ai-1, ai+1, . . .,an) такой что (F') = И. Положим ai :=f(a1, . . . ,ai-1) , s1 := (a1, . . . ,ai-1, ai, ai+1, . . .,an). Тогда (F) = И и F — выполнимая формула.

 

Множество формул Г невыполнимо — это означает, что множество Г не имеет модели, то есть не существует интерпретации, в которой все формулы Г имели бы значение И.

 







Дата добавления: 2015-10-15; просмотров: 295. Нарушение авторских прав


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


Studopedia.info - Студопедия - 2014-2020 год . (0.004 сек.) русская версия | украинская версия