%
%  Tests for semantic tableaux, built in two possible ways
%

:- ensure_loaded('../Evaluations/tableau.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/external_operators.pl').

:- operators_for_external_representation.

%
%  test1(+ExternalFormula)
%
test1(ExternalFormula) :-
	from_external_to_internal(ExternalFormula, Formula),
	create_tableau(Formula, Tableau),
	write_tableau(Tableau).

t11 :- test1(~((p -> q -> r) -> (p -> q) -> p -> r)).

t12 :- test1((p -> q) -> (r v p ) -> (r v q)).

t13 :- test1(p ^
	   (p -> (q v r) ^ ~ (q ^ r)) ^
	   (p -> (s v t) ^ ~ (s ^ t)) ^
	   (s -> q) ^
	   (~ r -> t) ^ 
	   (t -> s)).

t14 :- test1(~(p v q) ^ ~ ~(p v q)).

%
%  test1(+ExternalFormula)
%
test2(ExternalFormula) :-
	from_external_to_internal(ExternalFormula, Formula),
	create_systematic_tableau(Formula, Tableau),
	write_tableau(Tableau).

t21 :- test2(~((p -> q -> r) -> (p -> q) -> p -> r)).

t22 :- test2((p -> q) -> (r v p ) -> (r v q)).

t23 :- test2(p ^
	   (p -> (q v r) ^ ~ (q ^ r)) ^
	   (p -> (s v t) ^ ~ (s ^ t)) ^
	   (s -> q) ^
	   (~ r -> t) ^ 
	   (t -> s)).

t24 :- test2(~(p v q) ^ ~ ~(p v q)).