Главная arrow Логика arrow Алгоритм обратного логического вывода
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Алгоритм обратного логического вывода Печать

Во втором большом семействе алгоритмов логического вывода используется подход с обратным логическим выводом, представленный в разделе 7.5. Эти алгоритмы действуют в обратном направлении, от цели, проходя по цепочке от одного правила к другому, чтобы найти известные факты, которые поддерживают доказательство. Мы опишем основной алгоритм, а затем покажем, как он используется в логическом программировании, представляющем собой наиболее широко применяемую форму автоматизированного формирования рассуждений. В этом разделе будет также показано, что обратный логический вывод имеет некоторые недостатки по сравнению с прямым логическим выводом, и описаны некоторые способы преодоления этих недостатков. Наконец, будет продемонстрирована тесная связь между логическим программированием и задачами удовлетворения ограничений.

Простой алгоритм обратного логического вывода, FOL-BC-Ask, приведен в листинге 9.3. Он вызывается со списком целей, содержащим единственный элемент (первоначальный запрос) и возвращает множество всех подстановок, которые удовлетворяют этому запросу. Список целей можно рассматривать как "стек" целей, ожидающих отработки; если все они могут быть выполнены, то текущая ветвь доказательства формируется успешно. В алгоритме берется первая цель из списка и выполняется поиск в базе знаний всех выражений, положительный литерал которых (или голова) унифицируется с целью. При обработке каждого такого выражения создается новый рекурсивный вызов, в котором предпосылки (или тело) выражения добавляются к стеку целей. Напомним, что факты представляют собой выражения с головой, но без тела, поэтому, если какая-то цель унифицируется с известным фактом, то к стеку не добавляются какие-то подцели, а сама эта цель считается получившей решение. На рисунке показано дерево доказательства для получения факта Criminal (West) из высказываний, приведенных в уравнениях.

Image

Дерево доказательства, сформированное путем обратного логического вывода для доказательства того, что полковник Уэст совершил преступление. Это дерево следует читать в глубину, слева направо. Чтобы доказать факт Criminal (West);, необходимо доказать четыре конъюнкта, находящихся под ним. Некоторые из них находятся в базе знаний, а другие требуют дальнейшего обратного логического вывода. Связывания для каждой успешной унификации показаны после соответствующей подцели. Обратите внимание на, что после успешного достижения одной подцели в конъюнкции ее подстановка применяется для последующих подцелей. Таким образом, к тому времени, как алгоритм FOL-BC-Ask достигает последнего конъюнкта, первоначально имевшего форму Hostile (z), переменная z уже связана с Nono

Простой алгоритм обратного логического вывода

function FOL-ВС-Ask(KB, goals, 0) returns множество подстановок

  inputs: КБ, база знаний

    goals, список конъюнктов, образующих запрос (подстановка 0 уже применена)

    0, текущая подстановка, первоначально пустая подстановка {}

  local variables: answers, ответы - множество подстановок, первоначально пустое

  if список goals пуст then return {0}

    g' <- Subst(0, First(goals))

  for each высказывание г in KB, где Standardize-Apart(г) =

    (p1 ^... ^ pn => q) и 0' <= Unify (q', g') является выполнимым

    new_goals <— [p1,...,рn ] Rest (goals) ]

    answers <— FOL-BC-Ask(.FCB, new__goals, Compose (0', 0)) u answers

return answers

В этом алгоритме используется композиция подстановок. Здесь Compose (01, 02) — это подстановка, результат которой идентичен результату применения каждой подстановки по очереди, следующим образом:

Subst (Compose (01, 02) ,р) = Subst (02, Subst (01 ,p) )

В данном алгоритме текущие связывания переменных, которые хранятся в подстановке 0, компонуются со связываниями, возникающими в результате унификации цели с головой выражения, что приводит к получению нового множества текущих связываний для рекурсивного вызова.

Алгоритм обратного логического вывода в том виде, в каком он был приведен вэтом разделе, безусловно, представляет собой алгоритм поиска в глубину. Это означает, что его потребности в пространстве линейно зависят от размера доказательства (если на данный момент пренебречь тем, какой объем пространства требуется для накопления решений). Это также означает, что обратный логический вывод (в отличие от прямого логического вывода) страдает от проблем, обусловленных наличием повторяющихся состояний и неполноты. Эти проблемы и некоторые потенциальные решения будут рассматриваться ниже, но вначале покажем, как обратный логический вывод используется в системах логического программирования.