Ամսագրի կամ հրապարակման վերնագիր:
Հրապարակման ամսաթիվ:
Համար:
ISSN:
Լրացուցիչ տեղեկություն:
Թամազյան Հակոբ Ա., Тамазян Акоб А.
Վերնագիր:
Այլ վերնագիր:
Գծային արտածումների բարդությունների կապը ծավալիչներով սեկվենցիալ համակարգում և տեղադրման կանոնով Ֆրեգեի համակարգերում ; Связь между сложностям и доказательств линейных выводов в системе секвенциального исчисления с кванторами и системах Фреге с правилом подстановки
Ստեղծողը:
Համատեղ հեղինակները:
Խորագիր:
Mathematical cybernetics ; Computer science
Չվերահսկվող բանալի բառեր:
Sequent system ; Frege system ; Proof siz ; Number of proof lines ; Ex-ponential speed-up.
Ծածկույթ:
Ամփոփում:
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.
Նախկինում ապացուցվել է, որ ծավալիչներով սեկվենցիալ համակարգում առկա է քայլերի քանակի էքսպոնենցիալ արագացում տեղադրման կանոնով Ֆրեգեի համակարգերի նկատմամբ, երբ դիտարկում ենք ծառային արտածումները: Այս հոդվածը ցույց է տալիս, որ առանց ծավալիչների, ցանկացած նույնաբանության գծային արտածումը ծավալիչներով սեկվենցիալ համակարգում հնարավոր է վերածել նույն նույնաբանության գծային արտածման տեղադրման կանոնով Ֆրեգեի համակարգերում` ունենալով արտածման քայլերի քանակի և երկարության առավելագույն բազմանդամային աճ:
Ранее было доказано, что существует экспоненциальное ускорение количества шагов в системе секвенциального исчисления высказываний с кванторами по сравнению с системами Фреге с правилом подстановки, когда мы рассматриваем выводы в виде деревьев. Эта статья показывает, что линейный вывод любой бескванторной тавтологии в системе секвенциального исчисления высказываний с кванторами можно превратить в линейный вывод той же тавтологии в системах Фреге с правилом подстановки с не более чем полиномиально возрастающим количеством шагов и длиной вывода.