期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2000
卷号：2000
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We 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 this system. This result is a consequence of deriving the basic
properties of certain quasipolynomial-size monotone
formulas computing the boolean threshold functions.
Since it is known that the shortest proofs of the PHP in
systems such as Resolution or Bounded Depth Frege are exponentially
long, it follows from our result that these systems
are exponentially separated from the monotone Gentzen Calculus.
We also consider the monotone sequent (CLIQUE)
expressing the {\it clique}-{\it coclique} principle defined by
Bonet, Pitassi and Raz (1997).
We show that monotone proofs for this sequent can be easily
reduced to monotone proofs of the one-to-one and onto PHP, and so
CLIQUE also has quasipolynomial-size monotone proofs.
As a consequence, Cutting Planes with polynomially bounded coefficients is
also exponentially separated from the monotone Gentzen Calculus.
Finally, a simple simulation argument implies that
these results extend to the Intuitionistic Gentzen Calculus.
Our results partially answer some questions left open by P. Pudl\'ak.
