Quadratic proofs of the pigeonhole formulas are presented using the connection method proof techniques. For this class of formulas exponential lower bounds are known for the length-of-resolution refutations. This indicates a significant difference in the power of these two proof techniques. While short proofs of these formulas are known using extended resolution, this particular proof technique, in contrast to both the connection method and resolution, seems not suitable for the actual proof search.
If you have any questions or comments regarding this page please send mail to firstname.lastname@example.org.