omparison of the Complexities in Frege Proofs with Different Substitution Rules
We compare the proof complexities in Frege systems with multiple substitution rule and with constant bounded substitution rule. We prove that any two constant bounded substitution Frege systems are polynomially equivalent both by size and by steps. Frege system with multiple substitution rule and Frege system with constant bounded substitution rule are also polynomially equivalent by size, but the first system has exponential speed-up over the second system by steps.
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, vol. 8, pp. 57-64,1975.
A.A. Chubaryan, The complexity in Frege Proofs with substitution, Mathem. Problems of Computer Science, NAN, Armenia, vol. 22, pp. 7-11, 2001.
How to Cite
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.