Go to the content (press return)

# FUTUR. Website for the scientific production of UPC researchers

## Monotone Proofs of the Pigeon Hole Principle

Author
Galesi, N.; Atserias, A.; Gavaldà, R.
Type of activity
Journal article
Journal
Electronic colloquium on computational complexity
Date of publication
2000-02
Number
TR00-008
First page
1
Last page
13
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 Resoluti...
Keywords
Monotone Calculus, Proof Complexity, Threshold Functions, pigeon hole principle
Group of research
ALBCOM - Algorithms, Computational Biology, Complexity and Formal Methods
LARCA - Laboratory of Relational Algorithmics, Complexity and Learnability
LOGPROG - Logic and Programming