Cut normal forms and proof complexity

Annals of Pure and Applied Logic 97 (1-3):127-177 (1999)
  Copy   BIBTEX

Abstract

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal form and monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

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

On the non-confluence of cut-elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.
On the complexity of proof deskolemization.Matthias Baaz, Stefan Hetzl & Daniel Weller - 2012 - Journal of Symbolic Logic 77 (2):669-686.
Complexity of resolution proofs and function introduction.Matthias Baaz & Alexander Leitsch - 1992 - Annals of Pure and Applied Logic 57 (3):181-215.
Uniqueness of normal proofs of minimal formulas.Makoto Tatsuta - 1993 - Journal of Symbolic Logic 58 (3):789-799.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Nisan-Wigderson generators in proof systems with forms of interpolation.Ján Pich - 2011 - Mathematical Logic Quarterly 57 (4):379-383.
Normal forms for elementary patterns.Timothy J. Carlson & Gunnar Wilken - 2012 - Journal of Symbolic Logic 77 (1):174-194.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.

Analytics

Added to PP
2014-01-16

Downloads
20 (#744,405)

6 months
3 (#1,023,809)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Unsound inferences make proofs shorter.Juan P. Aguilera & Matthias Baaz - 2019 - Journal of Symbolic Logic 84 (1):102-122.
On the complexity of proof deskolemization.Matthias Baaz, Stefan Hetzl & Daniel Weller - 2012 - Journal of Symbolic Logic 77 (2):669-686.
Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.
Describing proofs by short tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.

View all 7 citations / Add more citations

References found in this work

Untersuchungen über das logische Schließen. II.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 39:405–431.
Proof Theory and Logical Complexity. [REVIEW]Helmut Pfeifer - 1991 - Annals of Pure and Applied Logic 53 (4):197.

Add more references