Алгоритм резолюции
Процедуры логического вывода, основанные на правиле резолюции, действуют с использованием принципа доказательства путем установления противоречия, который описывался в конце раздела 7.4. Таким образом, чтобы показать, что KB \= ос, мы покажем, что высказывание {KB л -.а) является невыполнимым. Это можно сделать, доказав, что имеет место противоречие.
Алгоритм резолюции приведен в листинге7.5. Вначале высказывание (KB л —юс) преобразуется в форму CNF. Затем к результирующим выражениям применяется правило резолюции. В каждой паре выражений, содержащих взаимно противоположные литералы, происходит удаление этих противоположных друг другу литералов для получения нового выражения, которое добавляется к множеству существующих выражений, если в этом множестве еще нет такого выражения. Указанный процесс продолжается до тех пор, пока не происходит одно из следующих двух событий:
• перестают вырабатываться какие-либо новые выражения, которые могли быть добавлены к существующим, и в этом случае из базы знаний кв не следует высказывание а;
• два противоположных друг другу выражения устраняются, в результате чего создается пустое выражение; в этом случае из базы знаний KB следует высказывание а.
Листинг 7.5. Простой алгоритм резолюции для пропозициональной логики. Функция PL-Resolve возвращает множество всех возможных выражений, полученных путем устранения противоположных друг другу литералов из двух высказываний, которые поступают на ее вход
function PL-Resolution(KB, се) returns значение true или false
inputs: KB, база знаний - высказывание в пропозициональной логике а, запрос - высказывание в пропозициональной логике
clauses <— множество выражений, полученное после преобразования высказывания KB л -ЮС в форму CNF
new <г- {} loop do
for each d, Cj in clauses do
resolvents <— PL-Resolve (Ci, 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 A Rt = (Bi,i <=> (Pi,2 v P2/i)) A -. Bi,i
и требуется доказать высказывание а, которое, скажем, имеет вид -iPi/2. После преобразования высказывания (KB л -. а) в форму CNF получим выражения, показанные в верхнем ряду на рис. 7.6. В нижнем ряду на этом рисунке показаны все выражения, полученные путем устранения противоположных друг другу литералов из всех пар выражений, приведенных в верхнем ряду. Затем после устранения литерала Pi,2, противоположного литералу -п Р1#2, будет получено пустое выражение, показанное в виде небольшого квадрата. Анализ результатов, приведенных на рис. 7.6, позволяет обнаружить, что многие этапы резолюции были бессмысленными. Например, выражение в1Л v -пБ1Л v Р1#2 эквивалентно выражению True v Plf2, которое эквивалентно True. Логический вывод, согласно которому выражение True является истинным, не очень полезен. Поэтому любое выражение, в котором присутствуют два взаимно дополнительных литерала, может быть отброшено.
Полнота резолюции
Чтобы завершить обсуждение правила резолюции в этом разделе, покажем, почему алгоритм PL-Resolution является полным. Для этого целесообразно ввести понятие резолюционного замыкания RC{S) множества выражений S, представляющего собой множество всех выражений, которые могут быть получены путем повторного применения правила резолюции к выражениям из множества S или к их производным. Резолюционным замыканием является множество выражений, которое вычисляется алгоритмом PL-Resolution в качестве окончательного значения переменной clauses. Можно легко показать, что множество RC(S) должно быть конечным, поскольку количество различных выражений, которые могут быть сформированы из символов Р1#..., Рк, присутствующих в 5, является конечным. (Следует отметить, что это утверждение не было бы истинным, если бы не применялся этап факторизации, в котором уничтожаются дополнительные копии литералов.) Поэтому алгоритм PL-Resolution всегда оканчивает свою работу.
Теорема полноты для правила резолюции в пропозициональной логике называется основной теоремой резолюции.
Если множество выражений является невыполнимым, то резолюционное замыкание этих выражений содержит пустое выражение.
Докажем эту теорему, показав, что справедливо противоположное ей утверждение: если замыкание RC(S) не содержит пустое выражение, то множество S выполнимо. В действительности для множества S можно создать модель с подходящими истинностными значениями для Р1#рк. Процедура создания такой модели описана ниже.
Для i от 1 до к:
• если в множестве RC(S) имеется выражение, содержащее литерал -iPi, такое, что все другие его литералы являются ложными при данном присваивании, выбранном для Pi,..., Pi-i, то присвоить литералу Pi значение false;
• в противном случае присвоить литералу Pi значение true.
Остается показать, что это присваивание значений литералам Р1#...,Рк представляет собой модель множества выражений S, при условии, что множество RC(S) является замкнутым согласно правилу резолюции и не содержит пустого выражения. Доказательство этого утверждения оставляем читателю в качестве упражнения.