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

    File: freeVarTabl.pl
    Copyright (C) 2004,2005,2006 Patrick Blackburn & Johan Bos

    This file is part of BB1, version 1.3 (November 2006).

    BB1 is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    BB1 is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with BB1; if not, write to the Free Software Foundation, Inc., 
    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

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

:- module(freeVarTabl,[info/0,
                       infix/0,
                       prefix/0,
                       tprove/1,
                       tprove/2,
		       tprove/3,
		       tproveTestSuite/0]).

:- use_module(comsemPredicates,[infix/0,
                                prefix/0,
                                memberList/2,
				removeFirst/3,
				appendLists/3,
                                basicFormula/1,
                                compose/3,
				newFunctionCounter/1,
                                substitute/4]).

:- use_module(folTestSuite,[formula/2]).


/*========================================================================
   Expand Tableau until it is closed, allowing Qdepth 
   applications of the universal rule.
========================================================================*/

closedTableau([],_Q):- !.

closedTableau(OldTableau,Qdepth):-
   expand(OldTableau,Qdepth,TempTableau,NewQdepth), !,
   removeClosedBranches(TempTableau,NewTableau),
   closedTableau(NewTableau,NewQdepth).


/*========================================================================
   Remove all closed branches
========================================================================*/

removeClosedBranches([],[]).

removeClosedBranches([Branch|Rest],Tableau):-
   closedBranch(Branch), !,
   removeClosedBranches(Rest,Tableau).

removeClosedBranches([Branch|Rest],[Branch|Tableau]):-
   removeClosedBranches(Rest,Tableau).


/*========================================================================
   Check whether a branch is closed
========================================================================*/

closedBranch(Branch):-
   memberList(n(_,t(X)),Branch),
   memberList(n(_,f(Y)),Branch),
   basicFormula(X), 
   basicFormula(Y),
   unify_with_occurs_check(X,Y).


/*========================================================================
   VarList is a list of free variables, and SkolemTerm is a previously 
   unused Skolem function symbol fun(N) applied to those free variables.
========================================================================*/

skolemFunction(VarList,SkolemTerm):-
   newFunctionCounter(N),
   compose(SkolemTerm,fun,[N|VarList]).


/*========================================================================
   Try to create a tableau expansion for f(X) that is closed allowing 
   Qdepth applications of the universal rule.
========================================================================*/

tprove(X,Qdepth):-
   notatedFormula(NotatedFormula,[],f(X)),
   closedTableau([[NotatedFormula]],Qdepth).

tprove(X,Qdepth,Result):-
   notatedFormula(NotatedFormula,[],f(X)),
   (
      closedTableau([[NotatedFormula]],Qdepth), !,
      Result = theorem
   ;
      Result = unknown
   ).


/*========================================================================
   Prove a formula with Q-depth of 100 (default)
========================================================================*/

tprove(X):-
   tprove(X,1000).


/*========================================================================
   Notate the free variables of a formula
========================================================================*/

notatedFormula(n(Free,Formula),Free,Formula).


/*========================================================================
   Prove all formulas from the test suite 
========================================================================*/

tproveTestSuite:-
   format('~n~n>>>>> FREE VARIABLE TABLEAU ON TEST SUITE <<<<<',[]),
   formula(Formula,Status),
   format('~n~nInput formula: ~p~nStatus: ~p',[Formula,Status]),
   tprove(Formula,100,Result), 
   format('~nProver: ~p~n',[Result]),
   fail.

tproveTestSuite.


/*========================================================================
   Newtableau with Q-depth NewQdepth is the result of applying  
   a tableau expansion rule to Oldtableau with a Q-depth of OldQdepth.
========================================================================*/

expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):-
   unaryExpansion(Branch,NewBranch).

expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):-
   conjunctiveExpansion(Branch,NewBranch).

expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):-
   existentialExpansion(Branch,NewBranch).

expand([Branch|Tableau],QD,[NewBranch1,NewBranch2|Tableau],QD):-
   disjunctiveExpansion(Branch,NewBranch1,NewBranch2).

expand([Branch|Tableau],OldQD,NewTableau,NewQD):-
   universalExpansion(Branch,OldQD,NewBranch,NewQD),
   appendLists(Tableau,[NewBranch],NewTableau).

expand([Branch|Rest],OldQD,[Branch|Newrest],NewQD):-
   expand(Rest,OldQD,Newrest,NewQD).


/*========================================================================
   Take Branch as input, and return NewBranches if a tableau rule
   allows unary expansion.
========================================================================*/

unaryExpansion(Branch,[NotatedComponent|Temp]) :-
   unary(SignedFormula,Component),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotatedComponent,Free,Component).


/*========================================================================
   Take Branch as input, and return the NewBranch if a tableau rule 
   allows conjunctive expansion. 
========================================================================*/

conjunctiveExpansion(Branch,[NotatedComp1,NotatedComp2|Temp]):-
   conjunctive(SignedFormula,Comp1,Comp2),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotatedComp1,Free,Comp1),
   notatedFormula(NotatedComp2,Free,Comp2).


/*========================================================================
   Take Branch as input, and return the NewBranch1 and NewBranch2 
   if a tableau rule allows disjunctive expansion. 
========================================================================*/

disjunctiveExpansion(Branch,[NotComp1|Temp],[NotComp2|Temp]):-
   disjunctive(SignedFormula,Comp1,Comp2),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotComp1,Free,Comp1),
   notatedFormula(NotComp2,Free,Comp2).


/*========================================================================
   Take Branch as input, and return the NewBranch if a tableau rule 
   allows existential expansion.
========================================================================*/

existentialExpansion(Branch,[NotatedInstance|Temp]):-
   notatedFormula(NotatedFormula,Free,SignedFormula),
   existential(SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   skolemFunction(Free,Term),
   instance(SignedFormula,Term,Instance),
   notatedFormula(NotatedInstance,Free,Instance).


/*========================================================================
   Take Branch and OldQD as input, and return the NewBranch and 
   NewQDepthif a tableau rule allow universal expansion.
========================================================================*/

universalExpansion(Branch,OldQD,NewBranch,NewQD):-
   OldQD > 0, 
   NewQD is OldQD - 1,
   memberList(NotatedFormula,Branch),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   universal(SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   instance(SignedFormula,V,Instance),
   notatedFormula(NotatedInstance,[V|Free],Instance),
   appendLists([NotatedInstance|Temp],[NotatedFormula],NewBranch).


/*========================================================================
   Decompose conjunctive signed formula
========================================================================*/

conjunctive(t(and(X,Y)),t(X),t(Y)).
conjunctive(f(or(X,Y)),f(X),f(Y)).
conjunctive(f(imp(X,Y)),t(X),f(Y)).


/*========================================================================
   Decompose disjunctive signed formula
========================================================================*/

disjunctive(f(and(X,Y)),f(X),f(Y)).
disjunctive(t(or(X,Y)),t(X),t(Y)).
disjunctive(t(imp(X,Y)),f(X),t(Y)).


/*========================================================================
   Decompose unary signed formula
========================================================================*/

unary(t(not(X)),f(X)).
unary(f(not(X)),t(X)). 


/*========================================================================
   Universal Signed Formulas
========================================================================*/

universal(t(all(_,_))).
universal(f(some(_,_))).


/*========================================================================
   Existential Signed Formulas
========================================================================*/

existential(t(some(_,_))).
existential(f(all(_,_))).


/*========================================================================
   Remove quantifier from signed quantified formula, and replacing all
   free occurrences of the quantified variable by occurrences of Term.
========================================================================*/

instance(t(all(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF).
instance(f(some(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF).
instance(t(some(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF).
instance(f(all(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF).


/*========================================================================
   Info
========================================================================*/

info:-
   format('~n> ----------------------------------------------------------------------------- <',[]),
   format('~n> freeVarTabl.pl, by Patrick Blackburn and Johan Bos                            <',[]),
   format('~n>                                                                               <',[]),
   format('~n> ?- tprove(Form).            - Try to prove Form                               <',[]),
   format('~n> ?- tprove(Form,QDepth).     - Try to prove Form using QDepth                  <',[]),
   format('~n> ?- tprove(Form,QDepth,Res). - Try to prove Form using QDepth, return Res      <',[]),
   format('~n> ?- tproveTestSuite.         - runs the test suite for theorem proving         <',[]),
   format('~n> ?- infix.                   - switches to infix display mode                  <',[]),
   format('~n> ?- prefix.                  - switches to prefix display mode                 <',[]),
   format('~n> ?- info.                    - show this information                           <',[]),
   format('~n> ----------------------------------------------------------------------------- <',[]),
   format('~n~n',[]).


/*========================================================================
   Display info at start
========================================================================*/

:- info.

