Article:
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
them.
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.