У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

A; B;…:- K, L,…

Хотя принятые предположения о форме записи дизъюнктов представляются произвольными, в них заложен некоторый мнемонический смысл. Если записать дизъюнкт, явно указав все знаки дизъюнкций и отрицаний и отделив литералы с отрицаниями от литералов без отрицаний, то получится примерно следующее;

(А # В #…) # (~К # -L #…)

что эквивалентно

(A # B # …) # ~(K & L & …)

Это в свою очередь эквивалентно (К & L &…) -› (А # В #…)

Если записать ',' вместо 'и', ';' вместо 'или' и ':-' вместо 'является следствием', то дизъюнкт естественным образом примет следующий вид:

A; B;…:- K, L,…

С учетом этих соглашений формула

(человек(адам) & человек(ева)) &((человек(Х) # ~мать(Х,Y)) # ~человек(Y))

записывается так:

человек(адам):-.

человек(ева):-.

человек(Х):- мать(Х,Y), человек(Y).

Это выглядит уже довольно знакомо. В действительности, это выглядит в точности как определение на Прологе того, что значит быть человеком. Однако другие формулы дают более загадочный результат. Так, для примера о выходном дне имеем:

выходной(Х); работает(крис,X):-.

выходной(Х); сердитый(крис); унылый(крис):-.

Сразу не так очевидно, чему это может соответствовать в Прологе. Этот вопрос будет подробнее рассмотрен в следующем разделе.

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

человек(f1(X)); король(Х):-.

король(Х):- почитает(f1(Х),Х).

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

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

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

Из

унылый(крист); сердитый(крис):- рабочий_день(сегодня), идет_дождь(сегодня).

и

неприятный(крис):- сердитый(крис), усталый(крис).

следует

унылый(крис); неприятный(крис):- рабочий_день(сегодня), идет_дождь(сегодня), усталый(крис).

На естественном языке это звучит так. Если сегодня рабочий день и идет дождь, то Крис – унылый или сердитый. Кроме того, если Крис сердитый и усталый, то он неприятен. Поэтому, если сегодня рабочий день, идет дождь и Крис усталый, то Крис является унылым или неприятным.