Name
Abstract | ||
|---|---|---|
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 clique-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ák. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1002/1521-3870(200111)47:4<461::AID-MALQ461>3.0.CO;2-B | Electronic Colloquium on Computational Complexity (ECCC) |
Keywords | Field | DocType |
quasipolynomial-size monotone proof,pigeon hole principle,monotone proofs,monotone variant,monotone gentzen calculus,gentzen calculus,monotone proof,bounded depth frege,certain quasipolynomial-size monotone formula,quasipolynomial-size proof,intuitionistic gentzen calculus,monotone sequent,proof complexity,pigeonhole principle | Discrete mathematics,Bernstein's theorem on monotone functions,Combinatorics,Algebra,Mathematical proof,Proof complexity,Mathematics,Monotone polygon,Pigeonhole principle | Journal |
Volume | Issue | ISSN |
47 | 4 | 0302-9743 |
ISBN | Citations | PageRank |
3-540-67715-1 | 4 | 0.48 |
References | Authors | |
30 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Albert Atserias | 1 | 419 | 32.76 |
| Nicola Galesi | 2 | 367 | 28.05 |
| Ricard Gavaldà | 3 | 1265 | 81.30 |