Программирование на языке Пролог

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

?- A₁, A₂,…, A_n

в точности соответствует хорновскому дизъюнкту без заголовка:- A₁, A₂,…, А_п

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

Пролог-система основывается на процедуре доказательства теорем методом резолюций для хорновских дизъюнктов. Конкретная стратегия, используемая при этом, является разновидностью линейной входной резолюции. При использовании этой стратегии, выбор дизъюнктов для резолюции на каждом шаге ограничен следующими условиями. Процедура начинается с применения правила резолюций к целевому дизъюнкту и к одной из гипотез, что дает новый дизъюнкт. Затем производится резолюция этого дизъюнкта и одной из гипотез, что дает еще один новый дизъюнкт. Затем правило резолюций применяется к последнему полученному дизъюнкту и к одной из гипотез и так далее. На каждом этапе правило резолюций применяется к последнему из вновь полученных дизъюнктов и к одной из исходных гипотез. Правило резолюций никогда не применяется, если оба дизъюнкта были выведены на предыдущих этапах или являются исходными гипотезами. С точки зрения Пролога, последний выведенный дизъюнкт можно рассматривать как конъюнкцию целевых утверждений, которые еще надо доказать (согласовать с базой данных). В начальный момент это вопрос, а в конце процесса, при благоприятных условиях,- это пустое утверждение. На каждом этапе ищется утверждение, заголовок которого сопоставим с одним из целевых утверждений. Если необходимо, происходит конкретизация переменных. Удаляется целевое утверждение, с которым произошло сопоставление, а затем к целевым утверждениям, которые необходимо согласовать, добавляется тело найденного утверждения, в котором произведена конкретизация переменных. Так, например, начав с вопроса

:- мать(джон,Х), мать(Х,Y).

и утверждения

мать(U,V):- родитель(U,V), женщина(V).

получаем

:- родитель(джон,Х), женщина(Х), мать(Х,Y).

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