Алгоритм резолюции

Процедуры логического вывода, основанные на правиле резолюции, действуют с использованием принципа доказательства путем установления противоречия, который описывался в конце раздела. Таким образом, чтобы показать, что KB ≠ α, мы покажем, что высказывание (KB ^ ¬α) является невыполнимым. Это можно сделать, доказав, что имеет место противоречие.

Алгоритм резолюции приведен в листинге. Вначале высказывание (KB ^ ¬α) преобразуется в форму CNF.

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

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

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

 

function PL-Resolution(KB, се) returns значение true или false

  inputs: KB, база знаний - высказывание в пропозициональной логике

  а, запрос - высказывание в пропозициональной логике

  clauses <— множество выражений, полученное после преобразования

  высказывания KB л —i(X в форму CNF

  new <— {}

  loop do

  for each d, Cj in clauses do

  resolvents <— PL-Resolve (Cl, Cj)

  if множество resolvents содержит пустое выражение

  then return true

  new <— new u resolvents

  if new с clauses then return false

  clauses <— clauses u new

 

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

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

KB = R2 ^ R4 = (B1,1 <=> (P1,2 v P2,1)) ^ ¬B1,1

и требуется доказать высказывание α, которое, скажем, имеет вид ¬P1,2. После преобразования высказывания (KB ^ ¬α) в форму CNF получим выражения. В нижнем ряду на этом рисунке показаны все выражения, полученные путем устранения противоположных друг другу литералов из всех пар выражений, приведенных в верхнем ряду. Затем после устранения литерала P1,2, противоположного литералу ¬P1,2, будет получено пустое выражение, показанное в виде небольшого квадрата.

Анализ результатов, позволяет обнаружить, что многие этапы резолюции были бессмысленными. Например, выражение B1,1 v ¬B1,1 v P1,2 эквивалентно выражению True v P1,2, которое эквивалентно True. Логический вывод, согласно которому выражение True является истинным, не очень полезен. Поэтому любое выражение, в котором присутствуют два взаимно дополнительных литерала, может быть отброшено.