В общем случае, поиск вывода на предложенной конструкции двоичного дерева выглядит так. В процессе означивания термов, происходит движение вниз по дереву поиска. При невозможности дальнейшего означивания, выдается сигнал неудачи и происходит "отход" назад. В тактике "наивного бектрекинга" причины неудачи не анализируются и отход происходит на предыдущий шаг, где выбирается следующая альтернатива. Однако, если сделать анализ возможных "причин неудачи", т.е. анализ ранее сделанных подстановок, из-за которых невозможна подстановка на этом шаге, то возможен отход к той точке дерева, которая является возможной "причиной" неудачного означивания, блокировка ранее выбранного решения и просмотр следующей альтернативы. Такая организация процесса "отхода" позволяет существенно повысить эффективность системы поиска, так как при выборе альтернатив из рассмотрения исключаются целые куски дерева подстановок, лежащие ниже той его вершины, которая является возможной "причиной" неудачи.

Представим в виде такого двоичного дерева процесс решения методом "поиска в глубину" предложенного примера. При этом неудачу при означивании будем помечать F (false), после чего происходит "отход" вверх по дереву. Сделанная ранее "неудачная" подстановка, которая вероятно ответственна за невозможность дальнейшего означивания запрещается (появляется соответствующее неравенство, например yjb при первом "отходе"), т.е. на дереве в соответствующей точке выбирается правое ребро, и поиск подстановок продолжается. Успешное завершение поиска обозначим Tr (true).



P(x) ¬

/ \ 

xja/ \ x/a 

/ Q(y) \ ¬ 

/ / \  

P(x) / yjb / \ y/b  

\ x/b / \  

Q(y) \ / Q(y) \ R(z,y)  

/ \ \  

yjb / \ y/c \  

/ \ F1 

Q(y) / \ R(z,y) 

\ y/c \ 

\ \ z/b 

R(z,y) \ \ 

\ z/b \ S(x,a) 

\ \ 

S(x,a) \ F2

\

Tr



В случае intelligent backtracking при неудаче производится анализ возможной причины неудачи и отход осуществлялся на тот узел дерева, в котором была сделана неверная подстановка. В нашем примере таких отходов было два. В первом случае, intelligent backtracking не отличается от стандартного, так как отход производится на ближайшую точку ветвления. Но во-втором случае, анализ неудачи показывает, что необходимо вернуться в первый узел дерева поиска (означивание переменной x) и запретить подстановку x/a. При этом, полезную информацию о запрете подстановки y/b, полученную при первом "бектрекинге" также можно сохранить и использовать для дальнейшего поиска вывода.

В третьем параграфе ("Формальная система интеллектуального бекттрекинга") ставится задача построения исчисления поиска вывода "интеллектуального бектрекинга" на основе языка исчисления предикатов первого порядка, который обогащается дополнительными отношениями на термах — отношениями равенства и неравенства. Это позволяет задать систему ограничений (отношение неравенства) и систему предпочтений (система равенств) на возможные подстановки при поиске вывода.

В первой части параграфа задается логическая система L в этом обогащенном языке исчисления предикатов. Наиболее существенным является определение правильно построенной формулы L и связанные с ним понятия непротиворечивой тройки и совместимости троек. п. п. ф. L представляет собой выражение вида (Г С К) [О], где:

С — является п. п. ф. исчисления предикатов,

Г (К) — система неравенств (равенств) (Г, К — возможно пустые),

О — подстановка, применяемая к цепочке (Г С К).

Для того чтобы выражение (Г С К) [О] являлось п. п. ф. системы L необходимо выполнение следующих условий:

1. Г должно быть непротиворечиво, т.е. не должно содержать противоречивых неравенств типа х j х.

2. Г и К должны быть совместимы, т.е. если х j a О Г, то х j a О К и наоборот.

3. О должна быть совместима с Г, т.е. результат конкретизации Г посредством О не должен содержать противоречивых неравенств типа х j a (конкретизация Г посредством О непротиворечива).

4. О совместима с Г и К, т.е. при конкретизации Г и К посредством О должны быть совместимы.

Тройка ГКО называется непротиворечивой, если и только если Г, К, О удовлетворяют выше сформулированным ограничениям, т.е. если ( Г С К ) [ О ] является п. п. ф. L.

Тройка ГiКiОi совместима с непротиворечивой тройкой ГjКjОj, если и только если тройка (Гi Гj) (Кi Кj) (Оi Оj) непротиворечива, где цепочки Гi Гj (Кi Кj, Оi Оj) — результат композиции неравенств Гi и Гj (равенств Кi Кj , подстановок Оi Оj).