Roger Antonsen, Arild Waaler

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.

@InProceedings{AntonsenWaaler07b, author = {Roger Antonsen and Arild Waaler}, editor = {Frank Pfenning}, title = {A {L}abelled {S}ystem for {IPL} with {V}ariable {S}plitting}, booktitle = {CADE-21, 21th International Conference on Automated Deduction, Bremen, Germany}, volume = 4603, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, year = {2007}, isbn = {978-3-540-73594-6}, pages = {132–146}, ee = {http://dx.doi.org/10.1007/978-3-540-73595-3_10} }

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.