%
%  Test programs for semantic tableaux.
%

%
%  One of these lines should be commented.
%

:- load_files(tabl).      % To test simple tableau construction.
%:- load_files(systab).    % To test systematic tableau construction.

test_tableau(Fml) :-
  to_internal(Fml, FmlI),
  create_tableau(FmlI, Tab),
  write_tableau(Tab).

t1 :- test_tableau(
  ~ ( (p -> q -> r ) -> (p -> q) -> (p -> r) ) ).

t2 :- test_tableau(
     (p -> q) -> (r v p ) -> (r v q) ).

t3 :- test_tableau(
  p ^
  (p -> (q v r) ^ ~ (q ^ r)) ^
  (p -> (s v t) ^ ~ (s ^ t)) ^
  (s -> q) ^
  (~ r -> t) ^ 
  (t -> s)
      ).

t4 :- test_tableau(
   ~ (p v q) ^ ~ ~ (p v q)
   ).