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

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

Этап 3 - сколемизация

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

exists(X,женщина(X)& мать(Х,ева))

в результате сколемизации преобразуется в формулу

женщина(g1)& мать(g1, ева)

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

Если формула содержит кванторы общности, то процедура сколемизации уже не столь проста. Например, если в формуле ^[17]

аll(Х, человек(Х) -› exists(Y,мать(X,Y)))

(«каждый человек имеет мать») заменить каждое вхождение переменной V, связанной квантором существования, на константу g2и удалить квантор существования, то получится:

all(X, человек(Х) -› мать(X,g2))

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

all(X, человек(Х) -› мать(Х, g2(Х)))

В этом случае функциональный символ g2соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.

Этап 4 - вынесение кванторов общности в начало формулы

Этот этап очень прост. Каждый квантор общности просто выносится в начало формулы. Это не влияет на значение формулы. Так, например, формула

all(X, мужчина(Х) -› аll(Y,женщина(Y) -› нравится (X,Y)))

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

аll(Х, аll(Y,мужчина(Х) -› (женщина(Y) -› нравится (X,Y))))

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

аll(Х,живой(Х) # мертвый(Х)& аll(Y,нравится(мэри,Y) #грязный(Y))

теперь можно представить так:

(живой(Х) # мертвый(Х))& (нравится(мэри,Y) # грязный (Y))

Эта формула значит, что, какие бы Xи Yни были выбраны, либо Xживой, либо Xмертвый, и либо Мэри нравится Y, либо Y– грязный.

Этап 5 - использование дистрибутивных законов для & и #

На этом этапе исходная формула исчисления предикатов претерпела довольно много изменений. Формула больше не содержит в явном виде кванторов, а из логических связок в ней остались лишь & и # (помимо отрицания, входящего в состав литералов). Теперь формула преобразуется к специальному виду - конъюнктивной нормальной форме,характерной тем, что дизъюнктивные члены формулы не содержат внутри себя конъюнкцию. Таким образом, формулу можно преобразовать к такому виду, когда она будет представлять последовательность элементов, соединенных друг с другом конъюнкциями, а каждый элемент является либо литералом, либо состоит из нескольких литералов, соединенных дизъюнкцией. Чтобы привести формулу к такому виду, необходимо использовать следующие два тождества:

(А&В) # Сэквивалентно (А # С)&(В # С)

А # (В&С)эквивалентно ( А # В)&(А # С)