Equal rights for the cut: Computable non-analytic cuts in cut-based proofs

TY - JOUR

T1 - Equal rights for the cut: Computable non-analytic cuts in cut-based proofs

AU - Finger, M

AU - Gabbay, D

PY - 2007

Y1 - 2007

N2 - This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof. We then concentrate on the problem of efficiently computing non-analytic cuts. For that, we study the generalisation of techniques present in many modern theorem provers, namely the techniques of conflict-driven formula learning

AB - This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof. We then concentrate on the problem of efficiently computing non-analytic cuts. For that, we study the generalisation of techniques present in many modern theorem provers, namely the techniques of conflict-driven formula learning

U2 - 10.1093/jigpal/jzm040

DO - 10.1093/jigpal/jzm040

M3 - Article

VL - 15

SP - 553

EP - 575

JO - LOGIC JOURNAL- IGPL

JF - LOGIC JOURNAL- IGPL

IS - 5-6

ER -