
% TEST: [c/\(a\/b)]?(~a)/\a.

:- op(510, fx, [~]).
:- op(520, xfy, [/\]).
:- op(530, xfy, [\/]).
:- op(540, xfx, [->]).
:- op(550, xfx, [?]).

Assumptions?Goal:- 
	transform(Assumptions, Goal, Formula),
	setup(Formula, Valuation),
	(generate(Valuation),
	value(Formula,t,Valuation),
	write('not valid'));
	write('valid').

transform([],G,~G).
transform([H|T],G,H/\X):- transform(T,G,X).

setup(A,[[A|_]]):- atomic(A).
setup(~F,V):-  setup(F,V).
setup(F,V):- 
	F=..[_,A,B], 
	setup(A,X), 	
	setup(B,Y),
	union(X,Y,V).

generate([]).
generate([[A,V]|T]):-
	(V=t; V=f),
	generate(T).

value(A,Z,V):- atomic(A),!,member([A,Z],V).
value(~A,Z,V):- value(A,X,V), truth_table(~X,Z).
value(A/\B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X/\Y,Z).
value(A\/B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X\/Y,Z).
value(A->B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X->Y,Z).

truth_table(t/\t,t):- !.
truth_table(_/\_,f).
truth_table(f\/f,f):- !.
truth_table(_\/_,t).
truth_table(t->f,f):- !.
truth_table(_->_,t).
truth_table(~t,f).
truth_table(~f,t).

union([],Y,Y).
union([[A,_]|T],Y,Z):- member([A,_],Y),!, union(T,Y,Z).
union([[A,V]|T],Y,[[A,V]|Z]):- union(T,Y,Z).
member(X,[H|T]):- X=H;member(X,T).

subterm(T,T).
subterm(S,T):- T =..[_|Args], sub(S, Args).
sub(S, [First|Rest]):- subterm(S, First); sub(S,Rest).





