Преобразование формулы исчисления предикатов в стандартную форму - Prolog

Формулировка задачи:

Собственно мне нужно решить проблему автоматического преобразования формулы исчисления предикатов в стандартную форму для последующей работы с методом резолюций. Считается хорошим тоном решать подобные задачи на Прологе или Лиспе. Т.к. с Прологом знаком выбрал его. Думал зайду в интернет 10 минут посижу и все, скачал...но не тут-то было!! Вместо этого изучаю просторы библиотек и интернета недели две. Наткнулся на крайне интересную книжечку Клоксина и Меллиша по Прологу. [ссылка удалена - нарушение авторского права] В

Приложении В

описана программа которая мне и нужна, но вот с её реализацией плоховато. Пробовал на SWI-Prolog... Вот пытаю счастья в народе..может кто поможет...поделится мыслишками.

Решение задачи: «Преобразование формулы исчисления предикатов в стандартную форму»

textual
                            Листинг программы 
                        

                            translate(X):-
    implout(X,X1),
    negin(X1,X2),
    skolem(X2,X3,[]),
    univout(X3,X4),
    conjn(X4,X5),
    print(X5),nl,
    clausify(X5,Clauses,[]),
    pclauses(Clauses).
 
:-op(30,fx,~).
:-op(100,xfy,#).
:-op(100,xfy,&).
:-op(150,xfy,->).
:-op(150,xfy,<->).
 
 
implout((P<->Q),((P1 & Q1) # (~P1 & ~Q1))):-
    !,
    implout(P,P1),
    implout(Q,Q1).
implout((P->Q),(~P1 # Q1)):-!,
    implout(P,P1),
    implout(Q,Q1).
implout(all(X,P),all(X,P1)):-!, implout(P,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),(~P1)):-!, implout(P,P1).
implout(P,P).
 
 
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(all(X,P),all(X,P1),Vars):-!, skolem(P,P1,[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):-!,
    skolem(P,P1,Vars),
    skolem(Q,Q1,Vars).
skolem(P,P,_).
 
univout(all(_,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).
 
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((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(_,[]).
putin(X,[],[X]):-!.
putin(X,[X|L],L):-!.
putin(X,[Y|L],[Y|L1]):-putin(X,L,L1).
 
 
 
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([L]):-!, write(L).
pconj([L|Ls]):-write(L), write(','), pconj(Ls).
 
 
gensym(X,Y):-
    vid_nom(X,NUM),
    name(X,N1),
    cel_name(NUM,N2),
    prisoed(N1,N2,N),
    name(Y,N).
vid_nom(X,NUM):-
    retract(tek_num(X,NUM1)), !,
    NUM is NUM1+1,
    asserta(tek_num(X,NUM)).
vid_nom(X,1):-asserta(tek_nom(X,1)).
 
cel_name(CEL,ITOG):-cel_name(CEL,[],ITOG).
cel_name(I,TEK,[C|TEK]):-I<10,!,C is I+48.
cel_name(I,TEK,ITOG):-
    CHAS is I/10,
    OST is I mod 10,
    C is OST+48,
    cel_name(CHAS,[C|TEK],ITOG).
 
prisoed([],SP,SP).
prisoed([ZSP|SP1],SP2,[ZSP|SP3]):-
    prisoed(SP1,SP2,SP3).
 
subst(V1,V2,F,V2):-
    F==V1,
    !.
subst(_V1,_V2,F,F):-
    \+compound(F),
    !.
subst(V1,V2,F1,F2):-
    functor(F1, Functor, Arity),
    functor(F2, Functor, Arity),
    subst(Arity,V1,V2,F1,F2).
subst(0,_V1,_V2,_F1,_F2):-!.
subst(N,V1,V2,F1,F2):-
    arg(N,F1,Arg1),
    subst(V1,V2,Arg1,Arg2),
    arg(N,F2,Arg2),
    M is N-1,
    !,
    subst(M,V1,V2,F1,F2).
                        