Conference proceedings article:
Maria Luisa Bonet and Samuel R. Buss.
"On the deduction rule and the number of proof lines."
In Proceedings of the Sixth Annual IEEE Symposium
on Logic in Computer Science. (LICS'91). IEEE Computer Society Press, 1991, pp.
286-297.
Subsequent journal papers that subsume this conference paper:
Download conference article: postscript or PDF.
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 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(\alpha(n))$ where $\alpha$ is the inverse Ackermann function. A nested
deduction Frege system can linearly simulate the propositional sequent calculus and hence
a Frege proof system can simulate the propositional sequent calculus with proof lengths
bounded by $O(n\cdot\alpha(n))$.
As a technical tool, we introduce the serial transitive closure
problem: given a directed graph and a list of {\em closure edges} in the transitive
closure of the graph, the problem is to derive all the closure edges. We give a nearly
linear bound on the number of steps in such a derivation when the graph is tree-like.