Incremental variable splitting (Q429591): Difference between revisions

The main contribution of this paper is to adapt the incremental closure framework for free variables to variable splitting tableaux. The variable splitting method for free-variable tableau calculi provides an admissibility condition under which the same free variables can be assigned values independently on different branches. While this can be very useful for automated proof search, a direct implementation of this condition is impractical. In this paper it is shown how the incremental closure approach can be extended to provide an incremental, and therefore tractable, evaluation of the global closure criterion of the variable splitting calculus. The admissibility condition for closing substitutions is expressed as a constraint satisfaction problem. This allows one to devise a mechanism which checks the existence of an admissible closing substitution incrementally, during the construction of a proof. A rule-based algorithm for testing satisfiability of constraints that accounts for split variables is specified. Experimental results -- based on a prototype variable splitting theorem prover implemented in Java -- are provided.