Polynomial Size Proofs of the Propositional Pigeonhole Principle
Buss, Samuel R.
J. Symbolic Logic, Tome 52 (1987) no. 1, p. 916-927 / Harvested from Project Euclid
Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.
Publié le : 1987-12-14
Classification: 
@article{1183742501,
     author = {Buss, Samuel R.},
     title = {Polynomial Size Proofs of the Propositional Pigeonhole Principle},
     journal = {J. Symbolic Logic},
     volume = {52},
     number = {1},
     year = {1987},
     pages = { 916-927},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183742501}
}
Buss, Samuel R. Polynomial Size Proofs of the Propositional Pigeonhole Principle. J. Symbolic Logic, Tome 52 (1987) no. 1, pp.  916-927. http://gdmltest.u-ga.fr/item/1183742501/