Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR00-087 | 14th November 2000 00:00

#### Monotone simulations of nonmonotone propositional proofs

TR00-087
Authors: Albert Atserias, Nicola Galesi, Pavel Pudlak
Publication: 15th November 2000 09:36
Keywords:

Abstract:

We show that an LK proof of size \$m\$ of a monotone sequent (a sequent

that contains only formulas in the basis \$\wedge,\vee\$) can be turned

into a proof containing only monotone formulas of size \$m^{O(\log m)}\$

and with the number of proof lines polynomial in \$m\$. Also we show

that some interesting special cases, namely the functional and the

onto versions of PHP and a version of the Matching Principle, have

polynomial size monotone proofs.

ISSN 1433-8092 | Imprint