Sharpened lower bounds for cut elimination

Journal of Symbolic Logic 77 (2):656-668 (2012)

Abstract
We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth d of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to d — 0(1). The proof method is based on more efficiently expressing the Gentzen-Solovay cut formulas as low depth formulas.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1333566644
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 39,951
Through your library

References found in this work BETA

Proof Theory and Logical Complexity.Helmut Pfeifer & Jean-Yves Girard - 1989 - Journal of Symbolic Logic 54 (4):1493.
The Role of Quantifier Alternations in Cut Elimination.Philipp Gerhardy - 2005 - Notre Dame Journal of Formal Logic 46 (2):165-171.
Cut Normal Forms and Proof Complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Analytics

Added to PP index
2012-04-05

Total views
32 ( #246,477 of 2,235,909 )

Recent downloads (6 months)
2 ( #758,721 of 2,235,909 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature