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

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

Этап 2 - перенос отрицания внутрь формулы

Этап 1 - исключение импликаций

Определим предикат 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 предполагает, что указанные операции будут применяться лишь после того, как полностью будут завершены первые три этапа преобразования. Следовательно, формула не должна содержать импликаций и кванторов существования.

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

Реальная программа для преобразования формулы в конъюнктивную нормальную форму является значительно более сложной по сравнению с последней программой. При обработке формулы вида (Р # Q), где Р и Q – произвольные формулы, прежде всего, необходимо преобразовать Р и Q в конъюнктивную нормальную

форму, скажем P1 и Q1. И только после этого можно применять одно из преобразований, дающих эквивалентную формулу. Процесс обработки должен происходить именно в таком порядке, так как может оказаться, что ни Р ни Q не содержат& на верхнем уровне, а Р1 и Q1 содержат. Программа имеет вид:

conjn((P # Q),R):-!, conjn(P,P1), conjn(Q,Q1), conjn1((P1 # Q1),R).

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

conjn(P,P).

conjn1(((P & Q) # R), (P1 & Q1)):-!, conjn((P # Q), P1), conjn((Q # R), Q1).

conjn1((P # (Q & R)),(P1 & Q1)):-!, conjn((P # Q), P1), conjn((P # R), Q1).

conjn1(P,P).

Дата добавления: 2014-12-08