Separation results for the size of constant-depth propositional proofs

Annals of Pure and Applied Logic 136 (1-2):30-55 (2005)
  Copy   BIBTEX


This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle



    Upload a copy of this work     Papers currently archived: 76,442

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

A note on propositional proof complexity of some Ramsey-type statements.Jan Krajíček - 2011 - Archive for Mathematical Logic 50 (1-2):245-255.
Matrix identities and the pigeonhole principle.Michael Soltys & Alasdair Urquhart - 2004 - Archive for Mathematical Logic 43 (3):351-357.
Sharpened lower bounds for cut elimination.Samuel R. Buss - 2012 - Journal of Symbolic Logic 77 (2):656-668.
The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
Simplified Lower Bounds for Propositional Proofs.Alasdair Urquhart & Xudong Fu - 1996 - Notre Dame Journal of Formal Logic 37 (4):523-544.
Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.


Added to PP

19 (#590,037)

6 months
1 (#454,876)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Quantified propositional calculi and fragments of bounded arithmetic.Jan Krajíček & Pavel Pudlák - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):29-46.
Dynamic ordinal analysis.Arnold Beckmann - 2003 - Archive for Mathematical Logic 42 (4):303-334.

View all 6 references / Add more references