Книга: ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

Этап 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 соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.

Оглавление книги