TY - JOUR
AU - Tamazyan, Hakob A.
PY - 2023/05/31
Y2 - 2024/05/21
TI - The Relationship Between the Proof Complexities of Linear Proofs in Quantified Sequent Calculus and Substitution Frege Systems
JF - Mathematical Problems of Computer Science
JA - MPCS
VL - 59
IS -
SE - Articles
DO - 10.51408/1963-0099
UR - http://mpcs.sci.am/index.php/mpcs/article/view/786
SP - 27-34
AB - <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>
ER -