TR00-008 Authors: Albert Atserias, Nicola Galesi, Ricard GavaldÃ

Publication: 11th February 2000 14:43

Downloads: 2101

Keywords:

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.