A Labelled System for IPL with Variable Splitting

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.

http://dx.doi.org/10.1007/978-3-540-73595-3_10

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

Abstract

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.