A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover–Delayer games

In this note we show that the asymmetric Prover–Delayer game developed in Beyersdorff et al. (2010) [2] for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover–Delayer game to show a lower bound of the form 2Ω(nlogn)2Ω(nlogn) for the pigeonhole principle in tree-like Resolution. This gives a new and simpler proof of the same lower bound established by Iwama and Miyazaki (1999) [7] and Dantchev and Riis (2001) [5].

Research highlights► New asymmetric Prover–Delayer game for lower bounds in free-like proof systems. ► Refines the Prover–Delayer Game of Pudlak and Impagliazzo. ► New simple proof of the optimal lower bound for the pigeonhole principle.