phrase(Cтип,Слова):- Стип =.. [Pred|Args], присоединить(Args,[Слова,[]],Newargs), Цель =.. [Pred|Newargs], call (Цель).

где присоеднить определен так же как в разд. 3.6.

Как было обещано в гл. 10, мы проиллюстрируем процесс преобразования формулы исчисления предикатов в стандартную форму, представив фрагменты программы на Прологе, выполняющей это преобразование. Верхний уровень программы выглядит следующим образом:

translate(X):-

 implout(X,Xl), /* Этап 1 */

 negin(Xl,X2), /* Этап 2 */

 skolem(X2,X3,[]), /* Этап 3 */

 univout(X3,X4), /* Этап 4 */

 conjn(X4,X5), /* Этап 5 */

 clausify(X5,Clauses, []), /* Этап 6 */

 pclauses(Clauses). /* Печать дизъюнктов */

Здесь приведено определение предиката translate, действующего таким образом, что, если выполнить целевое утверждение translate(X), где X – это формула исчисления предикатов, то программа напечатает эту формулу в стандартной форме в виде последовательности дизъюнктов. В этой программе формулы исчисления предикатов представляются в виде структур языка Пролог, как на это указывалось ранее (в гл. 10). Однако мы сделаем некоторое отступление от предыдущего описания и будем представлять переменные, входящие в формулы исчисления предикатов, атомами языка Пролог, с целью облегчить их обработку. Предполагается, что можно отличить переменные в формулах исчисления предикатов от констант, используя некоторое соглашение относительно формы записи имен. Например, можно считать, что имена переменных всегда начинаются с одной из букв х, у, z. В действительности, переменные всегда вводятся в формулу посредством кванторов и, следовательно, их легко можно опознать. Лишь при чтении результата, печатаемого программой, программисту необходимо помнить, какие имена соответствуют переменным формул исчисления предикатов, а какие константам.

Прежде всего, необходимо объявить операторы для логических связок, используемых в формулах:

?- op(30,fx,~).

?- op(100,xfy,#).

?- op(100,xfy,&).

?- op(150,xfy,-›).

?- op(150,xfy,‹-›).

Следует обратить внимание на то, как определены операторы. В частности ~ имеет более низкий приоритет чем # и &. Для начала, необходимо сделать одно важное предположение. Предполагается, что переменные переименованы таким образом, что в обрабатываемой формуле одна и та же переменная никогда не вводится более чем одним квантором. Это необходимо, чтобы предотвратить возможные конфликты в употреблении имен в дальнейшем.

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

Определим предикат implout так, что implout(X, Y) означает, что формула Y получается из формулы X путем исключения всех импликаций.

implout((P ‹-› Q), (P1 & Q1) # (~Р1 & ~Q1))):- !, implout(P,Pl), implout(Q,Ql).

implout((P -› Q),(~P1 # Q1)):-!, implout(P,P1), implout(Q,Q1).

implout(all(X,P),all(X,P1)):- !.

implout(exists(X,P),exists(X,P1)):-!, implout(P, P1).

implout((P & Q),(P1 & Q1)):- !, implout(P,P1), implout(Q,Q1).

implout((P # Q),(P1 # Q1)):-!, implout(P,P1), implout(Q,Q1).

implout((-P),(~Pl)):-!, implout(P,P1).

implout(P,P).

Здесь необходимо определить два предиката – negin и neg. Целевое утверждение negin(X, Y) означает, что формула Y получена из X в результате применения к ней преобразования «перенос отрицания». Этот предикат является основным и именно к нему производится обращение из программы. Целевое утверждение neg(X, Y) означает, что формула Y получена из формулы ~X с помощью того же преобразования, что и в negin. В обоих случаях предполагается, что формула прошла обработку на первом этапе и, следовательно, не содержит -› и ‹-›

negin((~P),P1):-!, neg(P,P1).

negin(all(X,P),all(X,P1)):-!, negin(P,P1).

negin(exists(X,P),exists(X,P1)):-!, negin(P,P1).

negin((P & Q),(P1 & Q1)):-!, negin(P,P1), negin(Q,Q1).

negin((P # Q),(P1 # Q1)):-!, negin(P,P1), negin(Q,Q1).

negin(P,P).

neg((~P),P1):-!, negin(P,P1).

neg(all(X,P), exists(X,P1)):-!, neg(P,P1).

neg(exists(X,P),all(X,P1)):-!, neg(P,P1).

neg((P & Q),(P1 # Q1)):-!, neg(P,P1), neg(Q, Q1).

neg((P # Q),(P1 & Q1)):~!, neg(P,P1), neg(Q, Q1).

neg(P,(~P)).

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

skolem(all(X,P),all(X,P1),Vars):-!, scolem(P,Pl,[X|Vars]).

skolem(exists(X,P),P2,Vars):-!, gensym(f,F), Sk =..[F|Vars], subst(X,Sk,P,P1), skolem(P1,P2,Vars).

skolem((P # Q),(P1 # Q1),Vars):-!, skolem(P,P1,Vars), skolem(Q,Q1,Vars).

skolem((P & Q),(P1 & Q1), Vars):-!, skoIem(P,P1,Vars), skolem(Q,Q1,Vars).

skolem(P,P,_).

В этом определении используются два новых предиката. Предикат gensym должен быть определен таким образом, что целевое утверждение gensym(X, Y) вызывает конкретизацию переменной Y значением, представляющим новый атом, построенный из атома X и некоторого числа. Он используется для порождения сколемовских констант, не использовавшихся ранее. Предикат gensym определен в разд. 7.8 как генатом. Второй новый предикат, о котором уже упоминалось, это subst. Мы требуем, чтобы subst(Vl,V2,F1,F2) было истинно, если формула F2 получается на F1 в результате замены всех вхождений V1 на V2. Определение этого предиката оставлено в качестве упражнения для читателя. Оно аналогично определениям, приведенным в разд. 7.5 и 6.5.

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

univout(all(X,P), P1):- !, univout(P,P1).

univout((P & Q),(P1 & Q1)):-!, univout(P,P1), univout(Q,Q1).

univout((P # Q),(P1 # Q1)):- !, univout(P,P1), univout(Q,Q1).

univout(P,P).

Эти правила определяют предикат univout таким образом, что univout(X, Y) означает, что Y получается из X в результате вынесения и удаления кванторов общности.

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