Вывод на основе правила резолюции

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

или эквивалентно .

В логике предикатов первого порядка она выглядит так же. Формулы в ней являются формулами этой логики. Введем по аналогии с обощенным правилом модус поненс обобщенное правило резолюции, или обобщённую резолюцию:

,

,

Унификация

Подстановка

.

Здесь обозначается литерал, такой, что при и при . Аналогичный смысл имеет символ в литерале . Подстановка означает формулу, которая получает из формулы в результате подстановки во все её атомы. Суть обобщенного правила модус поненс можно ыразить следующим образом. Если существует истинная формула

,

которая является дизъюнкцией литералов , и истинная формула

,

которая также является дизъюнкцией литералов , и в этих формулах предикатные символы литералов и одинаковы , , и для атомов и существует унификация , которая делает их (записывается как Унификация , то можно вывести истинную формулу, которая получается в результате подстановки в дизъюнцию исходных формул после удаления в них литералов и . Выведенную таким образом истинную формулу называют резольвентой. Так же как и в случае резолюции для логики высказываний, обобщенную резолюцию можно выразить с использованием импликации. Обратим внимание, что исходные формулы в обобщенной резолюции и резольвента являются дизъюнкцией литералов. Обычно такие формулы называют клаузальными формами, или клаузами. Таким образом, использование резолюции для вывода требует клаузальной формы представления знаний. Это, в свою очередь, означает, что база знаний, вывод для которой осуществляется на основе обобщенной резолюции, должна представлять собой совокупность клауз, понимаемых в целом как формула, которая является конъюнкцией клауз. Формулы такого типа обычно называют конъюнктивными нормальными формулами.

Прямой вывод на основе резолюции. Вернёмся теперь к примеру с кубиками и повторим прямой вывод той же целевой формулы, но уже используя обобщенную резолюцию. Заметим, что формулы (11.1), (11.4) уже являются клаузами. остальные формулы с помощью простейших преобразований на оснвое закона легко преобразуются в клаузы. В результате вместо (11.5)-(11.10) получим следующие формулы.