Программирование на языке пролог
Шрифт:
Процесс приведения формулы исчисления предикатов к стандартной форме состоит из шести основных этапов.
Процедура начинается с замены всех вхождений -› и ‹- ›в соответствии с их определениями, данными в разд. 10.1. Так, например, формула
аll(Х,мужчина(Х) -› человек(Х))
будет преобразована в формулу
аll(Х,~мужчина(Х) # человек(Х))
На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. Если такой случай имеет место, то формула переписывается
~(человек (цезарь)& существующий (цезарь))
преобразуется в
~человек(цезарь) # существующий (цезарь)
а
~аll(Х, человек (X))
преобразуется в
exists(Х,~человек(Х))
Преобразования, выполняемые на втором этапе, основаны на следующих фактах:
~(&)значит то же самое, что и (~) # (~)
~exists(,)значит то же самое, что и all(,~)
~all(,)значит то же самое, что и exists(,~)
После завершения второго этапа каждое вхождение отрицания в формулу будет относиться лишь к атомарным подформулам. Атомарная формула или ее отрицание называется литералом.На всех последующих этапах литералы обрабатываются как единый элемент, а то, какие литералы представлены отрицанием, будет существенным лишь в самом конце.
На следующем этапе удаляются кванторы существования. Это делается путем введения новых констант – сколемовских констант– вместо переменных связанных (введенных) квантором существования. Вместо того чтобы говорить, что существует объект, обладающий некоторым множеством свойств, можно ввести имя для такого объекта и просто сказать, что он обладает данными свойствами. Это соображение лежит в основе введения сколемовских констант. Сколемизация более существенно изменяет логические свойства формулы, чем все обсуждавшиеся ранее преобразования. Тем не менее, она обладает следующим важным свойством. Если имеется формула, то интерпретация, в которой эта формула истинна, существует тогда и только тогда, когда существует интерпретация, в которой истинна формула, полученная из первой в результате сколемизации. Такая форма эквивалентности формул вполне достаточна для наших целей. Так, например, формула
exists(X,женщина(X)& мать(Х,ева))
в результате сколемизации преобразуется в формулу
женщина(g1)& мать(g1, ева)
где g1– некоторая новая константа, не использовавшаяся ранее. Константа g1представляет некоторую женщину, мать которой есть Ева. То, что для обозначения константы использован символ» отличный от использовавшихся ранее, существенно, так как в высказывании ничего не говорится о том, что какой-то конкретный человек является дочерью Евы. В утверждении говорится лишь о том, что такой человек существует. Может оказаться, что g1будет соответствовать тот же самый человек, который соответствует другой константе, но это уже дополнительная информация, никак не выраженная в высказывании.
Если формула содержит кванторы общности, то процедура сколемизации уже не столь проста. Например, если в формуле [17]
аll(Х, человек(Х) -› exists(Y,мать(X,Y)))
(«каждый человек имеет мать») заменить каждое вхождение переменной V, связанной квантором существования, на константу g2и удалить квантор существования, то получится:
all(X, человек(Х) -› мать(X,g2))
Последнее высказывание говорит о том, что все люди имеют одну и туже
17
В некоторых последующих примерах допущена неточность: в формулах используется импликация, хотя все импликации должны быть удалены на первом этапе.- Прим. перев.
all(X, человек(Х) -› мать(Х, g2(Х)))
В этом случае функциональный символ g2соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.
Этот этап очень прост. Каждый квантор общности просто выносится в начало формулы. Это не влияет на значение формулы. Так, например, формула
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– грязный.
На этом этапе исходная формула исчисления предикатов претерпела довольно много изменений. Формула больше не содержит в явном виде кванторов, а из логических связок в ней остались лишь & и # (помимо отрицания, входящего в состав литералов). Теперь формула преобразуется к специальному виду – конъюнктивной нормальной форме,характерной тем, что дизъюнктивные члены формулы не содержат внутри себя конъюнкцию. Таким образом, формулу можно преобразовать к такому виду, когда она будет представлять последовательность элементов, соединенных друг с другом конъюнкциями, а каждый элемент является либо литералом, либо состоит из нескольких литералов, соединенных дизъюнкцией. Чтобы привести формулу к такому виду, необходимо использовать следующие два тождества:
(А&В) # Сэквивалентно (А # С)&(В # С)
А # (В&С)эквивалентно ( А # В)&(А # С)
Так, например, формула:
выходной(Х) # (работает(крис, X) & (сердитый (крис) # унылый(крис)))
(Для каждого Xлибо X– выходной день, либо Крис работает в день Xи при этом он либо сердитый, либо унылый) эквивалентна следующей:
выходной(Х) # (работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))