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.