%
%  Test program for semantic tableaux.
%

:- load_files(tabl).
user:file_search_path(common,'../common').
:- ensure_loaded(common(intext)).
:- ensure_loaded(common(io)).

test(Fml) :-
  to_internal(Fml, FmlE),
  create_tableau(FmlE, Tab),
  write_tableau(Tab).

t1 :- test(~ ( all(X, (p(X) -> q(X))) -> (all(X, p(X)) -> all(X, q(X))) )).

t2 :- test(~ (all(X, p(X)) -> all(Y, p(Y)))).

t3 :- test(~ ( ex(X, all(Y, p(X, Y))) -> all(Y, ex(X, p(X, Y))))).

t4 :- test(~ (all(X, p(X) -> q) <-> (ex(X, p(X)) -> q))).