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