We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis 4; 3) can be turned into a proof containing only monotone formulas of size mOð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 Pigeonhole Principle and a version of the Matching Principle, have polynomial size monotone proofs. We prove that LK is polynomially bounded if and only if its monotone fragment is.
Monotone Simulations of Nonmonotone Proofs / Atserias, A.; Galesi, Nicola; Pudlak, P.. - STAMPA. - 16:(2001), pp. 36-41. (Intervento presentato al convegno 16th Annual IEEE Conference on Computational Complexity tenutosi a Chicago, IL, USA) [10.1109/CCC.2001.933870].
Monotone Simulations of Nonmonotone Proofs.
GALESI, NICOLA
;
2001
Abstract
We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis 4; 3) can be turned into a proof containing only monotone formulas of size mOð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 Pigeonhole Principle and a version of the Matching Principle, have polynomial size monotone proofs. We prove that LK is polynomially bounded if and only if its monotone fragment is.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
