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

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