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

         name: fo.pl
      version: July 2002
  description: Driver Predicates for First Order Tableaux
      authors: Aljoscha Burchardt, Stephan Walter
 
*************************************************************************/
:- module(fo,[theorem/2,modGen/3,modGenWrite/3]).
:- use_module(comsemLib,[naonly/2]).
:- [user:comsemOperators].
:- [foTabl].

/*=====================================================
  Theorem Proving
======================================================*/

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


/*=====================================================
  Model Generation
======================================================*/

modGen(Formula,Model,Qdepth) :-
	naonly(Formula,ConvFormula),
	tabl(true(ConvFormula),[],Model,[],[],Qdepth).

modGen(_,_,_) :- 
	format("~nNo model found!~n",[]).


/*=====================================================
  Model Generation w. Output
======================================================*/

modGenWrite(F,M,Qd) :-
	modGen(F,M,Qd),
	sort(M,MS),
	output(MS,true),
	output(MS,false).

output(Model,Sign) :-
	format('~n~n*** ~w ***~n',[Sign]),
	tab(2),
	outRec(Model,0,Sign),
	format('~n************',[]).
	
outRec([],_,_).

outRec([SF|Fs],Num,Sign):-
	SF =.. [Sign,F],
	(Num = 5 -> (OutNum = 0,nl,tab(2));OutNum is Num+1),
	format('~w ; ',[F]),
	outRec(Fs,OutNum,Sign).

outRec([_|Fs],Num,Sign):-
	outRec(Fs,Num,Sign).

/*
 modGen((forall(x,man(x)>(exists(y,man(y)&father(y,x))))&man(john)),M,10).
theorem((forall(x,man(x)v~man(x))),10).
*/