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

Внесение квантора существования

Если формула А (х) ® В выводима и в В нет х в качестве свободной переменной, то выводима и формула $ х А (х) ® В.

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

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

(Х Ú А) Ù (Y Ú ù А) ® (Х Ú Y).

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

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

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

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

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

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

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

$ х А (х) ® А (а).

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

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

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

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

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

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

" х А (х) ® А (х).

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

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

Дата добавления: 2014-01-06