Upper and Lower bounds on Resolution for PHP and Ramsey
Resolution and the weak pigeonhole principle by Buss and Pitassi. 1996.
Improved resolution lower bounds for the weak pigeonhole principle by Razborov. 2001
Notes on Razborov's result on many pigeons by Jukna. 2011
Resolution lower bounds for the weak functional pigeonhole principle. 2003
The complexity of propositional proofs} by Nathan Segerlind
Read once programs, rectangular proofs of the pigeonhold principle and the traversal calculus by Razborov, Wigderson, Yao. 2002
A lower bound for the pigeonhole principle in tree-resolution by asymmetric prover-delayer games} by Beyerdorff, Galesi, Lauria. 2010
My Slides on the proof
A note on propositional proof complexity of some Ramsey type statements} by Krajicek. 2010
The strength of Ramsey theorem for coloring relatively large sets by Carlucci, Zdanoswki, Wyszynski
A lower bound on the size of resolution proofs of the Ramey theorem by Pudlak IPL, V 112, 2012, pages 610–611