Journal of Symbolic Logic 58 (2):688-709 (1993)
|Abstract||We 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 (or formulas) 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(α(n)) 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(n · α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). 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(n log n)|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Dov M. Gabbay & Nicola Olivetti (1998). Algorithmic Proof Methods and Cut Elimination for Implicational Logics Part I: Modal Implication. Studia Logica 61 (2):237-280.
Andrzej Indrzejczak (2003). A Labelled Natural Deduction System for Linear Temporal Logic. Studia Logica 75 (3):345 - 376.
Ivan Welty (2011). Frege on Indirect Proof. History and Philosophy of Logic 32 (3):283-290.
Maria Bonet, Toniann Pitassi & Ran Raz (1997). Lower Bounds for Cutting Planes Proofs with Small Coefficients. Journal of Symbolic Logic 62 (3):708-728.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Wendy MacCaull & Ewa Orłlowska (2002). Correspondence Results for Relational Proof Systems with Application to the Lambek Calculus. Studia Logica 71 (3):389-414.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Sara Negri (2011). Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press.
Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi (2001). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. Journal of Symbolic Logic 66 (1):171-191.
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #291,125 of 722,745 )
Recent downloads (6 months)0
How can I increase my downloads?