Journal of Symbolic Logic 58 (2):688-709 (1993)
AbstractWe introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O.
Added to PP
Historical graph of downloads
References found in this work
Citations of this work
Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
On the Correspondence Between Arithmetic Theories and Propositional Proof Systems - a Survey.Olaf Beyersdorff - 2009 - Mathematical Logic Quarterly 55 (2):116-137.
Lower Complexity Bounds in Justification Logic.Samuel R. Buss & Roman Kuznets - 2012 - Annals of Pure and Applied Logic 163 (7):888-905.
Generalisation of Proof Simulation Procedures for Frege Systems by M.L. Bonet and S.R. Buss.Daniil Kozhemiachenko - 2018 - Journal of Applied Non-Classical Logics 28 (4):389-413.
Similar books and articles
Algorithmic Proof Methods and Cut Elimination for Implicational Logics Part I: Modal Implication.Dov M. Gabbay & Nicola Olivetti - 1998 - Studia Logica 61 (2):237-280.
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.
Correspondence Results for Relational Proof Systems with Application to the Lambek Calculus.Wendy MacCaull & Ewa Orłlowska - 2002 - Studia Logica 71 (3):389-414.
Lower Bounds for Cutting Planes Proofs with Small Coefficients.Maria Bonet, Toniann Pitassi & Ran Raz - 1997 - Journal of Symbolic Logic 62 (3):708-728.
A Labelled Natural Deduction System for Linear Temporal Logic.Andrzej Indrzejczak - 2003 - Studia Logica 75 (3):345 - 376.