Простой алгоритм прямого логического вывода
Как показано в листинге 9.2, первый рассматриваемый нами алгоритм прямого логического вывода является очень простым. Начиная с известных фактов, он активизирует все правила, предпосылки которых выполняются, и добавляет заключения этих правил к известным фактам. Этот процесс продолжается до тех пор, пока не обнаруживается ответ на запрос (при условии, что требуется только один ответ) или больше не происходит добавление новых фактов. Следует отметить, что факт не является "новым", если он представляет собой переименование известного факта. Одно высказывание называется переименованием другого, если оба эти высказывания идентичны во всем, за исключением имен переменных. Например, высказывания Likes (х, IceCream) и Likes (у, IceCream) представляют собой переименования по отношению друг к другу, поскольку они отличаются лишь выбором имени переменной, х или у; они имеют одинаковый смысл — все любят мороженое.
Листинг 9.2. Концептуально простой, но очень неэффективный алгоритм прямого логического вывода. В каждой итерации он добавляет к базе знаний кв все атомарные высказывания, которые могут быть выведены за один этап из импликационных высказываний и атомарных высказываний, которые уже находятся в базе знаний
function FOL-FC-Ask(KB, ОС) returns подстановка или значение false inputs: KB, база знаний - множество определенных выражений первого порядка а, запрос - атомарное высказывание local variables: new, новые высказывания, выводимые
в каждой итерации
repeat until множество new не пусто new <— {}
for each высказывание г in KB do
(Pi A ... л pn => q)
некоторого высказывания, которое уже находится в KB, шил рассматривается как элемент множества new then do
добавить д' к множеству new
ф <- Unify(д' , ее)
if значение ф не представляет собой fail then return ф добавить множество new к базе знаний KB return false
Для иллюстрации работы алгоритма FOL-FC-Ask воспользуемся описанной выше задачей доказательства преступления. Импликационными высказываниями являются высказывания, приведенные в уравнениях 9.3, 9.6-9.8. Требуются следующие две итерации.
• В первой итерации правило 9.3 имеет невыполненные предпосылки.
Правило 9.6 выполняется с подстановкой {х/Мг} и добавляется высказывание Sells (West, М1, Nono).
Правило 9.7 выполняется с подстановкой {х/Мх} и добавляется высказывание Weapon (Мг).
Правило 9.8 выполняется с подстановкой {x/Nono} и добавляется высказывание Hostile(Nono).
• На второй итерации правило 9.3 выполняется с подстановкой {x/West, y/Mlf z/Nono] и добавляется высказывание Criminal (West).
Сформированное дерево доказательства показано на рис. 9.2. Обратите внимание на то, что в этот момент невозможны какие-либо новые логические выводы, поскольку каждое высказывание, заключение которого можно было бы найти с помощью прямого логического вывода, уже явно содержится в базе знаний КВ. Такое состояние базы знаний называется фиксированной точкой (fixed point) в процессе логического вывода. Фиксированные точки, достигаемые при прямом логическом выводе с использованием определенных выражений первого порядка, аналогичны фиксированным точкам, возникающим при пропозициональном прямом логическом выводе (с. 315); основное различие состоит в том, что фиксированная точка первого порядка может включать атомарные высказывания с квантором всеобщности.
Свойства алгоритма FOL-FC-Ask проанализировать несложно. Во-первых, он является непротиворечивым, поскольку каждый этап логического вывода представляет собой применение обобщенного правила отделения, которое само является непротиворечивым. Во-вторых, он является полным применительно к базам знаний с определенными выражениями; это означает, что он позволяет ответить на любой запрос, ответы на который следуют из базы знаний с определенными выражениями. Для баз знаний Datalog, которые не содержат функциональных символов, доказательство полноты является довольно простым. Начнем с подсчета количества возможных фактов, которые могут быть добавлены, определяющего максимальное количество итераций. Допустим, что к — максимальная арность (количество параметров) любого предиката, р — количество предикатов и п — количество константных символов. Очевидно, что может быть не больше чем рпк различных базовых фактов, поэтому алгоритм должен достичь фиксированной точки именно после стольких итераций. В таком случае можно применить обоснование приведенного выше утверждения, весьма аналогичное доказательству полноты пропозиционального прямого логического вывода (см. с. 315). Подробные сведения о том, как осуществить переход от пропозициональной полноты к полноте первого порядка, приведены применительно к алгоритму резолюции в разделе 9.5.
При его использовании к более общим определенным выражениям с функциональными символами алгоритм FOL-FC-Ask может вырабатывать бесконечно большое количество новых фактов, поэтому необходимо соблюдать исключительную осторожность. Для того случая, в котором из базы знаний следует ответ на высказывание запроса д, необходимо прибегать к использованию теоремы Эрбрана для обеспечения того, чтобы алгоритм мог найти доказательство (случай, касающийся резолюции, описан в разделе 9.5). А если запрос не имеет ответа, то в некоторых случаях может оказаться, что не удается нормально завершить работу данного алгоритма. Например, если база знаний включает аксиомы Пеано:
NatNum{0)
Vn NatNumin) => NatNum{S{n) )
то в результате прямого логического вывода будут добавлены факты Na tNum (5(0) ), NatNum(S(S(0) ) ), NatNum(S(S(S(0) ) ) ) и т.д. Вообще говоря, избежать возникновения этой проблемы невозможно. Как и в общем случае логики первого порядка, задача определения того, следуют ли высказывания из базы знаний, сформированной с использованием определенных выражений, является полуразрешимой.