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

Как и в исчислении высказываний является основным способом доказательств.

Резолюция – это тавтология вида:

( Х  А)  (Y   А)  (Х  Y).

К ак и в исчислении высказываний метод резолюции основывается на доказательстве от противного: вместо доказательства А  В доказываем А   В = «ложь».

Алгоритм метода резолюции следующий:

1. Составляются конъюнкции из исходных посылок и отрицания заключения.

2. Данная форма приводится к КНФ, путем использования известных законов.

3. Исключаются кванторы существования, в результате применения скулемизации.

Примечание: математик Скулем доказал, что:

• если переменная х связана с квантором существования, который сам находится в области действия квантора общности, то квантор существования уничтожается вместе с переменной, а все вхождения х, которые были связаны квантором существования, заменяются на скулемовскую константу – некоторое значение х, при которых кванторное выражение истинно:

 х А (х)  А (а).

Пример:  х (х² + х + 3 = «истина»)  а² + а + 3 = «истина»).

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

 y ( x A (x))   y ( A ( f (y))), где f (y) – скулемовская функция.

Примечание:скулемовская функция показывает каким образом мы подразумеваем зависимость х от y.

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

4. Внести кванторы общности и исключить их, используя аксиому:

 х А (х)  А (х).

5. Выписать полученные дизъюнкты в отдельные строки.

6. Применить резолюцию к полученным дизъюнктам. Если будет выведен пустой дизъюнкт, т.е. доказана ложь, то исходное утверждение верно.