Roger Antonsen and Arild Waaler

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.

@InProceedings{AntonsenWaaler05, author = {Roger Antonsen and Arild Waaler}, title = {Consistency of {V}ariable {S}plitting in {F}ree {V}ariable {S}ystems of {F}irst-{O}rder {L}ogic}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX, Koblenz, Germany}, year = 2005, pages = {33–47}, series = {Lecture Notes in Computer Science}, editor = {Bernhard Beckert}, volume = 3702, isbn = {3-540-28931-3}, publisher = {Springer-Verlag}, ee = {http://dx.doi.org/10.1007/11554554_5} }

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 [1]. We also identify some challenging and interesting open research problems.