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

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

2.

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

3.

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

4.

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

5.

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

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

7.

Пусть дизъюнкты 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.

8.

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

9.

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

10.

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

11.

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

12.

Пример. Докажем невыполнимость множества
формул 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) .

13.

x
Ф7 res(Ф2 , Ф5 ) res(Ф2 ,
a
z
Ф8 res(Ф3 , Ф7 ) res( 3 ,
x
y
(Ф5 )) P1 ( z, z, u) P3 (a, u) P3 (a, z ) ;
z
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)

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

15.

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

16.

Применение метода резолюций
Метод резолюций
корректен,
полон,
алгоритмизуем.
Метод резолюций используется для решения
практических задач!

17.

Пример 1.
Методом резолюций доказать общезначимость
формулы

18.

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

19.

Пример 2. Обоснуем с помощью метода
резолюций
справедливость
следующих
рассуждений.
Пусть известно, что таможенники осматривают
багаж
каждого
пассажира,
кроме
высокопоставленных лиц. Багаж некоторых
пассажиров, везущих контрабанду, был осмотрен
людьми, способствующими провозу контрабанды.
Никто
из
высокопоставленных
лиц
не
способствовал
провозу
контрабанды.
Следовательно,
некоторые
таможенники
способствовали провозу контрабанды.

20.

Пример 3. С помощью метода резолюций
выяснить, кто любит Дашу, если известно, что:
1)
Даша любит Сашу,
2)
Саша любит колу,
3)
Паша любит колу и всех тех, кто любит
то, что любит Паша.