Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs

Logic Journal of the IGPL 15 (5-6):553-575 (2007)
  Copy   BIBTEX


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



    Upload a copy of this work     Papers currently archived: 89,654

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Analytic cut trees.Carlo Cellucci - 2000 - Logic Journal of the IGPL 8 (6):733-750.
Describing proofs by short tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
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.
Proofs with monotone cuts.Emil Jeřábek - 2012 - Mathematical Logic Quarterly 58 (3):177-187.
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.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.


Added to PP

11 (#965,719)

6 months
2 (#648,997)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Dov Gabbay
Hebrew University of Jerusalem

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references