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}
}

Sammendrag

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.