Studia Logica 64 (3):315-321 (2000)
AbstractThere is an exponential speed-up in the number of lines of the quantified propositional sequent calculus over Substitution Frege Systems, if one considers proofs as trees. Whether this is true also for the number of symbols, is still an open problem.
Similar books and articles
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
Bounded Arithmetic, Propositional Logic and Complexity Theory.Jan Krajíček - 1995 - Cambridge University Press.
Polynomial Size Proofs of the Propositional Pigeonhole Principle.Samuel R. Buss - 1987 - Journal of Symbolic Logic 52 (4):916-927.
Decidability of Quantified Propositional Intuitionistic Logic and S4 on Trees of Height and Arity ≤Ω.Richard Zach - 2004 - Journal of Philosophical Logic 33 (2):155-164.
Added to PP
Historical graph of downloads