D:\sbornik\...\Efficiency.DVI


Mathematical Problems of Computer Science 33, 5{10, 2010.

E ±ciency of Depth-Restr icted Substitution Rules

H a ko b N a lb a n d ya n

Institute for Informatics and Automation Problems of NAS of RA

e-mail: hakob nalbandyan@yahoo.com

Abstract

We compare the proof complexities in Frege systems with a substitution rule with-
out any restrictions and with depth-restricted substitution rule. We prove that Frege
system with well-known substitution rule and Frege system with depth-restricted sub-
stitution rule are 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.
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, vo l. 2 2 , p p . 7 { 1 1 , 2 0 0 1 .

[4 ] S . R . B u s s , \ S o m e r e m a r ks o n le n g t h s o f p r o p o s it io n a l p r o o fs " , Arch. M ath. L ogic, vo l.
3 4 ,p p . 3 7 7 -3 9 4 , 1 9 9 5 .

[5 ] A . A . Ch u b a r ya n , A r m . Ch u b a r ya n , H . N a lb a n d ya n , \ Co m p a r is o n o f t h e E ± c ie n c y o f
Fr e g e S ys t e m s wit h R e s t r ic t e d S u b s t it u t io n R u le s " , CS IT, Y e r e va n , p p . 3 1 -3 2 , 2 0 0 9 .

[6 ] A . A . Ch u b a r ya n , A r m . Ch u b a r ya n , H . N a lb a n d ya n , \ E ± c ie n c y o f we a k s u b s t it u t io n
r u le s " , E S M o f A S L , L C-0 9 , S o ¯ a , p . 3 7 .

5



6 E±ciency of Depth-Restricted Substitution Rules

ÊáñáõÃÛ³Ùµ ë³Ñٳݳ÷³Ï ï»Ë³¹ñÙ³Ý Ï³ÝáÝÝ»ñÇ
³ñ¹Ûáõݳí»ïáõÃÛáõÝÁ

Ð. ܳɵ³Ý¹Û³Ý

²Ù÷á÷áõÙ

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