Number of Symbols in Frege Proofs with and without the Deduction Rule
Marı́a Luisa Bonet · 1993
Abstract Abstract Frege systems with the deduction rule produce at most quadratic speedup over .F’rege systems using as a measure of length the number of symbols in the proof. We study whether that speedup is in reality smaller. We show that the speedup is linear when the Frege proofs are tree-like. Also, two groups of formulas, permutation formulas and transitive closure formulas, that seemed most likely to produce an almost quadratic speedup when using the deduction rule, are shown to produce only log n and log2n factors respectively.