и
родители(джон,анна,фред). Однако столь подробная диаграмма не поместилась бы на одной странице.
Данный пример иллюстрирует общую схему рассмотрения целевых утверждений, объединенных в конъюнкцию, для случая, когда все цели согласуются с базой данных. Стрелка перемещается вниз по странице, по очереди проходя через прямоугольники. Когда стрелка входит в какой-либо прямоугольник, выбирается некоторое утверждение и отмечается его позиция. Если данное утверждение сопоставимо с целью и является фактом, стрелка может покинуть прямоугольник (такая ситуация имела место для целевых утверждений мать и отец). Если же утверждение сопоставимо с целью, но является правилом, создаются прямоугольники для подцелей, и стрелка должна пройти через них, прежде чем она сможет покинуть первоначальный прямоугольник.
2.6.2. Рассмотрение целевых утверждений при использовании механизма возврата
Когда целевое утверждение недоказуемо (проверены все возможные утверждения или пользователь нажал клавишу ';'), «цепочка доказательств» проходит назад тот путь, по которому она пришла в данную точку. Она возвращается в покинутые перед этим прямоугольники для того, чтобы попытаться передоказать (вновь согласовать) соответствующие целевые утверждения. Когда стрелка возвращается в то место, где было выбрано какое-то утверждение (это событие изображается числом в скобках), Пролог пытается найти альтернативное утверждение, соответствующее данной цели. Сначала делаются неопределенными все переменные, которые были конкретизированы в ходе доказательства данного целевого утверждения. Затем возобновляется поиск в базе данных, начиная с того места, где был оставлен маркер. Если будет найдено другое утверждение, соответствующее целевому, Пролог помечает это место, и дальше события развиваются, как было описано выше в разд. 2.6.1. Отметим, что рассмотрение любых целевых утверждений, находящихся «ниже» данного (даже если они были пройдены в ходе рассмотрения предыдущей альтернативы), всегда начинается с самого начала. Пролог пытается доказать их без учета положения маркера (т. е. это не передоказательство). Если не удается найти другое подходящее утверждение, данное целевое утверждение считается недоказуемым и стрелка продолжает возвращаться назад до следующего маркера. В нашем примере, если целевое утверждение родители(джон,анна,фред) недоказуемо, стрелка уйдет назад из прямоугольника родители(джон,анна,фред)
