Incremental Variable Splitting
Journal of Symbolic Computation, volume 47, number 9, pages 1046–1065, Springer-Verlag, 2012.
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 has a large potential for automated proof search, a direct implementation of this condition is impractical. We adapt the incremental closure framework for free variables to variable splitting tableaux by recasting the admissibility condition for closing substitutions into a constraint satisfaction problem. The resulting mechanism allows to check the existence of an admissible closing substitution incrementally during the construction of a proof. We specify a rule-based algorithm for testing satisfiability of constraints that accounts for split variables, and present experimental results based on a prototype variable splitting theorem prover implementation measuring the computational overhead of the variable splitting framework.