期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2000
卷号：2000
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We show that an LK proof of size m of a monotone sequent (a sequent
that contains only formulas in the basis ) can be turned
into a proof containing only monotone formulas of size mO(logm)
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
