Journal or Publication Title:

Математические вопросы кибернетики и вычислительной техники=Կիբեռնետիկայի և հաշվողական տեխնիկայի մաթեմատիկական հարցեր=Mathematical problems of computer science

Date of publication:

2023

Number:

59

ISSN:

2579-2784 ; e-2538-2788

Additional Information:

Թամազյան Հակոբ Ա., Тамазян Акоб А.

Other title:

Գծային արտածումների բարդությունների կապը ծավալիչներով սեկվենցիալ համակարգում և տեղադրման կանոնով Ֆրեգեի համակարգերում ; Связь между сложностям и доказательств линейных выводов в системе секвенциального исчисления с кванторами и системах Фреге с правилом подстановки

Corporate Creators:

Yerevan State University

Coverage:

27-34

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.
Նախկինում ապացուցվել է, որ ծավալիչներով սեկվենցիալ համակարգում առկա է քայլերի քանակի էքսպոնենցիալ արագացում տեղադրման կանոնով Ֆրեգեի համակարգերի նկատմամբ, երբ դիտարկում ենք ծառային արտածումները: Այս հոդվածը ցույց է տալիս, որ առանց ծավալիչների, ցանկացած նույնաբանության գծային արտածումը ծավալիչներով սեկվենցիալ համակարգում հնարավոր է վերածել նույն նույնաբանության գծային արտածման տեղադրման կանոնով Ֆրեգեի համակարգերում` ունենալով արտածման քայլերի քանակի և երկարության առավելագույն բազմանդամային աճ:
Ранее было доказано, что существует экспоненциальное ускорение количества шагов в системе секвенциального исчисления высказываний с кванторами по сравнению с системами Фреге с правилом подстановки, когда мы рассматриваем выводы в виде деревьев. Эта статья показывает, что линейный вывод любой бескванторной тавтологии в системе секвенциального исчисления высказываний с кванторами можно превратить в линейный вывод той же тавтологии в системах Фреге с правилом подстановки с не более чем полиномиально возрастающим количеством шагов и длиной вывода.

Publisher:

Изд-во НАН РА

Format:

pdf

Identifier:

oai:arar.sci.am:366984

Location of original object:

ՀՀ ԳԱԱ Հիմնարար գիտական գրադարան