D:\sbornik\...\Chubaryan4.DVI


Mathematical Problems of Computer Science 30, 36{39, 2008.

Compar ison of the Complexities in Fr ege P r oofs

with Di®er ent Substitution Rules

A n a h it A . Ch u b a r ya n , A r m in e A . Ch u b a r ya n , S o n a R . A le ks a n ya n

Department of Informatics and Applied Mathematics, Yerevan State University
Department of Applied Mathematics, State Engineering University of Armenia

E-mails: achubaryan@ysu.am, chubarm@ysu.am, sonush@rambler.ru

Abstract

We compare the proof complexities in Frege systems with multiple substitution
rule and with constant bounded substitution rule. We prove that any two constant
bounded substitution Frege systems are polynomially equivalent both by size and by
steps. Frege system with multiple substitution rule and Frege system with constant
bounded substitution rule are also polynomially equivalent by size, but the ¯rst system
has exponential speed-up over the second system by steps.

Refer ences

[1 ] S . A . Co o k, A . R . R e c kh o w, Th e r e la t ive e ± c ie n c y o f p r o p o s it io n a l p r o o f s ys t e m s " ,
J ournal of Symbolic L ogic, vo l. 4 4 , p p . 3 6 { 5 0 , 1 9 7 9 .

[2 ] G. Ce jt in , A . Ch u b a r ya n , On s o m e b o u n d s t o t h e le n g t h s o f lo g ic a l p r o o fs in c la s s ic a l
p r o p o s it io n a l c a lc u lu s " , ( in R u s s ia n ) , Trudy Vycisl.Centra AN Arm SSR i Yerevan Univ.,
vo l. 8 , p p . 5 7 { 6 4 , 1 9 7 5 .

[3 ] A . A . Ch u b a r ya n , Th e c o m p le xit y in Fr e g e P r o o fs wit h s u b s t it u t io n " , M athem. P roblems
of Computer Science, NAN, Armenia, vo l. 2 2 , p p . 7 { 1 1 , 2 0 0 1 .

²ñï³ÍáõÙÝ»ñÇ µ³ñ¹áõÃÛáõÝÝ»ñÇ Ñ³Ù»Ù³ïáõÙÁ ï³ñµ»ñ
ï»Õ³¹ñÙ³Ý Ï³ÝáÝÝ»ñáí üñ»·»Ç ѳٳϳñ·áõÙ

², âáõµ³ñÛ³Ý, ². âáõµ³ñÛ³Ý, ê. ²É»ùë³ÝÛ³Ý

²Ù÷á÷áõÙ

²ß˳ï³Ýùáõ٠ѳٻٳïíáõÙ »Ý Áëï ³ñï³ÍáõÙÝ»ñÇ »ñÏáõ µ³ñ¹áõÃÛ³Ý µÝáõó·ñÇãÝ»ñÇ
(»ñϳñáõÃÛáõÝ ¨ ù³ÛÉ»ñÇ ù³Ý³Ï) üñ»·»Ç ѳٳϳñ·Ç µ³½Ù³ÏÇ ï»Õ³¹ñÙ³Ý ¨
ë³Ñٳݳ÷³Ï ï»Õ³¹ñÙ³Ý Ï³ÝáÝÝáí »ñÏáõ ÁݹɳÛÝáõÙÝ»ñ: ²å³óáõóí³Í ¿, áñ Áëï
³ñï³ÍÙ³Ý »ñϳñáõÃÛ³Ý µ³½Ù³ÏÇ ¨ ë³Ñٳݳ÷³Ï ï»Õ³¹ñÙ³Ý Ï³ÝáÝÝ»ñáí üñ»·»Ç
ѳٳϳñ·»ñÁ µ³½Ù³Ý¹³Ùáñ»Ý ѳٳñÅ»ù »Ý, ë³Ï³ÛÝ Áëï ù³ÛÉ»ñÇ ù³Ý³ÏÇ µ³½Ù³ÏÇ
ï»Õ³¹ñÙ³Ý Ï³ÝáÝáí üñ»·»Ç ѳٳϳñ·Ý áõÝÇ óáõóã³ÛÇÝ ³ñ³·³óáõÙ ë³Ñٳݳ÷³Ï
ï»Õ³¹ñٳٵ üñ»·»Ç ѳٳϳñ·»ñÇ Ýϳïٳٵ:

3 6