- G. S. Tseitin, "On the complexity of derivation in propositional calculus".
Studies in Mathematics and Mathematical Logic , Part II, A. O. Slisenko, ed. (Translated from Russian).Google Scholar - S. A. Cook, "Feasibly constructive proofs and the propositional calculus". Preliminary Version. Proceedings 7th Annual ACM STOC, May, 1975, pp. 83--97. Google ScholarDigital Library
Index Terms
- A short proof of the pigeon hole principle using extended resolution
Recommendations
Monotone Proofs of the Pigeon Hole Principle
ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and ProgrammingWe study the complexity of proving the Pigeon Hole Principle (PHP) in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We show that the standard encoding of the PHP as a monotone sequent admits quasipolynomial-size proofs in ...
Resolution Width-Size Trade-offs for the Pigeon-Hole Principle
CCC '02: Proceedings of the 17th IEEE Annual Conference on Computational ComplexityWe prove the following two results: (1) There is a resolution proof of the Weak Pigeon-Hole Principle, \( WPHP_{n}^{m} \) of size \( 2^{O\left( \frac{n\log n}{\log m}+\log m\right) } \) for any number of pigeons \( m \) and any number of holes \( n \). (...
A direct construction of polynomial-size OBDD proof of pigeon hole problem
Viewing OBDD from the explicit perspective of a propositional proof system is first proposed and studied in [A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77-91]. It has been shown that OBDD proof ...
Comments