Программирование на языке пролог
Шрифт:
A; B;…:- K, L,…
Хотя принятые предположения о форме записи дизъюнктов представляются произвольными, в них заложен некоторый мнемонический смысл. Если записать дизъюнкт, явно указав все знаки дизъюнкций и отрицаний и отделив литералы с отрицаниями от литералов без отрицаний, то получится примерно следующее;
(А # В #…) # (~К # -L #…)
что эквивалентно
(A # B # …) # ~(K & L & …)
Это в свою очередь эквивалентно (К & L &…) -› (А # В #…)
Если записать ',' вместо 'и', ';' вместо 'или' и ':-' вместо 'является следствием', то дизъюнкт естественным образом примет следующий вид:
A; B;…:- K, L,…
С учетом этих соглашений формула
(человек(адам) &
записывается так:
человек(адам):-.
человек(ева):-.
человек(Х):- мать(Х,Y), человек(Y).
Это выглядит уже довольно знакомо. В действительности, это выглядит в точности как определение на Прологе того, что значит быть человеком. Однако другие формулы дают более загадочный результат. Так, для примера о выходном дне имеем:
выходной(Х); работает(крис,X):-.
выходной(Х); сердитый(крис); унылый(крис):-.
Сразу не так очевидно, чему это может соответствовать в Прологе. Этот вопрос будет подробнее рассмотрен в следующем разделе.
В приложении В представлена программа на Прологе, печатающая дизъюнкты в рассмотренном здесь виде. Так, дизъюнкты, приведенные в конце предыдущего раздела, в соответствии с принятыми соглашениями печатаются программой в следующем виде:
человек(f1(X)); король(Х):-.
король(Х):- почитает(f1(Х),Х).
10.4. Принцип резолюций и доказательство теорем
Теперь, когда мы имеем способ, позволяющий представлять формулы исчисления предикатов в такой аккуратной и привлекательной форме, рассмотрим, что можно делать с ними далее. Очевидно, можно исследовать вопрос о том, следует личто-либо интересное из некоторой заданной совокупности высказываний. То есть интересно исследовать, к каким следствиямони приводят. Высказывания, которые исходно считаются истинными, называются аксиомамиили гипотезами,а высказывания, которые следуют из них, называются теоремами.Введенные понятия согласуются с терминологией, используемой при описании такого подхода к математике, когда работа математика представляется как процесс получения все новых и новых интересных теорем из таких хорошо аксиоматизированных областей, какими являются теория множеств и теория чисел. В этом разделе будут кратко рассмотрены вопросы получения интересных следствий для заданного множества высказываний, то есть вопросы доказательства теорем.
В 60-х годах в этой области наблюдалась большая активность, связанная с возможностью использования вычислительных машин для автоматического доказательства теорем. Именно эта область научной деятельности, по-прежнему остающаяся источником новых идей и методов, дала жизнь идеям, легшим в основу Пролога. Одним из фундаментальных достижений того времени явилось открытие Дж. А. Робинсоном принципа резолюцийи его применение к автоматическому доказательству теорем. Резолюция – это правило вывода,говорящее о том, как одно высказывание может быть получено из других. Используя принцип резолюций, можно полностью автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь решать, к каким из высказываний следует применять правило вывода, а правильные следствия из них будут строиться автоматически.
Правило резолюций разрабатывалось применительно к формулам, представленным в стандартной форме. Если заданы два дизъюнкта, связанных между собой
Из
унылый(крист); сердитый(крис):- рабочий_день(сегодня), идет_дождь(сегодня).
и
неприятный(крис):- сердитый(крис), усталый(крис).
следует
унылый(крис); неприятный(крис):- рабочий_день(сегодня), идет_дождь(сегодня), усталый(крис).
На естественном языке это звучит так. Если сегодня рабочий день и идет дождь, то Крис – унылый или сердитый. Кроме того, если Крис сердитый и усталый, то он неприятен. Поэтому, если сегодня рабочий день, идет дождь и Крис усталый, то Крис является унылым или неприятным.
В действительности, мы сильно упростили ситуацию, опустив два момента. Прежде всего, ситуация усложняется, когда дизъюнкты содержат переменные. В такой ситуации две атомарные формулы не обязательно должны быть идентичными – они должны быть лишь «сопоставимы». Кроме того, дизъюнкт, являющийся следствием двух других дизъюнктов, получается в результате их соединения (с удалением повторяющейся формулы) с помощью некоторой дополнительной операции. Эта операция включает в себя«конкретизацию» переменных до такой степени, чтобы две сопоставляемые формулы стали идентичными. Используя терминологию Пролога, можно сказать, что, если имелось два дизъюнкта, представленных в виде структур, и было выполнено сопоставление соответствующих подструктур, то результат соединения этих структур и был бы представлением нового дизъюнкта. Второе упрощение состоит в том, что в общем случае, правило резолюций допускает сопоставление нескольких литералов в правой части одного дизъюнкта с несколькимилитералами в левой части другого дизъюнкта. Здесь будут рассматриваться лишь примеры, когда из каждого дизъюнкта выбирается один литерал.
Рассмотрим один пример применения правила резолюций при наличии переменных:
человек(f1(Х)); король(Х):-. (1)
король(Y):- почитает(f1(Y),Y). (2)
почитает(Z,артур):- человек(Y). (3)
Два первых дизъюнкта представляют стандартную форму формулы, которую можно выразить так: «если каждый человек почитает кого-то, то этот кто-то – король». Переменные переименованы для удобства объяснения. Третий дизъюнкт выражает высказывание о том, что каждый человек почитает Артура. Применяя правило резолюций к (2) и (3) (сопоставляя два соответствующих литерала), получаем:
король(артур):- человек(f1(артур)). (4)
( Yв (2) сопоставлен с артурв (3), a Zв (3) сопоставлен с fl(Y)в (2)). Теперь можно применить правило резолюций к (1) и (4), что дает:
король(артур); король(артур):-.
Это эквивалентно факту, гласящему, что Артур является королем.
В формальном определении метода резолюций процедура «сопоставления», на которую мы неформально ссылались, называется унификацией.Интуитивно, множество атомарных формул унифицируемо,если эти формулы могут быть сопоставлены друг с другом как структуры языка Пролог. В действительности, как это будет показано в одном из следующих разделов, процедура сопоставления, используемая в большинстве реализаций языка Пролог, не совпадает в точности с унификацией.