У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

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

Реальная программа для преобразования формулы в конъюнктивную нормальную форму является значительно более сложной по сравнению с последней программой. При обработке формулы вида (Р # 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).

Здесь представлена последняя часть программы приведения формулы к стандартной форме. Прежде всего, определим предикат clausify, который осуществляет построение внутреннего представления совокупности дизъюнктов. Эта совокупность представлена в виде списка, каждый элемент которого является структурой вида cl(A, В). В этой структуре А– это список литералов без отрицания, а В– список литералов с отрицанием (знак отрицания ~ явно не содержится). Предикат clausifyимеет три аргумента. Первый аргумент для формулы, передаваемой с пятого этапа обработки, Второй и третий аргументы используются для представления списков дизъюнктов. Предикат clausifyсоздает список, заканчивающийся переменной, а не пустым списком ( []) как обычно, и возвращает эту переменную посредством третьего аргумента. Это позволяет другим правилам добавлять элементы в конец этого списка, конкретизируя соответствующим образом указанную переменную. В программе выполняется проверка с целью выявления ситуаций, когда одна и та же атомарная формула входит в дизъюнкт как с отрицанием, так и без него. Если такая ситуация имеет место, то соответствующий дизъюнкт не добавляется к списку, так как подобные дизъюнкты являются тривиально истинными и не дают ничего нового. Выполняется также проверка неоднократного вхождения литерала в дизъюнкт.

clausify((P& Q),C1,C2):-!, clausify(P,C1,C3), clausify(Q,C3,C2).

clausify(P,[cl(A,B)|Cs],Cs):- inclause(P,A,[],B,[]),!.

clausify(_,C,C).

inclause((P # Q), A, A1, B, B1):-!, inclause(P,A2,A1,B2,B1),inclause(Q,A,A2,B,B2).

inclause((~P),A,A,B1,B):-!, notin(P,A), putin(P,B,B1).

inclause(P,A1,A,B,B):- notin(P,B), putin(P,A,A1).

notin(X,[X|_]):-!, fail.

notin(X,[_|L]):-!, notin(X,L).

notin(X,[]).

putin(X,[],[X]):-!.

putin(X,[X|L],L):-!.

putin(X,[Y|L], [Y|L1]):- putin(X,L,L1).

Теперь будет определен предикат pclausesпечатающий формулу, представленную указанным способом, в соответствии с принятой формой записи.

pclauses([]):-!, nl, nl.

pclauses([cl(A,B)|Cs]):- pclause(A,B), nl, pclauses(Cs).

pclause(L,[]):-!, pdisj(L), write('.').

pclause([],L):-!, write(':-'), pconj(L), write('.').

pclause(L1,L2):- pdisj(L1), write(':-'), pconj(L2), write('.').

pdisj([L]):-!, write(L).

pdisj([L|Ls]):- write(L), write(';'), pdisj(Ls).

pconj([Lj):-!, write(L).

pconj([L|Ls]):- write(L), write(','), pconj(Ls).

В настоящее время существует много различных версий Пролога, которые можно встретить во многих организациях. Разнообразие версий отчасти объясняется разнообразием имеющихся ЭВМ. Нет двух ЭВМ, для которых с одинаковой легкостью писались бы все возможные программы. Это нашло отражение в том, что различные реализации Пролога отличаются друг от друга по своим возможностям. Но даже две ЭВМ одного и того же типа могут работать с разными операционными системами. Операционная система – это программа, осуществляющая общее управление работой ЭВМ, в том числе контроль за эффективным распределением ресурсов между пользователями ЭВМ. Одни операционные системы разрешают программисту использовать широкий набор возможностей, обеспечиваемых ЭВМ. Набор допустимых средств других более скромен. Отсюда и различия между Пролог-системами. Наконец, создатели Пролог-систем часто расходятся в представлениях о том, какие возможности являются лишь эстетически приятными, а какие действительно необходимы. В результате никакие две Пролог-системы не совпадают полностью по возможностям, и не похоже, что эта ситуация вскоре изменится, поскольку относительно реализаций Пролога постоянно возникают новые идеи и усовершенствования.