The Relationship Between the Proof Complexities of Linear Proofs in Quantified Sequent Calculus and Substitution Frege Systems
DOI:
https://doi.org/10.51408/1963-0099Keywords:
Sequent systems, Frege systems, Proof size, Number of proof lines, Exponential speed-upAbstract
It has formerly been proved that there is an exponential speed-up in the number of lines of the quantified propositional sequent calculus over substitution Frege systems when considering proofs as trees. This paper shows that a linear proof of any quantifierfree tautology in quantified propositional sequent calculus can be transformed into a linear proof of the same tautology in a substitution Frege systems with no more than polynomially increasing proof lines and size.
References
S. A. Cook and A. R. Reckhow, “The relative efficiency of propositional proof systems”, Symbolic Logic, vol. 44, pp. 36–50, 1979.
A. Carbone, “Quantified propositional logic and the number of lines of tree-like proofs”, Studia Logica, vol. 64, pp. 315–321, 2000.
H. A. Tamazyan and A. A. Chubaryan, “On proof complexities relations in some systems of propositional calculus, Mathematical Problems of Computer Science, vol. 54, pp. 138–146, 2020.
L. A. Apinyan and A. A Chubaryan, “On sizes of linear and tree-like proofs for any formulae families in some systems of propositional calculus”, Mathematical Problems of Computer Science, vol. 57, pp. 47–55, 2022.
P. Pudlák, The Lengths of Proofs, in S. Buss (ed.), Handbook of Proof Theory, Elsevier, vol. 137, pp. 547-637, 1998.
J. Krajíček, Proof Complexity, Encyclopedia of Mathematics and Its Applications, Cambridge University Press, vol. 170, 2019.
G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen, vol. 112, pp. 493–565, 1936.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2023 Hakob A. Tamazyan
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
