% Propositional Logic Formula Represented as a Prolog Term:
%  - p(X)  == atomic proposition X
%  - not(X) == ~(X)
%  - and(X,Y) == X & Y
%  - or(X,Y) == X or Y
%  - impl(X,Y) == X -> Y
%  - equiv(X,Y) == X <=> Y


% example formula (Knights & Knaves example)
formula(and(equiv(p(a),or(not(p(b)),not(p(c)))),
            equiv(p(b),p(a)))).

% pretty-print a formula	
pp(p(X)) :- print(X).
pp(not_p(X)) :- print('~'),print(X).
pp(or(X,Y)) :- print('('),pp(X), print(' or '), pp(Y), print(')').
pp(and(X,Y)) :- print('('),pp(X), print(' & '), pp(Y), print(')').
pp(impl(X,Y)) :- print('('),pp(X), print(' -> '), pp(Y), print(')').
pp(equiv(X,Y)) :- print('('),pp(X), print(' <=> '), pp(Y), print(')').
pp(not(X)) :- print('~('),pp(X),print(')').
%pp(X) :- print('### ERROR :'),print(X).



% phase 1 & 2: get rid of impl & equiv + push negation inside
convert(not(X),Res) :- push_negation(X,Res).
convert(impl(X,Y),Res) :- convert(or(not(X),Y),Res).
convert(equiv(X,Y),Res) :- convert(and(impl(X,Y),impl(Y,X)),Res).
convert(p(X),p(X)).
convert(or(X,Y),or(CX,CY)) :- convert(X,CX), convert(Y,CY).
convert(and(X,Y),and(CX,CY)) :- convert(X,CX), convert(Y,CY).


push_negation(p(X),not_p(X)).
push_negation(not(X),Res) :- convert(X,Res).
push_negation(and(X,Y),or(NX,NY)) :- push_negation(X,NX), push_negation(Y,NY).
push_negation(or(X,Y),and(NX,NY)) :- push_negation(X,NX), push_negation(Y,NY).
push_negation(impl(X,Y),Res) :- push_negation(or(not(X),Y),Res).
push_negation(equiv(X,Y),Res) :- push_negation(and(impl(X,Y),impl(Y,X)),Res).
	

% Still to do: phase 2: distribute & and or, push or inside

distribute(p(X),p(X)).
distribute(not_p(X),not_p(X)).
distribute(and(X,Y),and(DX,DY)) :- distribute(X,DX), distribute(Y,DY).
distribute(or(X,Y),Res) :- distribute(X,DX), distribute(Y,DY),
 distribute_or(DX,DY,Res).

distribute_or(and(X,Y),Z,and(XZ,YZ)) :- !,distribute_or(X,Z,XZ),distribute_or(Y,Z,YZ).
distribute_or(Z,and(X,Y),and(XZ,YZ)) :- !,distribute_or(Z,X,XZ),distribute_or(Z,Y,YZ).
distribute_or(A,B,or(A,B)).



run :- formula(F),
       print('Initial Formula: '),nl, pp(F),nl,
       convert(F,F2),
       print('After conversion and pushing negation:'),nl,pp(F2),nl,
       distribute(F2,CNF),
       print('Final CNF: '),nl,pp(CNF),nl.