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

•    перестают вырабатываться какие-либо новые выражения, которые могли быть добавлены к существующим, и в этом случае из базы знаний кв не следует высказывание а;

•   два противоположных друг другу выражения устраняются, в результате чего создается пустое выражение; в этом случае из базы знаний KB следует высказывание а.

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

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

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

и требуется доказать высказывание а, которое, скажем, имеет видПосле преобразования высказыванияв форму CNF получим выражения, показанные в верхнем ряду на рис. 7.6. В нижнем ряду на этом рисунке показаны все выражения, полученные путем устранения противоположных друг другу литералов из всех пар выражений, приведенных в верхнем ряду. Затем после устранения литерала противоположного литералубудет получено пустое выражение, показанное в виде небольшого квадрата. Анализ результатов, приведенных на рис. 7.6, позволяет обнаружить, что многие этапы резолюции были бессмысленными. Например, выражениеэквивалентно выражению которое эквивалентно True. Логический вывод, согласно которому выражение True является истинным, не очень полезен. Поэтому любое выражение, в котором присутствуют два взаимно дополнительных литерала, может быть отброшено.