Метод резолюции

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

Множество подстановок нужно выполнять последовательно, просматривая каждый раз только одну предметную переменную.

Принцип резолюции логики предикатов становится удобнее, если использовать упорядоченные дизъюнкты.

У порядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом старше атома в упорядоченном дизъюнкте тогда и только тогда, когда . Например, в упорядоченном дизъюнкте самым младшим считается атом , а самым старшим - . При наличии в упорядоченном дизъюнкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом.

Например, .

Пример 1. «Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один преподаватель не является невеждой»[3].

Введем предикаты: , , , .

Формула того суждения имеет вид:

Вывод заключения:

• преобразовать посылки и отрицание заключения к виду ССФ:

,

,

;

• выписать множество дизъюнктов посылок и отрицания заключения:

.

• введем обозначения для дизъюнктов:

,

,

,

,

;

• процесс вывода заключения по принципу резолюции представлен таблицей:

Родители	Унифицируемая пара предикатов	Унификатор	Полученная резольвента
и	,
и	,
и	,	‑‑‑
и	,	‑‑‑

Пример 2. Докажем пример 2 из пункта 1.2.14 методом резолюций.

• даны предикаты:

,

,

,

,

.

Формальная запись суждения имеет вид:

Вывод заключения:

• преобразовать посылки и отрицание заключения к виду ССФ:

,

,

;

• выписать множество дизъюнктов посылок и отрицания заключения:

;

• введем обозначения для дизъюнктов:

,

,

,

,

,

;

• процесс вывода заключения по принципу резолюции представлен таблицей:

Родители	Унифицируемая пара предикатов	Унификатор	Полученная резольвента
и	,
и	,
и	,
и	,
и	,	‑‑‑
и	,	‑‑‑

Существует много различных стратегий подбора пары родительских предложений для получения резольвенты. В рассмотренном выше примере нами была использована простейшая линейная по входу стратегия.