Давайте подытожим всю информацию, которую мы почерпнули в гл. 1 и 2 о том, что может произойти с целевым утверждением (целью).

1. Может иметь место попытка доказать согласованность целевого утверждения с базой данных. В процессе доказательства база данных просматривается, начиная с ее вершины. При этом возможны две ситуации:

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

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

2. Мы можем сделать попытку вновь доказать согласованность целевого утверждения с базой данных. Для этого прежде всего необходимо попытаться вновь согласовать каждую из его подцелей, при этом стрелка возвращается в некоторую исходную позицию, поднимаясь вверх по странице. Если ни одна из подцелей вновь не может быть согласована каким-либо подходящим образом, делается попытка найти альтернативное утверждение для самой исходной цели. В этом случае необходимо вернуть в исходное (неопределенное) состояние каждую переменную, конкретизированную при выборе предыдущего утверждения. Эти действия мы называем «уничтожением» результатов, полученных ранее при доказательстве согласованности целевого утверждения. Затем возобновляется просмотр базы данных, но начинается этот просмотр с места, отмеченного маркером данной цели. Как и ранее, эта новая цель, выбранная при возврате, может оказаться либо согласованной, либо несогласованной с базой данных. При этом будет иметь место либо шаг (а), либо шаг (б).

В этой главе процесс возврата будет рассмотрен более подробно. Кроме того, будет рассмотрен специальный механизм – «отсечение», который может быть использован в программах на Прологе. Отсечение позволяет указывать, какие из ранее сделанных выборов альтернатив не следует более пересматривать.