@article{Tamazyan_2023, title={The Relationship Between the Proof Complexities of Linear Proofs in Quantified Sequent Calculus and Substitution Frege Systems}, volume={59}, url={http://mpcs.sci.am/index.php/mpcs/article/view/786}, DOI={10.51408/1963-0099}, abstractNote={<p>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.</p>}, journal={Mathematical Problems of Computer Science}, author={Tamazyan, Hakob A.}, year={2023}, month={May}, pages={27–34} }