@misc{Tamazyan_Hakob_A._The,
 author={Tamazyan, Hakob A.},
 howpublished={online},
 publisher={Изд-во НАН РА},
 abstract={It has formerly been proved that there is an exponential speed-up in the number oflines of the quantified propositional sequent calculus over substitution Frege systemswhen considering proofs as trees. This paper shows that a linear proof of any quantifier-free tautology in quantified propositional sequent calculus can be transformed into alinear proof of the same tautology in a substitution Frege systems with no more thanpolynomially increasing proof lines and size. Նախկինում ապացուցվել է, որ ծավալիչներով սեկվենցիալ համակարգում առկա է քայլերի քանակի էքսպոնենցիալ արագացում տեղադրման կանոնով Ֆրեգեի համակարգերի նկատմամբ, երբ դիտարկում ենք ծառային արտածումները: Այս հոդվածը ցույց է տալիս, որ առանց ծավալիչների, ցանկացած նույնաբանության գծային արտածումը ծավալիչներով սեկվենցիալ համակարգում հնարավոր է վերածել նույն նույնաբանության գծային արտածման տեղադրման կանոնով Ֆրեգեի համակարգերում` ունենալով արտածման քայլերի քանակի և երկարության առավելագույն բազմանդամային աճ: Ранее было доказано, что существует экспоненциальное ускорение количества шагов в системе секвенциального исчисления высказываний с кванторами по сравнению с системами Фреге с правилом подстановки, когда мы рассматриваем выводы в виде деревьев. Эта статья показывает, что линейный вывод любой бескванторной тавтологии в системе секвенциального исчисления высказываний с кванторами можно превратить в линейный вывод той же тавтологии в системах Фреге с правилом подстановки с не более чем полиномиально возрастающим количеством шагов и длиной вывода.},
 type={Հոդված},
 title={The Relationship Between the Proof Complexities of Linear Proofs in Quantified Sequent Calculus and Substitution Frege Systems},
 keywords={Mathematical cybernetics, Computer science},
}