Программирование на языке пролог (ЛП)

До сих пор ничего не было сказано о том, что значат переменные, входящие в состав высказывания. В действительности, использование переменных имеет смысл лишь в случае, когда они вводятся с помощью кванторов.Кванторы позволяют делать высказывания о множествах объектов и формулировать утверждения, истинные для этих множеств. В исчислении предикатов имеются два квантора. Если ν обозначает переменную, а ρ – это произвольное высказывание, то коротко значение кванторов можно выразить так:

Исчисление предикатов	Обозначение в книге	Значение
∀ν. ρ	all(ν, ρ)	«ρ истинно для всех значений переменной ν»
∃ν.ρ	exists(ν, ρ)	«существует такое значение переменной ρ, для которого ν истинно»

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

all(X, мужчина(Х) -› человек(Х))

которая значит, что какое бы значение Xмы не выбрали, если Xявляется мужчиной, то тогда X– человек. Эту формулу можно прочитать так: для любого X, если X является мужчиной, то X является человеком.Или в более простой формулировке: каждый мужчина является человеком.Аналогично

exists(Z, отец(джон,2)& женщина(Z)))

значит, что существует объект, обозначаемый Zтакой, что Джон является отцом Zи Z– женщина. Эту формулу можно прочитать так: существует Z такой, что Джон является отцом Zи Z– женщина.Или в более естественной формулировке: Джон имеет дочь.Ниже приведены две более сложные формулы исчисления предикатов:

all(X, животное(Х) -› exists(Y,мать(X,Y)))

all(X, формула_исчисления_предикатов(Х) ‹-› атомарная_формула(Х) # составная_формула(Х))

10.2. Приведение формул к стандартной форме

Как было показано в предыдущем разделе, формулы исчисления предикатов, записанные с использованием связок -› (импликация) и ‹-› (эквивалентность), могут быть переписаны лишь с использованием связок& (конъюнкция), # (дизъюнкция) и ~ (отрицание). В действительности, существует множество разных форм записи формул, и мы ни в коей мере не принесли бы в жертву выразительность формул, если бы должны были полностью отказаться от использования, например, #, -›, ‹-›и exists(X, P). Как следствие этой избыточности, существуют много различных способов записи одного и того же высказывания. При необходимости выполнять формальные преобразования формул исчисления предикатов это оказывается очень неудобным. Было бы значительно лучше, если бы все, что мы хотим сказать, можно было выразить единственным способом. Поэтому здесь будет рассмотрен способ преобразования формул исчисления предикатов к специальному виду – стандартной форме,- обладающему тем свойством, что число различных способов записи одного и того же утверждения меньше по сравнению с использованием других форм. В действительности будет показано, что высказывание исчисления предикатов, представленное в стандартной форме, очень похоже на некоторое множество утверждений языка Пролог. Так что исследование стандартной формы имеет существенное значение для понимания связи между Прологом и математической логикой. В приложении В будет коротко описана программа на Прологе, автоматически транслирующая формулы исчисления предикатов в стандартную форму.

Процесс приведения формулы исчисления предикатов к стандартной форме состоит из шести основных этапов.

Этап 1 - исключение импликаций и зквивалентностей

Процедура начинается с замены всех вхождений -› и ‹- ›в соответствии с их определениями, данными в разд. 10.1. Так, например, формула

аll(Х,мужчина(Х) -› человек(Х))

будет преобразована в формулу

аll(Х,~мужчина(Х) # человек(Х))

Этап 2 - перенос отрицания внутрь формулы

На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. Если такой случай имеет место, то формула переписывается по соответствующим правилам. Так, например, формула

~(человек (цезарь)& существующий (цезарь))

преобразуется в

~человек(цезарь) # существующий (цезарь)

а

~аll(Х, человек (X))

преобразуется в

exists(Х,~человек(Х))

Преобразования, выполняемые на втором этапе, основаны на следующих фактах:

~(α&β)значит то же самое, что и (~α) # (~β)

~exists(ν,ρ)значит то же самое, что и all(ν,~ρ)

~all(ν,ρ)значит то же самое, что и exists(ν,~ρ)