Sciweavers

Share
LICS
1991
IEEE

On the Deduction Rule and the Number of Proof Lines

9 years 10 months ago
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...
Maria Luisa Bonet, Samuel R. Buss
Added 27 Aug 2010
Updated 27 Aug 2010
Type Conference
Year 1991
Where LICS
Authors Maria Luisa Bonet, Samuel R. Buss
Comments (0)
books