/*************************************************************************

         name: propTabl.pl
      version: June 28, 2002
  description: Predicates for Propositional Tableaux
      authors: Michael Kohlhase, Aljoscha Burchardt, Stephan Walter
 
*************************************************************************/

:- [comsemOperators].


/*=====================================================
  tabl/3
======================================================*/


tabl(true(A & B),InBranch,OutBranch) :-
	!,tabl(true(A),InBranch,K), 
	tabl(true(B),K,OutBranch).
 
tabl(false(A & _),InBranch,H) :- 
	tabl(false(A),InBranch,H).

tabl(false(_ & B),InBranch,H) :- 
	!,tabl(false(B),InBranch,H).

tabl(true(~A),InBranch,H) :- 
	!,tabl(false(A),InBranch,H).

tabl(false(~A),InBranch,H) :- 
	!,tabl(true(A),InBranch,H).

tabl(F,InBranch,OutBranch) :- 
	OutBranch = [F|InBranch],
	\+ clash(OutBranch).


/*=====================================================
  clash/1
======================================================*/

clash(List) :- 
	member(true(A),List),
	member(false(A),List).


