Arnold Beckmann and Samuel R. Buss,
"Separation results for the size of constant-depth propositional proofs"
Annals of Pure and Applied Logic 136, no. 1-2 (2005) 30-55.
Download article: postscript or PDF.
This paper proves exponential separations
between depth d LK and depth(d+1/2)-\LK for every half integer d utilizing the
order induction principle. As a consequence, we obtain an exponential
separation between depth d-LK and depth (d+1)-LK for integers d. We investigate
the relationship between the sequence-size, tree-size and height of depth
d-LK-derivations for half integers d, and describe transformations between
We define a general method to lift principles requiring exponential tree-size (d+1/2)-LK refutations 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.
Back to Sam Buss's publications page.