Journal article:

    Samuel R. Buss and Gyorgy Turán.
    "Resolution proofs of generalized pigeonhole principles."
    Theoretical Computer Science 62 (1988) 311-317.

    Download article: postscript or PDF

    Abstract: We extend results of A. Haken to give an exponential lower bound on the size of resolution proofs for propositional formulas encoding a generalized pigeonhole principle. These propositional formulas express the fact that there is no one-one mapping from  cn  objects to n objects when c > 1. As a corollary, resolution proof systems do not p-simulate constant formula depth Frege proof systems.

Back to Sam Buss's publications page.