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

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

2.

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

3.

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

4.

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

5.

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

6.

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

7.

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

8.

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)

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

10.

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

11.

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

12.

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

13. Аксиоматический метод

14.

Было определено множество формул алгебры
высказываний FАВ
Затем было выделено подмножество этого
множества TАВ FАВ, состоящие из специальных
формул – тавтологий.
При этом в основе определения тавтологии
лежит понятие интерпретации формул, т.е.
придание
некоторого
конкретного
содержательного смысла входящих в них
переменных. Такой подход к логическим
формулам носит теоретико-множественный
характер и называется семантическим.

15.

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

16.

Построение математических теорий в виде
аксиоматических теорий соответствующих
формальных исчислений составляет суть
аксиоматического метода в математике.
Простейшей
аксиоматической
теорией
является
аксиоматическая
логика
высказываний, которая строится на основе
соответствующего формального исчисления,
называемого
исчислением
высказываний
(сокращенно, ИВ).

17. Исчисление высказываний

18.

Множество
аксиом
Ax(ИВ)
исчисления
высказываний описывается следующими тремя
схемами аксиом:
( A1 ) ,
A2 1 2 3 1 2 1 3 ,
A3 ,
где , , i i 1,2,3 – произвольные формулы
исчисления высказываний.

19.

Исчисление высказываний имеет единственное
правило вывода, которое называется правилом
заключения или правилом modus ponens (сокращенно
MP) и которое для произвольных формул
исчисления высказываний , определяется по
формуле MP , .
Символически это правило вывода записывается
следующей схемой:
,
MP :
.

20.

В основе алгоритма вывода теорем исчисления
высказываний лежит следующее понятие.
Определение. Формула называется теоремой
исчисления высказываний, если найдется такая
конечная последовательность формул 1 ,..., n , в
которой:
1) n = ;
2) каждая формула i 1 i n либо является
аксиомой, либо получается из некоторых двух
предыдущих формул j , k 1 j, k i по
правилу вывода MP.
Последовательность формул 1 ,..., n называется
выводом или доказательством формулы .

21.

Вывод формулы сокращенно обозначают
символом | и говорят, что « есть теорема».
Множество всех таких теорем обозначается
символом Th(ИВ) и называется теорией
исчисления высказываний.
Главной целью построения исчисления
высказываний является определение такой
теории Th(ИВ), которая совпадает с множеством
тавтологий TАВ.

22.

Лемма.
Справедливы следующие утверждения:
1)всякая аксиома ИВ является тавтологией;
2)результат применения правила вывода MP
к любым тавтологиям , дает
тавтологию ;
3)всякая теорема ИВ является тавтологией,
т.е. выполняется Th(ИВ) TАВ.

23.

Теорема полноты ИВ.
Всякая тавтология является теоремой ИВ,
т.е. выполняется TАВ Th(ИВ) и, следовательно,
TАВ=Th(ИВ).

24.

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