Правило логического вывода с помощью резолюции
Правило резолюции для выражений в логике первого порядка представляет собой поднятую версию правила резолюции для пропозициональной логики, приведенного на с. 307. Два выражения, которые, согласно принятому предположению, должны быть стандартизированными таким образом, чтобы в них не было общих переменных, могут быть подвергнуты операции резолюции, если они содержат взаимно дополнительные литералы. Пропозициональные литералы являются взаимно дополнительными, если один из них представляет собой отрицание другого, а литералы в логике первого порядка являются взаимно дополнительными, если один из них унифицируется с отрицанием другого. Поэтому имеет место следующее правило:
li У ... У Ik; mi v ... У Л7П
Subst (9,i v ...v Јi-i v li+i v ... v 4 v mi v ... v mj-i v mj+i v ... v Л7П)
где Uni f у (Ii, -iflij) = 9. Например, можно применить операцию резолюции к следующим двум выражениям:
[Animal (F(x) ) v Loves (G(x) , x) ] и [—iLoves (u, v) v -Kills ( u, v) ]
путем устранения взаимно дополнительных литералов Loves (G(x) , х) и -iLoves(и, v) с помощью унификатора 9 = {u/G(x) ,v/x] для получения следующего выражения, называемого резольвентой:
[Animal (F(x) ) v -tKills (G(x) , x) ]
Только что приведенное правило называется правилом бинарной резолюции, поскольку в нем происходит удаление с помощью резолюции двух и только двух взаимно дополнительных литералов. Но правило бинарной резолюции, отдельно взятое, не позволяет получить полную процедуру логического вывода. С другой стороны, правило полной резолюции позволяет удалять в каждом выражении подмножества литералов, которые являются унифицируемыми. Альтернативный подход состоит в том, чтобы распространить операцию факторизации (удаления избыточных литералов) на логику первого порядка. В пропозициональной факторизации два литерала сводятся к одному, если они являются идентичными, а в факторизации первого порядка два литерала сводятся к одному, если они являются унифицируемыми.
Унификатор должен быть применен ко всему выражению. Сочетание бинарной резолюции и факторизации позволяет создать полную процедуру логического вывода
Примеры доказательств
При использовании резолюции доказательство того, что KB \= а (из базы знаний
следует высказывание ос) осуществляется путем доказательства невыполнимости выражения кв А -юс, т.е. путем получения пустого выражения. Алгоритмический подход, применяемый в логике первого порядка, идентичен подходу в пропозициональной логике, который показан в листинге 7.5, поэтому мы не будем здесь его повторять. Вместо этого приведем два примера доказательства. Первым из них является пример доказательства преступления, описанного в разделе 9.3. Соответствующие высказывания, преобразованные в форму CNF, выглядят следующим образом:
—(American (х) v —Weapon (у) v -i Sells {х,у, z) v -nHostile(z) v Criminal (x)
—tMissile (x) v —lOwns {Nono, x) v Sells (West, x, Nono)
-лЕпету(х,America) v Hostile(x)
—iMissile (x) v Weapon(x)
Owns (Nono, Mi)
Missile (Mi)
Ameri can (Wes t)
Enemy (Nono, Ameri с a)
В число этих высказываний должна быть включена также отрицаемая цель -Criminal (West). Процедура доказательства по методу резолюции показана на рис. 9.7. Обратите внимание на его структуру: единственный "хребет" начинается с целевого выражения, и операция резолюции применяется к выражениям из базы знаний до тех пор, пока не образуется пустое выражение. В этом состоит характерная особенность применения метода резолюции к базам знаний, представленным в виде хорновских выражений. В действительности выражения, расположенные вдоль главного хребта, точно соответствуют последовательным значениям целевых переменных в алгоритме обратного логического вывода, приведенном в листинге 9.3. Это связано с тем, что для резолюции всегда выбирается выражение, положительный литерал которого унифицируется с самым левым литералом "текущего" выражения в хребте; именно это происходит при обратном логическом выводе. Таким образом, обратный логический вывод в действительности представляет собой просто частный случай резолюции, в котором применяется конкретная стратегия управления для определения того, какая операция резолюции должна быть выполнена в следующую очередь.
В рассматриваемом здесь втором примере используется сколемизация и применяются выражения, которые не являются определенными. Это приводит к созданию немного более сложной структуры доказательства. На естественном языке эта задача формулируется, как описано ниже.
Каждого, кто любит всех животных, кто-то любит. Любого, кто убивает животных, никто не любит. Джек любит всех животных.
Кота по имени Тунец убил либо Джек, либо Любопытство. Действительно ли этого кота убило Любопытство?
Вначале представим в логике первого порядка первоначальные высказывания, некоторые фоновые знания и отрицаемую цель G:
A. Vx [Vy Animal (у) => Loves{x,y) ] => [Зу Loves{y,x)}
B. Vx [Зу Animal (у) л Kills(x,y)] => [Vz -iLoves { z, х) ]
C. Vx Animal (x) => Loves {Jack, x)
D. Kills(Jack, Tuna) v Kills(Curiosity, Tuna)
E. Ca t ( Tima)
F. Vx Cat(x) r=> Animal (x)
-iG. -iXi2Is (Curiosi ty, Tuna)
Затем применим процедуру преобразования, чтобы преобразовать каждое высказывание в форму CNF:
Al. Animal(F(x)) v Loves(G(x),x) A2 . -iLoves (x, F(x) ) v Loves (G(x) , x)
B. -nAnimal (y) v —iKills(x,y) v -iLoves (z,x)
C. —Animal(x) v Loves(Jack, x)
D. Kills(Jack,Tuna) v 1Is(Curiosity, Tuna)
E. Ca t ( Tima)
F. -iCat(x) v Animal (x)
-iG. -iKills (Curiosity, Tuna)
Доказательство с помощью метода резолюции того, что кота убило Любопытство, приведено на рис. 9.8. На естественном языке это доказательство может быть перефразировано, как показано ниже.
Предположим, что кота Тунца убило не Любопытство. Мы знаем, что это сделал либо Джек, либо Любопытство; в таком случае это должен был сделать Джек. Итак, Тунец — кот, а коты — животные, поэтому Тунец — животное. Любого, кто убивает животное, никто не любит, поэтому мы делаем вывод, что никто не любит Джека. С другой стороны, Джек любит всех животных, поэтому кто-то его любит; таким образом, возникает противоречие. Это означает, что кота убило Любопытство.
Такое доказательство действительно отвечает на вопрос "Действительно ли этого кота убило Любопытство?", но часто требуется найти ответ на более общие вопросы, такие как "Кто убил кота?" Резолюция позволяет это сделать, но для получения ответа требует немного больше работы. Данная цель может быть представлена в виде выражения 3w Kills (w, Типа), которое после его отрицания принимает в форме CNF вид —iKillsi w, Типа). Повторяя доказательство, показанное на рис. 9.8, с новой отрицаемой целью, мы получим аналогичное дерево доказательства, но с подстановкой {wl Curiosi ty] в одном из этапов. Поэтому в данном случае для поиска того, кто убил кота, достаточно проследить за связываниями, которые применяются к переменным запроса в этом доказательстве.
К сожалению, в методе резолюции могут вырабатываться неконструктивные доказательства для существующих целей. Например, в выражении -Kills{w, Типа) после применения операции резолюции удаляется взаимно дополнительный литерал, входящий в состав выражения Kills(Jack, Типа) v Kills {Curiosity, Типа), с получением выражения Kills {Jack, Типа), к которому снова применяется операция резолюции с использованием выражения —(Kills{w, Типа), что приводит к получению пустого выражения. Обратите внимание на то, что в этом доказательстве переменная w имеет два различных связывания, а правило резолюции сообщает нам, что кто-то действительно убил кота Тунца — либо Джек, либо Любопытство. Но в этом для нас нет ничего нового! Одно из решений данной проблемы состоит в том, чтобы регламентировать допустимые этапы резолюции так, чтобы переменные запроса могли быть связанными только один раз в каждом конкретном доказательстве; в таком случае можно будет предусмотреть применение перехода с возвратом по всем возможным связываниям. Еще одно решение состоит в добавлении специального литерала ответа к отрицаемой цели, которая принимает вид -\Kills(w, Типа) v Answer{w). Теперь процесс резолюции вырабатывает ответ каждый раз, когда формируется выражение, содержащее только единственный литерал ответа. Для доказательства, приведенного на рис. 9.8, таковым является выражение Answer {Curiosity). Неконструктивное доказательство привело бы к выработке выражения Answer {Curiosity) v Answer {Jack), которое не может рассматриваться как ответ и отбрасывается.