Метод резолюции для логики предикатов первого порядка

По существу метод (принцип) резолюции был обоснован Ж.Эрбраном в 1930г. Первым реализовал на ЭВМ идеи Эрбрана Дж.Робинсон в 1963г.

Метод резолюции - один из методов доказательства от противного. Основная идея метода заключается в попытке вывести из множества дизъюнктов S пустой дизъюнкт, для ко­торого нет интерпретаций и который тем самым гарантирует невыполнимость множества дизъюнктов. Процесс вывода пустого дизъюнкта может быть представлен процессом сведения числа вершин замкнутого дерева к единственной не­благоприятной вершине.

Мнемоническое правило вывода можно сформулировал, следующим образом: если пара исходных дизъюнктов мно­жества S содержит контрарную литералы (X и -„V), то новый дизъюнкт формируется из оставшихся частей дизъюнктов, не содержащих эти контрарные литералы. Этот вновь сформи­рованный дизъюнкт называется резольвентой исходных дизъюнктов.

Общезначимость правила резолюций выражается следую­щей леммой.

Лемма 1. Пусть S1 и S2 — дизъюнкты нормальной формы S, I — литера. Если , то дизъюнкт является логическим следствием нормальной формы S.

Если в процессе вывода новых дизъюнктов мы получаем два однолитерных дизъюнкта, образующих контрарную пару, то резольвентой этих двух дизъюнктов будет пустой дизъ­юнкт. Таким образом, выводом пустого дизъюнкта из множества дизъюнктов 5 называется конечная последова­тельность дизъюнктов С1, С₂,..., Ск такая, что любой С, яв­ляется или дизъюнкт из S или резольвентой, полученной принципом резолюции, и Ck= .

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

Пример. Пусть .

Пронумеруем исходные дизъюнкты:

Вывод представлен на рисунке 6.1с помощью дерева вы­вода.

Рис.6.1 Дерево вывода