/*****************************/
/* Christian Ohlsson         */
/* Logik för dataloger       */
/* Karlstad 990228           */
/* Laboration 3 i Logik      */
/*****************************/
/* Functions included        */
/* prenex                    */
/* implout                   */
/* negin                     */
/* kvant                     */
/* free_in                   */
/* rename_var                */
/*****************************/  

:- op(200,fx,~).
:- op(400,xfy,#).
:- op(400,xfy,&).
:- op(700,xfy,->).
:- op(700,xfy,<->).               

prenex(Formel,PNF):-
	implout(Formel,Svar1),
	negin(Svar1,Svar2),
	kvant(Svar2,PNF,[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10],L).

/* *****************************   IMPLOUT   **************************** */  

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(exist(X,P),exist(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   **************************** */ 

negin((~P),P1) :- !,neg(P,P1).
negin(all(X,P),all(X,P1)) :- !,negin(P,P1).
negin(exist(X,P),exist(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),exist(X,P1)) :- !,neg(P,P1).
neg(exist(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)).             
                        
/* *****************************   RENAME-VAR   **************************** */ 

r_v(X,exist(X,P),exist(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
r_v(X,exist(Y,P),exist(Y,P1),[F|R]):-  X\==Y, r_v(X,P,P1,[F|R]).

r_v(X,all(X,P),all(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
r_v(X,all(Y,P),all(Y,P1),[F|R]):-  X\==Y, r_v(X,P,P1,[F|R]).

r_v(X,Y#Z,Y1#Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
r_v(X,Y&Z,Y1&Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]). 
r_v(X,Y->Z,Y1->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
r_v(X,Y<->Z,Y1<->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).

r_v(X,Y,Y2,[F|R]):- Y=..[T,S],r_v(X,S,Y1,[F|R]), Y2=..[T,Y1].
r_v(X,[T|S],[F|S1],[F|R]):- X==T, r_v(X,S,S1,[F|R]).
r_v(X,[T|S],[S2|S1],[F|R]):- X\==T, r_v(X,S,S1,[F|R]),r_v(X,T,S2,[F|R]).
r_v(X,~P,~P1,[F|R]):- r_v(X,P,P1,[F|R]).
r_v(X,X,F,[F|R]).
r_v(X,U,U,[F|R]):- X\==U.
    
/* *****************************   FREE   ****************************** */ 

free_in(X,exist(Y,P)):- X\==Y, free_in(X,P).
free_in(X,all(Y,P)):- X\==Y, free_in(X,P).
free_in(X,Y#Z):-free_in(X,Y);free_in(X,Z).
free_in(X,Y&Z):-free_in(X,Y);free_in(X,Z).
free_in(X,Y->Z):-free_in(X,Y);free_in(X,Z).
free_in(X,Y<->Z):-free_in(X,Y);free_in(X,Z).

free_in(X,Y):- Y=..[F,R],free_in(X,R).
free_in(X,[F|R]):-free_in(X,F);free_in(X,R).

free_in(X,~Z):-free_in(X,Z).
free_in(X,X).
                              

/* ********************************************************************* */ 
/* *****************************   ALL &   ***************************** */ 

kvant(all(X,Y)&Z,SY,[F|R],L3):-   
	(free_in(X,Z),
	r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(all(X,(Y1&Z2)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(all(X,(Y1&Z2)),SY,L2,L3)).  
                          
/* *****************************   & ALL   **************************** */ 

kvant(Z&all(X,Y),SY,[F|R],L3):-   
	(free_in(X,Z),
       r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(all(X,(Z2&Y1)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(all(X,(Z2&Y1)),SY,L2,L3)).  
 

/* *****************************   ALL #   **************************** */ 

kvant(all(X,Y)#Z,SY,[F|R],L3):-   
	(free_in(X,Z),
        r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
        kvant(all(X,(Y1#Z2)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(all(X,(Y1#Z2)),SY,L2,L3)).  

                                             
/* *****************************   # ALL   **************************** */ 

kvant(Z#all(X,Y),SY,[F|R],L3):-   
	(free_in(X,Z),
       r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(all(X,(Z2#Y1)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(all(X,(Z2#Y1)),SY,L2,L3)). 
 

/* ***************************   EXIST &   ************************** */ 

kvant(exist(X,Y)&Z,SY,[F|R],L3):-   
	(free_in(X,Z),
       r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(exist(X,(Y1&Z2)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(exist(X,(Y1&Z2)),SY,L2,L3)).  
   
/* ***************************   & EXIST   ************************** */ 

kvant(Z&exist(X,Y),SY,[F|R],L3):-   
	(free_in(X,Z),
       r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(exist(X,(Z2&Y1)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(exist(X,(Z2&Y1)),SY,L2,L3)).  
   
/* ***************************   EXIST #   ************************** */ 

kvant(exist(X,Y)#Z,SY,[F|R],L3):-   
	(free_in(X,Z),
	r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(exist(X,(Y1#Z2)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(exist(X,(Y1#Z2)),SY,L2,L3)).
       
/* ***************************   # EXIST   ************************** */ 

kvant(Z#exist(X,Y),SY,[F|R],L3):-   
	(free_in(X,Z),
	r_v(X,Z,Z1,[F]),
	kvant(Y,Y1,R,R1),
	kvant(Z1,Z2,R1,L2),
       kvant(exist(X,(Z2#Y1)),SY,L2,L3));
        	(kvant(Y,Y1,R,R1),
                kvant(Z,Z2,R1,L2),
                kvant(exist(X,(Z2#Y1)),SY,L2,L3)). 
 


/* ***************************     &       ************************** */ 

kvant(P&Q,PQ,L,L3):-
      kvant(P,P1,L,L1),
      kvant(Q,Q1,L1,L2),
      ((P1\==P);(Q1\==Q)),
      kvant(P1&Q1,PQ,L2,L3).
 
/* ***************************     #       ************************** */ 

kvant(P#Q,PQ,L,L3):-
      kvant(P,P1,L,L1),
      kvant(Q,Q1,L1,L2),
      ((P1\==P);(Q1\==Q)),
      kvant(P1#Q1,PQ,L2,L3).

/* ***************************    EXIST   ************************** */ 

kvant(all(X,F),all(X,F1),L1,L2):-
       kvant(F,F1,L1,L2).
       
/* ***************************   ALL        ************************** */ 

kvant(exist(X,F),exist(X,F1),L1,L2):-
       kvant(F,F1,L1,L2).

/* ***************************   BASFALL    ************************** */ 

kvant(X,X,L,L).