Efficiency of Depth-Restricted Substitution Rules
Hakob Nalbandyan · Mathematical Problems of Computer Science · 2010
We compare the proof complexities in Frege systems with a substitution rule without any restrictions and with depth-restricted substitution rule. We prove that Frege system with well-known substitution rule and Frege system with depth-restricted substitution rule are polynomially equivalent by size, but the first system has exponential speed-up over the second system by steps.