On the Deduction Rule and the Number of Proof Lines

d Abstract) Maria Luisa Bonet∗ Samuel R. Buss∗ Department of Mathematics Department of Mathematics U.C. Berkeley U.C. San Diego Berkeley, California 94720 La Jolla, California 92093 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 these systems compared to lengths in Frege proof systems. As an application we give a near-linear simulation of the propositional Gentzen sequent calculus by Frege proofs. The length of a proof is the number of steps or 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(α(n)) where α is the inverse Acker...

• Type: Conference
• Year: 1991
• Where: LICS
• Authors: Maria Luisa Bonet, Samuel R. Buss
• Keywords: Automated Reasoning, Deduction Frege, Frege, Frege Proof, LICS 1991