/************************************************************************* File: freeVarTabl.pl Copyright (C) 2004 Patrick Blackburn & Johan Bos This file is part of BB1, version 1.2 (August 2005). 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.