23:- module( tableaux, [prove/5,
   24		      yadlr_concept/2, yadlr_relation/2, yadlr_instance/2,
   25		      yadlr_concept_name/2, yadlr_relation_name/2,
   26		      yadlr_instance_name/2,
   27		      yadlr_assert/3, yadlr_init/1,
   28		      yadlr_retrieve_concept/2, yadlr_retrieve_instance/2,
   29		      set_debug_msgs/1, set_depth_limit/1,
   30		      set_proof_tree_log/1, unset_proof_tree_log/0] ).   31
   32
   33:- use_module(library(lists), [append/3,flatten/2]).

   40:-
   41%   op(400, fxy, all),   % for all
   42%   op(400, fxy, exi),   % exists
   43   op(400, fy,  -),    % negation
   44   op(500, xfy, &),   % conjunction
   45   op(600, xfy, v),   % disjunction
   46   op(650, xfy, =>),  % implication
   47   op(700, xfy, <=>). % equivalence

   54%  exists X s.t. p(a,X) is represented as pred(p,pos,a,X)
   55%  for all X,   ~p(a,X) is represented as pred(p,neg,a,all)
   56
   57poslit( pred(pos,_,_,_) ). poslit( pred(pos,_,_) ).
   58neglit( pred(neg,_,_,_) ). neglit( pred(neg,_,_) ).
   59
   60contradict( pred(pos,F,A),     pred(neg,F,A) ).
   61contradict( pred(neg,F,A),     pred(pos,F,A) ).
   62contradict( pred(pos,F,A1,A2), pred(neg,F,A1,A2) ).
   63contradict( pred(neg,F,A1,A2), pred(pos,F,A1,A2) ).

   70% a branch is four lists of expressions,
   71% one with ground, atomic predicates,
   72% one with existentially quantified atomic predicates,
   73% one with other subformulas already dealt with,
   74% one with the TODO subformulas.
   75
   76%
   77% get_next/3 ( +Branch, -SubF, -Branch )
   78%
   79% gets the next sub-formula that still has work to do be done,
   80% and returns the subformula and the Branch without the said
   81% subformula
   82
   83get_next( branch(Ground,Exists,Rest,[SubF|TODO]), SubF,
   84          branch(Ground,Exists,[SubF|Rest],TODO) ).
   85
   86add_next(_, [], _) :- !, fail.
   87add_next( branch(Ground1,Exists,Rest,TODO1), L, branch(Ground2,Exists,Rest,TODO2) ) :-
   88	!,
   89	ground_literals(L, Ground, NotGround),
   90	append(Ground,Ground1,Ground2),
   91	append(NotGround,TODO1,TODO2).
   92
   93ground_literal(p, pred(pos,p) ).
   94ground_literal(q, pred(pos,q) ).
   95ground_literal(-p, pred(neg,p) ).
   96ground_literal(-q, pred(neg,q) ).
   97
   98ground_literals([], [], []).
   99ground_literals([Head|Tail], Ground, Rest) :-
  100	ground_literals(Tail, Ground1, Rest1),
  101	(ground_literal(Head,Pred) -> 
  102	    Ground = [Pred|Ground1], Rest = Rest1
  103	;
  104	    Ground = Ground1, Rest = [Head|Rest1]
  105	).
  106
  107expand(-(T1 <=> T2), [-(T1 => T2)],           [-(T2 => T1)] ) :- !.
  108expand( (T1 <=> T2), [(T1 => T2),(T2 => T1)], [] ) :- !.
  109expand(-(T1  => T2), [T1,-T2],                [] ) :- !.
  110expand( (T1  => T2), [-T1],                   [T2] ) :- !.
  111expand(-(T1  &  T2), [-T1],                   [-T2]) :- !.
  112expand( (T1  &  T2), [T1,T2],                 [] ) :- !.
  113expand(-(T1  v  T2), [(-T1),(-T2)],           []) :- !.
  114expand( (T1  v  T2), [T1],                    [T2] ) :- !.
  115expand( -T,          [-T],                    [] ) :- !.
  116expand(  T,          [T],                     [] ).
  117
  118
  119%
  120% recurse/2 ( +Branch, -Res )
  121%
  122% InBranch is a branch. OutBranches are brances, after one
  123% expansion step. NOTE: Disjunctions will output two branches from
  124% a single input branch.
  125
  126try_one(F,_,F).
  127try_one(_,F,F).
  128
  129recurse( branch(Ground, Exist, Rest, []), [] ) :- !,
  130	% DEBUG
  131	print(branch(Ground, Exist, Rest, [])), nl,
  132	print(closed), nl,
  133	fail.
  134recurse(Branch, Res) :-
  135	% DEBUG
  136	print(Branch), nl,
  137	get_next(Branch, SubF, Branch1),
  138	expand(SubF, F1, F2),
  139	!,
  140	try_one(F1, F2, F),
  141	add_next(Branch1, F, Branch2),
  142	recurse(Branch2, Res).
  143
  144prove(F,Res) :- recurse( branch([],[],[],[-F]), Res1 ) -> Res=Res1 ; Res=valid