%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 
%%%   normalize.P
%%%      xsb version
%%%   Convert wffs to list of normal logic clauses
%%%
%%%   and       /\  
%%%   or        \/
%%%   not       ~
%%%   xor       xor
%%%   implies   =>   
%%%   iff       <=>  
%%%   all       all(X,-)
%%%   some      exists(Y,-)
%%%
%%%    all(X,p(X) => exists(Y, r(Y) /\ q(X,Y))) 
%%%  --------------------------------------------
%%%    p(X) => r(sk1(X)) /\ q(X,sk1(X))
%%%  --------------------------------------------
%%%    r(sk1(X)) :- p(X).
%%%    q(X,sk1(X)) :- p(X).

:- op(300,fx,'~').
:- op(400,yfx,'/\').  
:- op(500,yfx,'\/').
:- op(600,xfx,'=>').
:- op(650,xfx,'<=>').
:- op(350,xfx,'xor').


%%%%%%%%%%%%%%%%%%%%%%
%%% generate a skolem 
:- dynamic skolems/1.
:- assert(skolems([sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,
                   sk12,sk13,sk14,sk15,sk16,sk17,sk18,sk19,sk20])).
genskolem(SK) :- retract(skolems([SK|R])),
                 assert(skolems(R)).


  %%----- drive negation inward --------------
conVert(~(~X),Uvars,Y) :- 
   !,
   conVert(X,Uvars,Y).
conVert(~(X /\ Y),Uvars,A) :- 
   !,
   conVert((~X \/ ~Y), Uvars,A).
conVert(~(X \/ Y),Uvars,A) :- 
   !,
   conVert((~X /\ ~Y),Uvars,A).
conVert(~(X => Y),Uvars,A) :-              
   !,
   conVert((X /\ ~Y),Uvars,A).
conVert(~(X <=> Y),Uvars,A) :-             
   !,
   conVert((X /\ ~Y) \/ (~X /\ Y),Uvars,A).
conVert(~exists(X,P),Uvars,A) :- 
   !,
   conVert(all(X,~P),Uvars,A).
conVert(~all(X,P),Uvars,A) :- 
   !,
   conVert(exists(X,~P),Uvars,A).
conVert(~(X xor Y),Uvars,A) :-
   !,
   conVert((X /\ Y) \/ (~X /\ ~Y), Uvars, A).
  %%----- quantifiers -----------------------
conVert(all(X,P),Uvars,Q) :-
   !,
   not occurs(X,Uvars),       %% MUST use separate variables
   conVert(P,[X|Uvars],Q).
conVert(exists(X,P),Uvars,Q) :-
   !,
   not occurs(X,Uvars),       %% MUST use separate variables
   genskolem(SK),
   X=..[SK|Uvars],
   conVert(P,Uvars,Q). 
  %%----- connectives ------------------------
conVert((X <=> Y),Uvars,(A /\ B)) :-
   !,
   conVert((X => Y),Uvars,A),
   conVert((Y => X),Uvars,B).
conVert((X => Y),Uvars,Q) :-
   !,
   conVert((~X \/ Y),Uvars,Q).
conVert((X /\ Y),Uvars,(A /\ B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
conVert((X \/ Y),Uvars,(A \/ B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
conVert((X xor Y),Uvars,(A \/ B) /\ (~A \/ ~B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
  %%----- logically atomic --------------------
conVert(X,_,X).


%%----- distribute --------------------------
distriBute((X /\ Y) \/ Z, 
            (X \/ Z) /\ (Y \/ Z),true) :- !.
distriBute(X \/ (Y /\ Z),
             (X \/ Y) /\ (X \/ Z),true) :- !.
distriBute(X,X,fail).


%%----- conjunctive normal form --------------
cnF((X /\ Y),(A /\ B)) :-
   !,
   cnF(X,A),
   cnF(Y,B).
cnF((X \/ Y),G) :-
   !,
   cnF(X,A),
   cnF(Y,B),
   distriBute((A \/ B),F,Flag),
   (Flag -> cnF(F,G)  %% More work may be needed
             ;
            G = F ).
cnF(X,X).


%%-----  make a sequence out of a conjunction -----
flatten_and(X /\ Y, F) :-
   !,
   flatten_and(X,A),
   flatten_and(Y, B),
   sequence_append(A,B,F).
flatten_and(X,X).

%%-----  make a sequence out of a disjunction -----
flatten_or(X \/ Y, F) :-
   !,
   flatten_or(X,A),
   flatten_or(Y,B),
   sequence_append(A,B,F).
flatten_or(X,X).


%%----- append two sequences -------------------------------
sequence_append((X,R),S,(X,T)) :- !, sequence_append(R,S,T).
sequence_append((X),S,(X,S)).

%%----- separate into positive and negative literals -----------
separate((A,B),P,N) :- 
   !,
   (A = ~X -> N=[X|N1],
               separate(B,P,N1)
             ;
               P=[A|P1],
               separate(B,P1,N) ).
separate(A,P,N) :-
   (A = ~X -> N=[X],
               P = []
            ;
               P=[A],
               N = [] ).

%%----- tautology ----------------------------
tautology(P,N) :- some_occurs(N,P).

some_occurs([F|R],B) :-
   occurs(F,B) | some_occurs(R,B).

occurs(A,[F|_]) :-
   A == F,
   !.
occurs(A,[_|R]) :-
   occurs(A,R).

%%----- normalize(+Wff,-NormalClauses) ------
normalize(Wff,NormalClauses) :- 
   conVert(Wff,[],S),
   cnF(S,T),
   flatten_and(T,U),
   make_clauses(U,NormalClauses).

make_clauses((A,B),C) :-
   !,
   flatten_or(A,F),
   separate(F,P,N),
   (tautology(P,N) -> 
      make_clauses(B,C)
          ;
      make_clause(P,N,D),
      C = [D|R],
      make_clauses(B,R) ).
make_clauses(A,C) :-
   flatten_or(A,F),
   separate(F,P,N),
   (tautology(P,N) ->
       C = []
        ;
       make_clause(P,N,D),
       C = [D] ).

make_clause([],N, (false :- B)) :-
   !,
   make_sequence(N,B,',').
make_clause(P,[],H) :-
   !,
   make_sequence(P,H,'|').
make_clause(P,N, (H :- T)) :-
   make_sequence(P,H,'|'),
   make_sequence(N,T,',').

make_sequence([A],A,_) :- !.
make_sequence([F|R],(F|S),'|') :-
   make_sequence(R,S,'|').
make_sequence([F|R],(F,S),',') :-
   make_sequence(R,S,',').


%% --------- to test program -------------
test :- write('wff? '),
        read(Wff),
        normalize(Wff,NCs),
        write_list(NCs),
        nl, test.

write_list([F|R]) :- 
   write(F), write('.'), nl,
   write_list(R).
write_list([]).