Резольвенты и резолютивный вывод в исчислении предикатов

Применения метода резолюций логики предикатов

Алгоритм метода резолюций в логике предикатов

1.31M

Category: $mathematics$ mathematics

Lektsia_9_3gr

1. Метод Эрбрана

2.

Доказательство
замкнутой
тождественной
формулы
доказательству
Ф
истинности
равносильно
противоречивости
ее
отрицания ¬Ф.
Далее рассматривается задача доказательства
противоречивости замкнутой формулы Ф.

3.

Правило 1. Противоречивость замкнутой
формулы алгебры предикатов Φ равносильна
противоречивости ее скулемовской стандартной
формы , которая является универсально
замкнутой формулой
i1 xi1 ... ik xik
с конъюнктивным ядром D1 ... Dm , где
D1 ,..., Dm – некоторые дизъюнкты литер алгебры
предикатов.
С другой стороны, универсально замкнутая
формула противоречива в том и только том
случае, если она невыполнима.

4.

Доказательство
противоречивости
(т.е.
невыполнимости)
замкнутой
формулы
сводится к доказательству невыполнимости
множества дизъюнктов S {D1 ,..., Dm } .
Эрбран показал, что при доказательстве
невыполнимости такого множества формул S
можно
ограничиться
рассмотрением
интерпретаций в одной специальной области
интерпретации,
которая
называется
эрбрановским универсумом и состоит из
функциональных выражений от констант из S.

5.

Правило
2.
Доказательство
противоречивости формул алгебры предикатов
сводится к доказательству противоречивости
конечных множеств дизъюнктов S.
Для этого строится резолютивный вывод 0
из множества дизъюнктов S.

6. Унификаторы формул

7.

Пример.
В алгебре высказываний контрарные литеры
В алгебре предикатов литеры
не
являются
переменных
литеры
контрарными,
но
при
замене
получаем контрарные

8.

Пусть S – множество формул алгебры предикатов.
Элементы области интерпретации формул из S
могут описываться не только с помощью
предметных переменных, но и с помощью так
называемых термов – специальных выражений,
которые индуктивно определяются следующим
образом:
а) все предметные переменные и предметные
символы формулы являются термами,
б) если f – n-арный функциональный символ
формулы из S и t1 ,...,t n – термы, то выражение
f (t1 ,...,t n ) является термом.

9.

Обозначим X S и FS соответственно множества всех
предметных
переменных
и
функциональных
постоянных символов, встречающихся в формулах
множества S.
Пусть TS - множество всех термов множества
формул S с функциональными символами из
множества FS . В частности, каждая переменная
x X S является термом из множества TS и, значит,
X S TS .

10.

Отображения θ множества переменных X S в
множество термов TS называются подстановками (или
заменами переменных) и обозначаются
x1 ... xn
t1 ... tn ,
где указываются ti ( xi ) для всех
,
удовлетворяющих условию
).
Если терм
содержит переменную
не должен содержать переменную
, то терм

11.

Действие
подстановки
θ
естественно
продолжается на термы из TS , атомарные
формулы, встречающихся в формулах множества
S, и дизъюнкты из S.
Например, для терма t t ( x1 ,..., xn ) значение
(t ) t ( ( x1 ),..., ( xn )) .
Аналогично, для формулы D значение (D) –
есть формула, полученная заменой всех
вхождений в D термов t на термы (t ) .

12.

Пусть W { 1 ,..., k } – множество атомарных
формул, встречающихся в формулах из
множества S. Подстановка θ называется
унификатором множества формул W, если
( 1 ) ... ( k ) .
Говорят, что множество атомарных формул W
унифицируемо, если для него существует
унификатор.

13.

Пример. Множество формул
P(b, y ), P( x, f (c))
с
бинарным
предикатным
символом
унарным функциональным символом
f
P,
и
предметными символами b,c унифицируемо,
так как подстановка
унификатором.
x
b
y
f c
является его

14. Резольвенты и резолютивный вывод в исчислении предикатов

15.

Пусть S - множество дизъюнктов, D1 , D2
дизъюнкты из S, которые не имеют общих переменных, и L1 , L2 – литеры в дизъюнктах D1 , D2 , причем
литера с отрицанием.
Если множество формул W {L1 , L2 } имеет
унификатор θ, то дизъюнкт, получаемый из дизъюнкта ( D1 ) ( D2 ) вычеркиванием контрарных литер
( L1 ) и ( L2 ) , называется бинарной резольвентой
дизъюнктов D1 и D2 и обозначается символом
res ( D1 , D2 ) . При этом литеры L1 и L2 называются
отрезаемыми литерами.
Если ( D1 ) ( L1 ) и ( D2 ) ( L2 ) , то бинарную
резольвенту дизъюнктов D1 и D2 полагаем равной 0.

16.

Если дизъюнкты D1 , D2 имеют общие
переменные, то, заменив в формулe D2 эти
общие переменные на переменные, не
встречающиеся в D1 и D2 , получим дизъюнкт
D2 , который не имеет общих переменных с
дизъюнктом D1 .
Бинарной резольвентой дизъюнктов D1 и D2
называется бинарная резольвента дизъюнктов
D1 и D2 .

17.

Пример. Найдем бинарную резольвенту дизъюнктов
D1 P1 ( x ) P2 ( x ) и D2 P1 (c) P3 ( x )
Так как D1 , D2 имеют общую переменную x, то
заменим в формуле D2 переменную х на новую
переменную у: D2 = P1 ( c ) P3 ( y ) .
Выбираем в D1 и D2 литеры L1 P1 ( x ) и L2 P1 (c) ,
соответственно. Так как L2 L2 P1 (c) и формулы
L1 , L2
имеют
резольвента
x
,
c
унификатор
формул
D1
и
D2
( D1 ) ( D2 ) P1 (c) P2 (c) P1 (c) P3 ( y )
литер P1 ( c ) и P1 ( c ) .
то
бинарная
получается из
вычеркиванием

18.

Резолютивный вывод формулы Ф из
множества дизъюнктов S есть такая
конечная
последовательность
дизъюнктов Ф1 ,...,Фк , что:
1) Фk Ф ,
Фi
2)
каждый
дизъюнкт
или
принадлежит
множеству
S,
или
является
резольвентой
некоторых
дизъюнктов, предшествующих Фi .

19.

Лемма. Резолютивный вывод из множества
дизъюнктов
сохраняет
S
выполнимость
формул.
Правило
3.
(Основная
теорема
дизъюнктов
S
метода
резолюций).
Множество
тогда и только
противоречиво
тогда, когда существует
резолютивный вывод нуля 0 из S.

20.

Пример.
Докажем
противоречивость
множества дизъюнктов W Ф1 ,...,Ф6 , где
Ф1 P1 ( a, f (b), f ( c )) ,
Ф2 P2 ( a ) ,
Ф3 P1 ( x, x, f ( x )) ,
Ф4 P1 ( x, y , z ) P3 ( x, z ) ,
Ф5 P2 ( x ) P1 ( y , z, u ) P3 ( x, u ) P3 ( x, y ) P3 ( x, z ) ,
Ф6 P3 (a, c) .

21.

x
Ф7 res(Ф2 , Ф5 ) res(Ф2 ,
a
y
(Ф5 )) P1 ( z, z, u) P3 (a, u) P3 (a, z ) ;
z
z
Ф8 res(Ф3 , Ф7 ) res( 3 ,
x
u
( 7 )) P3 (a, f ( x )) P3 (a, x ) ;
f ( x )
x
Ф9 res(Ф6 , Ф8 ) res( 6 , ( 8 )) P3 (a, f (c));
c
x
Ф10 res(Ф4 , Ф9 ) res(
a
z
( 4 ), 9 ) P1 (a, y, f (c));
f (c)
y
Ф11 res(Ф1 , Ф10 ) res( 1 ,
( 10 )) 0.
f ( b)

22. Применения метода резолюций логики предикатов

23.

Следующие задачи равносильны:
а) проверка
формул;
тождественной
истинности
б) проверка логического следования формул;
в) проверка тождественной ложности формул;
д) проверка
дизъюнктов.
противоречивости
множества

24. Алгоритм метода резолюций в логике предикатов

25.

Шаг
1.
Доказательство
тождественной
истинности замкнутой формулы Ф сводится к
доказательству
отрицания ¬Ф= .
противоречивости
ее

26.

Шаг
2.
Доказательство
противоречивости
замкнутой формулы алгебры предикатов
сводится к доказательству противоречивости ее
скулемовской стандартной формы
, которая
является универсально замкнутой формулой
с конъюнктивным ядром
,
где
– некоторые дизъюнкты литер
алгебры предикатов.