Logic Journal of the IGPL 15 (5-6):553-575 (2007)
AbstractThis 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
Similar books and articles
Towards Automated First-Order Abduction: The Cut-Based Approach.Marcelo Finger - 2012 - Logic Journal of the IGPL 20 (2):370-387.
Describing Proofs by Short Tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Lower Bounds for Cutting Planes Proofs with Small Coefficients.Maria Bonet, Toniann Pitassi & Ran Raz - 1997 - Journal of Symbolic Logic 62 (3):708-728.
Normal Derivations and Sequent Derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.
Type Two Cuts, Bad Cuts and Very Bad Cuts.Renling Jin - 1997 - Journal of Symbolic Logic 62 (4):1241-1252.
Cut Normal Forms and Proof Complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.
Cut-Based Abduction.Marcello D'agostino, Marcelo Finger & Dov Gabbay - 2008 - Logic Journal of the IGPL 16 (6):537-560.
Imperative Programs as Proofs Via Game Semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
Connection-Driven Inductive Theorem Proving.Christoph Kreitz & Brigitte Pientka - 2001 - Studia Logica 69 (2):293-326.
Consistency Statements and Iterations of Computable Functions in IΣ1 and PRA.Joost J. Joosten - 2010 - Archive for Mathematical Logic 49 (7-8):773-798.
Best-Path Theorem Proving: Compiling Derivations.Martin Frické Frické - 2012 - In James Maclaurin (ed.), Rationis Defensor.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
Added to PP
Historical graph of downloads