?-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).

expand(Cs,NCs) :-
	stepDNF(Cs,Cs0),
	expand(Cs0,NCs).
expand(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_prover(X) :-
	expand([[neg X]],Y),
	closed(Y).

tableau_prover2(X) :-
	expand([[neg X]],Y),
	!,
	closed(Y).

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

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

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

% examples from lecture 
:- tableau_prover((p imp (q imp r)) imp ((p or s) imp ((q imp r) or s))).
:- tableau_prover((p and (q imp (r or s))) imp (p or q)).
:- tableau_prover(((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s)))).

% shows inefficiency of prover 1
:- \+ tableau_prover2(neg (((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s))))).

% shows inefficiency of prover 2 and breaks booltool
:- tableau_prover2(neg (((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s)))) or (((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s))))).
:- tableau_prover3(neg (((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s)))) or (((p and q) or (r imp s)) imp ((p or (r imp s)) and (q or (r imp s))))).