It is well known that coset-generating relations lead to tractable
constraint satisfaction problems. These are precisely the relations closed
under the operation $xy^{-1}z$ where the multiplication is taken in
some finite group. Bulatov et al. have on the other hand shown that
any clone containing the multiplication of some ``block-group'' ... more >>>

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 ... more >>>