"ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ" - читать интересную книгу автора (Клоксин У, Меллиш К)

2.6. Общая схема согласования целевых утверждений

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