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

         name: prop.pl
      version: July 2002
  description: Wrapper Predicate for Propositional Tableaux
      authors: Michael Kohlhase, Aljoscha Burchardt, Stephan Walter
 
*************************************************************************/
:- module(prop,[theorem/1,modGen/3]).
:- use_module(comsemLib,[naonly/2,toconj/2]).
:- [user:comsemOperators].
:- [propTabl].


theorem(Formula) :-	
	naonly(Formula,ConvFormula),
	\+ tabl(false(ConvFormula),[],_).


modGen(Formula,WKNumber,Model) :- 
	wk(WKNumber,WK), 
	toconj([Formula|WK],Conjunction),
	naonly(Conjunction,Converted),
	tabl(true(Converted),[],Model).


%% Example wk
wk(1,[man(john),love(john,mary)]).

/* Example calls
modGen(love(john,mary)>woman(mary),1,M).
theorem(walk(john) v (~walk(john))).
*/