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