Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR00-087 | 14th November 2000 00:00

Monotone simulations of nonmonotone propositional proofs

RSS-Feed




TR00-087
Authors: Albert Atserias, Nicola Galesi, Pavel Pudlak
Publication: 15th November 2000 09:36
Downloads: 3723
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