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