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.

Back to Sam Buss's publications page.