On small-depth Frege proofs for PHP
On small-depth Frege proofs for PHP
We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined on the $n \times n$ grid where n is odd. We are interested in the case where each formula in the proof is a depth d formula in the basis given by $\wedge, \vee$, and $\neg$. We prove …