Прежде всего, необходимо объявить операторы для логических связок, используемых в формулах:
?- op(30,fx,~).
?- op(100,xfy,#).
?- op(100,xfy,&).
?- op(150,xfy,-›).
?- op(150,xfy,‹-›).
Следует обратить внимание на то, как определены операторы. В частности ~ имеет более низкий приоритет чем # и &. Для начала, необходимо сделать одно важное предположение. Предполагается, что переменные переименованы таким образом, что в обрабатываемой формуле одна и та же переменная никогда не вводится более чем одним квантором. Это необходимо, чтобы предотвратить возможные конфликты в употреблении имен в дальнейшем.
Для преобразования формул к стандартной форме мы используем метод преобразования дерева, обсуждавшийся в разд. 7.11 и 7.12. При представлении логических связок как функторов, формулы исчисления предикатов превращаются в структуры, которые могут быть изображены в виде деревьев. Каждый из шести основных этапов перевода в стандартную форму представляет некоторое преобразование дерева, которое отображает входное дерево в выходное.
Этап 1 - исключение импликаций
Определим предикат imploutтак, что implout(X, Y)означает, что формула Yполучается из формулы Xпутем исключения всех импликаций.
Здесь необходимо определить два предиката – neginи neg.Целевое утверждение negin(X, Y)означает, что формула Yполучена из Xв результате применения к ней преобразования «перенос отрицания». Этот предикат является основным и именно к нему производится обращение из программы. Целевое утверждение neg(X, Y)означает, что формула Yполучена из формулы ~Xспомощью того же преобразования, что и в negin.В обоих случаях предполагается, что формула прошла обработку на первом этапе и, следовательно, не содержит -› и ‹-›
Предикат skolemимеет три аргумента, соответствующих: исходной формуле, преобразованной формуле и списку переменных, которые на текущий момент были введены посредством кванторов общности.
В этом определении используются два новых предиката. Предикат gensymдолжен быть определен таким образом, что целевое утверждение gensym(X, Y)вызывает конкретизацию переменной Yзначением, представляющим новый атом, построенный из атома Xи некоторого числа. Он используется для порождения сколемовских констант, не использовавшихся ранее. Предикат gensymопределен в разд. 7.8 как генатом.Второй новый предикат, о котором уже упоминалось, это subst.Мы требуем, чтобы subst(Vl,V2,F1,F2)было истинно, если формула F2получается на F1в результате замены всех вхождений V1на V2.Определение этого предиката оставлено в качестве упражнения для читателя. Оно аналогично определениям, приведенным в разд. 7.5 и 6.5.
Этап 4 - вынесение кванторов общности в начало формулы
После выполнения этого этапа, естественно, будет необходимо иметь возможность указывать, какие атомы Пролога представляют переменные формулы исчисления предикатов, а какие атомы представляют константы. Мы больше не сможем воспользоваться удобным правилом, согласно которому переменными являются в точности те символы, которые вводятся с помощью кванторов. Здесь представлена программа, выполняющая операции вынесения и удаления кванторов общности.
