Предок(Y,Z).

Родитель(X,Y),

Как и раньше, переменным приписываются значения X=том, Z=пат. В этот момент переменной Yеще не приписано никакого значения. Исходная цель предок(том,пат)заменяется двумя целями родитель(том,Y)и предок(Y,пат), которые являются резольвентой пр2 и исходной цели – заключения теоремы, полученной после унификации сопоставимых предикатов.

Имея теперь перед собой две цели, алгоритм пытается достичь их в том порядке, в каком они записаны. Достичь первой из них легко, поскольку она соответствует факту из посылок. Произведя унификацию предиката родитель(том,Y)и предиката родитель(том,боб),который стоит в посылках первым, алгоритм переменной Y приписывает значение боб. Тем самым достигается первая цель, а вторая превращается в цель предок(боб,пат).

Для достижения этой цели вновь применяется правило пр1. Заметим, что это (второе) применение правила пр1 никак не связано с его первым применением. Поэтому алгоритм использует новое множество переменных правила всякий раз, как оно применяется. Чтобы указать это, мы переименуем переменные правила пр1 для нового его применения следующим образом:

предок(X ¢,Z ^¢): — родитель(X ¢,Z ^¢).

Голова этого правила совпадает с предикатным символом текущей цели предок(боб,пат), поэтому выполняется унификация {боб / X ¢,пат/ Z ^¢ ).Текущая цель заменяется целью родитель(боб,пат) –новую резольвенту.Такая цель немедленно достигается, поскольку встречается в посылках теоремы в качестве факта. Этот шаг завершает вычисления, так как получена новая резольвента – пустой дизъюнкт склейкой отрицания заключения теоремы (как того требует метод резолюций) и текущей цели.

Все шаги достижения цели предок (том, пат) представлены на рис.4.3 в виде дерева логического вывода. Вершины дерева соответствуют целям или спискам целей, которые требуется достичь.

Дуги между вершинами соответствуют применению альтернативных предложений программы, которые преобразуют цель, соответствующую одной вершине, в цель, соответствующую другой вершине. Корневая (верхняя) цель достигается тогда, когда находится путь от корня дерева (верхней вершины) к листу, помеченному меткой «да». Лист помечается меткой «да», если он представляет собой посылку-факт.

Рис.4.3. Дерево логического вывода.

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

? — предок (том, пат)

пролог-система выдает ответ

Да.