Проблема общезначимости формул алгебры предикатов. Лекция 7

1.

Проблема общезначимости
формул алгебры предикатов

2.

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

3.

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

4.

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

5.

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

6.

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

7.

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

8.

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

9.

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

10.

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

11.

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

12.

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

13.

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

14.

Композиция подстановок
y1 ... ym
x1 ... xn
,
s1 ... sm
t1 ... tn
является подстановкой
xi1 ... xik
,
(
t
)
...
(
t
)
ik
i1
1
где xi dom (dom ) и (ti ) xi для всех
j 1, k .
Хорошо известно, что
j
j
( ) ( ) .
j

15.

Пример.
Композицией подстановок
÷ x y z ÷
q =÷
÷ c x f ( y) ÷
÷,
÷
÷
является подстановка

16.

2. С другой стороны, композицией подстановок
x
f ( y)
y
x y z
,
z
c f (c) y
является подстановка
x
y
z x
z
,
f ( y ) z z f f (c) y
так как ( )( y ) ( y ) z y .

17.

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

18.

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

19.

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

20.

Метод резолюций в
исчислении предикатов

21.

Пусть 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.

22.

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

23.

Пример. Найдем бинарную резольвенту дизъюнктов
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 ) .
то
бинарная
получается из
вычеркиванием

24.

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

25.

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

26.

Пример.
Докажем
противоречивость
множества дизъюнктов 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) .

27.

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)

28.

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

29.

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

30.

Пример.
Методом
резолюций
доказать
общезначимость
формулы
Условие
Для формулы
равносильно
.
найдем ПНФ и ССФ.

31.

ПНФ формулы
ССФ формулы
Для доказательства невыполнимости этой формулы достаточно
доказать
противоречивость
множества
дизъюнктов
ее
конъюнктивного ядра

32.

Резолютивный вывод формулы 0 из множества дизъюнктов
:
,
где

33.

где

34.

Резолютивный
вычисления
вывод
как
средство
Метод резолюций используется для решения следующей
задачи:
Будет ли верно утверждение
, если известно, что верны
утверждения
Здесь база знаний
Предложение
- запрос к базе знаний.
Задача (неформальная): выяснить, является
предложение следствием утверждений базы знаний Г.
Задача (формальная): проверить, что
по законам формальной логики.
выводится из
ли