ПРЯМОЙ ЛОГИЧЕСКИЙ ВЫВОД
Алгоритм прямого логического вывода для пропозициональных определенных выражений приведен в разделе 7.5. Его идея проста: начать с атомарных высказываний в базе знаний и применять правило отделения в прямом направлении, добавляя все новые и новые атомарные высказывания до тех пор, пока не возникнет ситуация, в которой невозможно будет продолжать формулировать логические выводы. В данном разделе приведено описание того, как можно применить этот алгоритм к определенным выражениям в логике первого порядка и каким образом он может быть реализован эффективно. Определенные выражения, такие как Situation=>Response, особенно полезны для систем, в которых логический вывод осуществляется в ответ на вновь поступающую информацию. Таким образом могут быть определены многие системы, а формирование рассуждений с помощью прямого логического вывода может оказаться гораздо более эффективным по сравнению с доказательством теорем с помощью резолюции. Поэтому часто имеет смысл попытаться сформировать базу знаний с использованием только определенных выражений, чтобы избежать издержек, связанных с резолюцией.
Определенные выражения в логике первого порядка
Определенные выражения в логике первого порядка весьма напоминают определенные выражения в пропозициональной логике (с. 312): они представляют собой дизъюнкции литералов, среди которых положительным является один и только один. Определенное выражение либо является атомарным, либо представляет собой импликацию, антецедентом (предпосылкой) которой служит конъюнкция положительных литералов, а консеквентом (следствием) — единственный положительный литерал. Ниже приведены примеры определенных выражений в логике первого порядка.
Kingix) л Greedy(x) => Evil{x) King {John) Greedy (y)
В отличие от пропозициональных литералов, литералы первого порядка могут включать переменные, и в таком случае предполагается, что на эти переменные распространяется квантор всеобщности. (Как правило, при написании определенных выражений кванторы всеобщности исключаются.) Определенные выражения представляют собой подходящую нормальную форму для использования в обобщенном правиле отделения.
Не все базы знаний могут быть преобразованы в множество определенных выражений из-за того ограничения, что положительный литерал в них должен быть единственным, но для многих баз знаний такая возможность существует. Рассмотрим приведенную ниже задачу.
Закон гласит, что продажа оружия недружественным странам, осуществляемая любым американским гражданином, считается преступлением. В государстве Ноуноу, враждебном по отношению к Америке, имеются некоторые ракеты, и все ракеты этого государства были проданы ему полковником Уэстом, который является американским гражданином.
Мы должны доказать, что полковник Уэст совершил преступление. Вначале все имеющиеся факты будут представлены в виде определенных выражений в логике первого порядка, а в следующем разделе будет показано, как решить эту задачу с помощью алгоритма прямого логического вывода.
• "...продажа оружия враждебным странам, осуществляемая любым американским гражданином, является преступлением":
American(х) л Weapon(у) л Sells(х,у,z) л Hostile(z)
=> Criminal(х) (9.3)
• "В государстве Ноуноу... имеются некоторые ракеты". Высказывание Зх Owns{Nono,х) A Missile(x) преобразуется в два определенных выражения путем устранения квантора существования и введения новой константы М].:
Owns {Nono, Mi) (9.4)
Missile(M1) (9.5)
• ".. .все ракеты этого государства были проданы ему полковником Уэстом":
Missile(x) л Owns {Nono, х) => Sells ( West, х, Nono) (9.6)
Нам необходимо также знать, что ракеты — оружие:
Missile{x) => Weapon{x) (9.7)
Кроме того, мы должны знать, что государство, враждебное по отношению к Америке, рассматривается как "недружественное":
Enemy{х, America) => Hostile{x) (9.8)
• "... полковником Уэстом, который является американским гражданином": Ameriсап{West) (9.9)
• "В государстве Ноуноу, враждебном по отношению к Америке...":
Enemy {Nono,America) (9.10)
Эта база знаний не содержит функциональных символов и поэтому может служить примером класса баз знаний языка Datalog, т.е. примером множества определенных выражений в логике первого порядка без функциональных символов. Ниже будет показано, что при отсутствии функциональных символов логический вывод становится намного проще.