ОБРАТНЫЙ ЛОГИЧЕСКИЙ ВЫВОД
Во втором большом семействе алгоритмов логического вывода используется подход с обратным логическим выводом, представленный в разделе 7.5. Эти алгоритмы действуют в обратном направлении, от цели, проходя по цепочке от одного правила к другому, чтобы найти известные факты, которые поддерживают доказательство. Мы опишем основной алгоритм, а затем покажем, как он используется в логическом программировании, представляющем собой наиболее широко применяемую форму автоматизированного формирования рассуждений. В этом разделе будет также показано, что обратный логический вывод имеет некоторые недостатки по сравнению с прямым логическим выводом, и описаны некоторые способы преодоления этих недостатков. Наконец, будет продемонстрирована тесная связь между логическим программированием и задачами удовлетворения ограничений.
Алгоритм обратного логического вывода
Простой алгоритм обратного логического вывода, FOL-BC-Ask, приведен в листинге 9.3. Он вызывается со списком целей, содержащим единственный элемент
(первоначальный запрос) и возвращает множество всех подстановок, которые удовлетворяют этому запросу. Список целей можно рассматривать как "стек" целей, ожидающих отработки; если все они могут быть выполнены, то текущая ветвь доказательства формируется успешно. В алгоритме берется первая цель из списка и выполняется поиск в базе знаний всех выражений, положительный литерал которых (или голова) унифицируется с целью. При обработке каждого такого выражения создается новый рекурсивный вызов, в котором предпосылки (или тело) выражения добавляются к стеку целей. Напомним, что факты представляют собой выражения с головой, но без тела, поэтому, если какая-то цель унифицируется с известным фактом, то к стеку не добавляются какие-то подцели, а сама эта цель считается получившей решение. На рис. 9.4 показано дерево доказательства для получения факта Criminal (West) из высказываний, приведенных в уравнениях 9.3—9.10.
Листинг 9.3. Простой алгоритм обратного логического вывода
function FOL-BC-Ask(KB, goals, 9) returns множество подстановок inputs: KB, база знаний
goals, список конъюнктов, образующих запрос (подстановка 0 уже применена)
0, текущая подстановка, первоначально пустая подстановка {} local variables: answers, ответы - множество подстановок,
первоначально пустое
if список goals пуст then return {0} g' <- Subst(0, First(goals))
for each высказывание r in KB, где Standardize-Apart(г) = (pi л ... л pn => g) и 01 <— Unify(g, g1 ) является выполнимым new_goals <— [pi,рп| Rest (goals) ]
answers <— FOL - ВС-As k (KB, new__goals, Compose (01, 0)) U answers return answers
В этом алгоритме используется композиция подстановок. Здесь Compose (61,62) — это подстановка, результат которой идентичен результату применения каждой подстановки по очереди, следующим образом:
Subst (Compose (0i, 02) ,р) = Subst (02, Subst (0i, р) )
В данном алгоритме текущие связывания переменных, которые хранятся в подстановке 6, компонуются со связываниями, возникающими в результате унификации цели с головой выражения, что приводит к получению нового множества текущих связываний для рекурсивного вызова.
Алгоритм обратного логического вывода в том виде, в каком он был приведен в этом разделе, безусловно, представляет собой алгоритм поиска в глубину. Это означает, что его потребности в пространстве линейно зависят от размера доказательства (если на данный момент пренебречь тем, какой объем пространства требуется для накопления решений). Это также означает, что обратный логический вывод (в отличие от прямого логического вывода) страдает от проблем, обусловленных наличием повторяющихся состояний и неполноты. Эти проблемы и некоторые потенциальные решения будут рассматриваться ниже, но вначале покажем, как обратный логический вывод используется в системах логического программирования.