Efficiency of Depth-Restricted Substitution Rules
Abstract
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.
References
S.A. Cook, A.R. Reckhow, “The relative efficiency of propositional proof systems", Journal of Symbolic Logic, vol. 44, pp. 36-50, 1979.
G. Cejtin, A. Chubaryan, “On some bounds to the lengths of logical proofs in classical propositional calculus", (in Russian), Trudy Vycisl. Centra AN Arm SSR i Yerevan Univ. 8, pp. 57-64, 1975.
A.A. Chubaryan, “The complexity in Frege Proofs with substitution", Mathem. Problems of Computer Science, vol. 22, pp. 7-11, 2001.
S.R. Buss, “Some remarks on lengths of propositional proofs", Arch. Math. Logic, vol. 34, pp. 377-394, 1995.
A.A. Chubaryan, Arm. Chubaryan, H. Nalbandyan, “Comparison of the Efficiency of Frege Systems with Restricted Substitution Rules", CSIT, Yerevan, pp. 31-32, 2009.
A.A. Chubaryan, Arm. Chubaryan, H. Nalbandyan, “Efficiency of weak substitution rules", ESM of ASL, LC-09, Sofia, p. 37.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
