/* A program transforming propositional formulas into CNF */


/* Operator Definitions */

:- op(140,fy,neg).
:- op(150,xfy,and).
:- op(160,xfy,or).
:- op(170,xfx,imp).
:- op(180,xfx,equ).


/* Rules for step 1 of the algorithm */


step1(neg X, neg Y) :- step1(X,Y).
step1(X and Y, U and V) :- step1(X,U), step1(Y,V).
step1(X or Y, U or V) :- step1(X,U), step1(Y,V).
step1(X equ Y, (U imp V) and (V imp U)) :- step1(X,U), step1(Y,V).
step1(X imp Y, U imp V) :- step1(X,U), step1(Y,V).
step1(X,X).



/* Rules for step 2 of the algorithm */


step2(neg X, neg Y) :- step2(X,Y).
step2(X and Y, U and V) :- step2(X,U), step2(Y,V).
step2(X or Y, U or V) :- step2(X,U), step2(Y,V).
step2(X imp Y, neg U or V) :- step2(X,U), step2(Y,V).
step2(X,X).


/* Rules for step 3 of the algorithm */

step3(X and Y, U and V) :- step3(X,U), step3(Y,V).
step3(X or Y, U or V) :- step3(X,U), step3(Y,V).
step3(neg(X and Y), U or V) :- step3(neg X, U), step3(neg Y,V).
step3(neg(X or Y), U and V) :- step3(neg X, U), step3(neg Y,V).
step3(neg neg X, Y):- step3(X,Y).
step3(X,X).


/* Negation Normal Form */

negation(X,V) :- step1(X,Y), step2(Y,Z), step3(Z,V),!.


/* Rules for step 4 of the algorithm */

step4([K|R],Y) :- member(Conj,K),
    Conj = X1 and X2,
    remove(Conj, K, Temp),
    Newcon1 = [X1|Temp],
    Newcon2 = [X2|Temp],
    Y=[Newcon1,Newcon2|R].

step4([K|R],Y) :- member(Disj,K),
    Disj = X1 or X2,
    remove(Disj, K, Temp),
    Newcon = [X1,X2|Temp],
    Newcon2 = [X2|Temp],
    Y=[Newcon|R].

step4([K|R],[K|NR]) :- step4(R,NR).


/* Conjunctive Normal Form */

expand(X,Z) :- step4(X,Y), expand(Y,Z).
expand(X,X).


conjunctive(X,Z) :- negation(X,Y), expand([[Y]],Z), !.


/* Clause Form */

clause_form(X,Z) :- conjunctive(X,Y), double(Y,Z), !.


/* Auxiliary Predicates */
/* remove(E,L1,L2) removes each occurrence of element E in L1 to obtain L2 */

remove(_,[],[]).
remove(I,[I|T],NT) :- !,remove(I,T,NT).
remove(I,[H|T],[H|NT]) :- remove(I,T,NT).

/* listToSet(L,S) removes duplicates in L to obtain set S */

listToSet([K|R],Y) :- member(K,R), !,
    remove(K,R,NR),
    Y1=[K|NR], listToSet(Y1,Y).
listToSet([K|R],[K|NR]) :- listToSet(R,NR).
listToSet([],[]).

/* double(LL,LS) removes duplicates in each element of the list of lists LL to obtain LS */

double([K|R],[NK|NR]) :- listToSet(K,NK), double(R,NR).
double([],[]).