inKNF(and(X,Y)):-inKNF(X),inKNF(Y).
inKNF(X):-isClause(X).

isClause(var(X)).
isClause(not(var(X))).
isClause(or(X,Y)):-isClause(X),isClause(Y).

%------------------------

toKNF(X,X):-inKNF(X).
toKNF(X,Z) :- trans(X,Y),toKNF(Y,Z). 


trans(not(not(X)),X).

trans(not(and(X,Y)) ,or(not(X),not(Y))).
trans(not(or(X,Y))  ,and(not(X),not(Y))).

trans(or(and(X,Y),Z),and(or(X,Z),or(Y,Z))).
trans(or(X,and(Y,Z)),and(or(X,Y),or(X,Z))).

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


%-----------------------------

toClauseSet(X,YS) :- inKNF(X),toClauseSet2(X,YS).

toClauseSet2(and(X,Y),ZS)  :- toClauseSet2(X,XS),toClauseSet2(Y,YS),append(XS,YS,ZS).
toClauseSet2(or(X,Y),[ZS]) :- toClause(or(X,Y),ZS).
toClauseSet2(not(X),[ZS])  :- toClause(not(X),ZS).
toClauseSet2(var(X),[ZS])  :- toClause(var(X),ZS).

toClause(or(X,Y),ZS) :- toClause(X,XS),toClause(Y,YS),append(XS,YS,ZS).
toClause(not(var(X)),[not(var(X))]).
toClause(var(X),[var(X)]).

append([],XS,XS).
append([X|XS],YS,[X|ZS]):-append(XS,YS,ZS).