Consistency of Variable Splitting in Free Variable Systems of First-Order Logic
In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX, Koblenz, Germany, volume 3702 of Lecture Notes in Computer Science, pages 33-47, Springer-Verlag, 2005.
We prove consistency of a sequent calculus for classical logic with explicit splitting of free variables by means of a semantical soundness argument. The free variable system is a mature formulation of the system proposed at TABLEAUX 2003 . We also identify some challenging and interesting open research problems.