Relations between the Proof Complexities in Frege Systems, Deep-Inference Proof Systems KS and еКS - Chubaryan, A. A. (ՀՀ ԳԱԱ «Գիտություն» հրատ.)
Using the determinative sizes fօr tautologies of some sequences, it is proved in this paper that a Frege system and deep-inference proof system еКS exhibit an exponential speed-up over the deep-inference proof systems KS both by lines and size of proofs. Օգտագործելով որոշակի հաջորդականությունների նույնաբանությունների որոշիչ երկարությունները՝ ապացուցվել է, որ Ֆրեգեի համակարգերը և խորքային արտածման կանոններով еКS համակարգը ցուցաբերում են էքսպոնենցիալ արագացում խորքային արտածման կանոններով КS համակարգի նկատմամբ՝ և՛ ըստ արտածումների քայլերի, և՛ ըստ դրանց երկարությունների: Используя величины определяющих длин тавтологий некоторых последовательностей, доказано, что системы Фреге и система глубинных правил выводов еКS проявляют экспоненциальное ускорение относительно системы глубинных правил выводов КS как по шагам, так и по длинам выводов.
Keywords: Mathematics