A Labelled System for IPL with Variable Splitting
In Frank Pfenning, editor, CADE-21, 21th International Conference on Automated Deduction, Bremen, Germany, volume 4603, pages 132–146, Lecture Notes in Computer Science, Springer-Verlag, 2007.
The paper introduces a free variable, labelled proof system for intuitionistic propositional logic with variable splitting. In this system proofs can be found without backtracking over rules by generating a single, uniform derivation. We prove soundness, introduce a construction that extracts finite countermodels from unprovable sequents, and formulate a branchwise termination condition. This is the first proof system for intuitionistic propositional logic that admits goal-directed search procedures without compromising proof lengths, compared to corresponding tableau calculi.