Программная реализация метода резолюций

Все сказанное выше можно записать в виде алгоритма 4.3.

Алгоритм 43. Метод резолюций

proc R (S).

С: = S.

while? g С do Select (C, pi, р2, 11, 12, s).

if pl, p2 = nil then return fail end if p := Res (pi, p2, 11, 12, s).

С := C + p end while return OK end proc.

proc Res (pi, p2, 11, 12, s).

pi := pi {s}; p2 := p2{s} pi := pi — 11; p2 := p2 — 12 return pi v p2 end proc.

proc Select (C, pi, p2, 11, 12, s).

Выбрать в множестве дизъюнктов С два дизъюнкта pi, р2, содержащие контрарные литералы 11, 12, унифицируемые наиболее общим унификатором s end proc.

При записи этих процедур используется наша стандартная практика составления алгоритмов для решения переборных задач — то, что можно фиксировать, фиксировано. В частности, процедура Res фиксирована. Нефиксированной процедурой является процедура Select. Именно в эту функцию перемещена стратегия управления, которая выбирает два дизъюнкта для резольвирования.

Всякий программист знает метод резолюций.

Студенты не знают метода резолюций.

Некоторые студенты умные люди.

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

Введем множество предикатов, описывающих высказывания, используемые в вышеприведенных утверждениях:

II — «быть программистом»,.

Р — «знать метод резолюций»,.

С — «быть студентом»,.

У — «быть умным человеком».

На языке формул исчисления предикатов первого порядка исходные утверждения (посылки) будут выглядеть следующим образом: Удг (П (дг) —> Р (я*)); /х (С (х) —" -.Р (х)); Зх (С (х)'&У (х)).

Целевая формула: Зх (У (х)&(-«П (х))).

Отрицание целевой формулы: V. r (-iY (.r)vn (.r)).

Опровергнем се с помощью метода резолюций.

1. Сводим к дизъюнктам исходные формулы:

Vx (II (x) -" Р (л" преобразуется в -n!l (x)vP (x);

Vx (C (x) -" —iP (.r)) преобразуется вiC (x)v-iP (x);

Зл (С (х)&У (л)) преобразуется в С (а) и У (а) — два единичных дизъюнкта; /л (-1У (х)уП (д)) преобразуется внУ (.г)уП (;г).

Таким образом, мы получили следующее множество дизъюнктов S: S = {-in (x)v vP (x), -iC (x)v-iP (x), С («), У (a), -.y (x)vn (x)}.

• 2. Применяем правило резолюции к 4-му и 5-му дизъюнктам и добавляем их к исходному множеству S: S = {-in (x)vP (x), -.C (.r)v-!P (x), С (а), У (а), ->У (x)vU (x)_t П (а)}.
• 3. Применяем правило резолюции к 1-му и 6-му дизъюнктам и добавляем их ко множеству дизъюнктов: S = {-.П (д:)уР (.г), -.C (.r)v-.P (.r), С (я), У (я), -1У (д:)уП (л:), Ща), Р(а)}.
• 4. Применяем правило резолюции к 2-му и 7-му дизъюнктам и добавляем их к множеству дизъюнктов: S = {-.II (x)vP (x), -iC (x)v-.P (x), С (я), У (я), ->У (x)vl (x), П (я), Р (я),^С (я)}.
• 5. Применяем правило резолюции к 8-му и 3-му дизъюнктам и добавляем их к множеству дизъюнктов: S = {-.n (x)vP (x), -iC (x)v-.P (x), С (я), У (я), ->У (д)уП (д:), П (я), Р (а), -лС (а), ?}.

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

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

• (1) —iFI (x)vP (x)
• (2) -, C (x)v-, P (x)
• (3) С (а)
• (4) У (а)
• (5) -nY (x)vIl (x)
• (6) П (а) 4−5
• (7) Р (а) 1−6
• (8) —iC (a) 2−7
• (9)? 3−8

В последующих примерах выводы методом резолюций записываются именно в такой сокращенной форме.