:-op(140,fy,neg).
:-op(160, xfx, [and, or, imp, revimp, nand, nor, notimp, notrevimp]).

member(X,[X|_]).
member(X,[_|Xs]) :- member(X,Xs).

remove(_X,[],[]).
remove(X,[X|Xs],Ys) :-
	remove(X,Xs,Ys).
remove(X,[Y|Xs],[Y|Ys]) :-
	X \== Y,
	remove(X,Xs,Ys).

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
	append(Xs,Ys,Zs).

is_unary(neg neg _X).
is_unary(neg true).
is_unary(neg false).

is_conjunctive(_X and _Y).
is_conjunctive(neg(_X or _Y)).
is_conjunctive(neg(_X imp _Y)).
is_conjunctive(neg(_X revimp _Y)).
is_conjunctive(neg(_X nand _Y)).
is_conjunctive(_X nor _Y).
is_conjunctive(_X notimp _Y).
is_conjunctive(_X notrevimp _Y).

is_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _Y).
is_disjunctive(_X revimp _Y).
is_disjunctive(_X nand _Y).
is_disjunctive(neg(_X nor _Y)).
is_disjunctive(neg(_X notimp _Y)).
is_disjunctive(neg(_X notrevimp _Y)).

component(neg neg X, X).
component(neg true, false).
component(neg false, true).

components(X and Y, X,Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y,X,Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X revimp Y, X, neg Y).
components(neg(X revimp Y), neg X, Y).
components(X nand Y, neg X, neg Y).
components(neg (X nand Y), X,Y).
components(X nor Y,neg X, neg Y).
components(neg(X nor Y), X,Y).
components(X notimp Y, X, neg Y).
components(neg(X notimp Y), neg X, Y).
components(X notrevimp Y, neg X, Y).
components(neg(X notrevimp Y), X, neg Y). 

stepDNF([C|Cs],NCs) :-
	member(Formula,C),
	is_unary(Formula),
	component(Formula,Newformula),
	remove(Formula,C,NC0),
	append(NC0,[Newformula],NC),
	append(Cs,[NC],NCs).
stepDNF([C|Cs],NCs) :-
	member(Alpha,C),
	is_conjunctive(Alpha),
	components(Alpha,Alpha1,Alpha2),
	remove(Alpha,C,NC0),
	append(NC0,[Alpha1,Alpha2],NC),
	append(Cs,[NC],NCs).
stepDNF([C|Cs],NCs) :-
	member(Beta,C),
	is_disjunctive(Beta),
	components(Beta,Beta1,Beta2),
	remove(Beta,C,NC0),
	append(NC0,[Beta1],NC1),
	append(NC0,[Beta2],NC2),
	append(Cs,[NC1,NC2],NCs).	
stepDNF([C|Cs],[C|NCs]) :-
	stepDNF(Cs,NCs).

% tests
:-stepDNF([[neg neg p]],[[p]]).
:-stepDNF([[p or q]],[[p],[q]]).
:-stepDNF([[p and q]],[[p,q]]).
:-stepDNF([[(p imp (q imp r)) imp ((p imp q) imp (p imp r))]],X).

expand1(Cs,Cs).
expand1(Cs,NCs) :-
	stepDNF(Cs,Cs0),
	expand1(Cs0,NCs).

expand2(Cs,NCs) :-
	stepDNF(Cs,Cs0),
	expand2(Cs0,NCs).
expand2(Cs,Cs).

towards_DNF(X,Y) :- expand1([[X]],Y).

dualclauseform(X,Y) :- expand2([[X]],Y).

% tableau prover

closed([]).
closed([B|Bs]) :-
	member(false,B),
	closed(Bs).
closed([B|Bs]) :-
	member(X, B),
	member(neg X, B),
	closed(Bs).

tableau_thm(X) :-
	expand2([[neg X]],Y),
	closed(Y).

expand_and_close(T) :-
	closed(T).
expand_and_close(T0) :-
	stepDNF(T0,T1),
	expand_and_close(T1).

tableau_thm2(X) :-
	expand_and_close([[neg X]]).

% tests
:-tableau_thm(x or neg x).
:-tableau_thm2(x or neg x).
:-tableau_thm2(((p and (q imp (r or s))) imp (p or q))).
:-tableau_thm(((p and (q imp (r or s))) imp (p or q))).