D:\sbornik\...\Sayadyan1.DVI Mathematical Problems of Computer Science 28, 2007, 135{140. Relative E ±ciency of N onclassical Resolution and Cut-fr ee Sequent System S e r g e y M. S a ya d ya n Department of Informatics and Applied Mathematics, Yerevan State University e-mail: sayadyans@yahoo.com Abstract Comparison of the e±ciency of resolution system and cut-free sequent calculus remains an open problem since 1974 (Cook, Reckhow). The problem was solved by A. Chubaryan for classical propositional logic in 2001. The paper proves that mentioned two systems for Intuitionistic propositional logic (Minimal propositional logic) are also polynomially equivalent. Refer ences [1 ] P . P u d l¶a k, Th e L e n g t h s o f P r o o fs , Handbook of proof theory, N o r t h -H o lla n d , 1 9 9 8 , 5 4 7 - 6 3 7 . [2 ] S . C. K le e n e , In t r o d u c t io n t o m e t a m a t h e m a t ic s , D . Van Nostrand Company, IN C, N e w Y o r k, 1 9 5 2 . [3 ] A n . Ch u b a r ya n , A r m . Ch u b a r ya n , S . S a ya d ya n , Th e r e la t ive o ± c ie n c y o f p r o p o s it io n a l p r o o fs s ys t e m s fo r c la s s ic a l a n d n o n c la s s ic a l lo g ic , F isrt conference of UNIL OG-05, H a n d - b o o k, Mo n t r e u x, 2 0 0 5 , 9 4 . [4 ] S . A . Co o k, A . R . R e c kh o w, 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 , JS L 4 4 , 1 , 1 9 7 9 , 3 6 -5 0 . [5 ] G. Min t s , R e s o lu t io n s ys t e m s fo r n o n c la s s ic a l lo g ic , Semiotika i informatika, vip . 2 5 , 1 9 8 5 , 1 2 0 -1 3 3 ( in R u s s ia n ) . [6 ] U . E g ly, S . S c h m it t , On In t u it io n is t ic P r o o f Tr a n s fo r m a t io n s , t h e ir Co m p le xit y, a n d A p - p lic a t io n t o Co n s t r u c t ive P r o g r a m S yn t h e s is , F orschungrbericht AID A-99-02, D a r m s t a d t , Ge r m a n y, 2 0 0 3 , 4 3 -6 8 . [7 ] H . B o lib e kya n , A . Ch u b a r ya n , On s o m e p r o o f s ys t e m s fo r I.Jo h a n s s o n 's m in im a l lo g ic o f p r e d ic a t e s , L ogic Colloquium 2003, H e ls in ki, Fin la n d , A u g . 1 4 -2 0 , 2 0 0 3 , A b s t r a c t s , p . 5 6 . [8 ] A . A . Ch u b a r ya n , R e la t ive e ± c ie n c y o f a p r o o f s ys t e m s o f c la s s ic a l p r o p o s it io n a l lo g ic , Izvestija Natsionalnoj Akademii Nauk Armenii, Ma t e m a t ic a , V o l. 3 7 , N 5 , 2 0 0 2 , 4 5 - 5 8 . [E n g lis h t r a n s la t io n : Jo r n a l o f Co n t e m p o r a r y Ma t h e m a t ic a l A n a lys is ( A r m e n ia n A c a d e m y o f S c ie n c e s ) , V o l. 3 7 , N 5 ]. 1 3 5 1 3 6 Relative E±ciency of Nonclassical Resolution and Cut-free Sequent System 軽áÉÛáõódzÛÇ ¨ ³é³Ýó ѳïáõÛÃÇ Ï³ÝáÝÇ ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·»ñÇ Ñ³ñ³µ»ñ³Ï³Ý ¿ýý»ÏïÇíáõÃÛáõÝÁ áã ¹³ë³Ï³Ý ³ëáõóÛÇÝ Ñ³ßíÇ Ñ³Ù³ñ ê. ê³Û³¹Û³Ý ²Ù÷á÷áõ٠軽áÉÛáõódzÛÇ Ñ³Ù³Ï³ñ·Ç ¨ ³é³Ýó ѳïáõÃÇ Ï³ÝáÝÇ ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·Ç ѳٻٳïáõÃÛáõÝÁ ÙÝáõÙ ¿ñ µ³ó ËݹÇñ ëÏë³Í 1974 Ã.-Çó (ÎáõÏ, è»Ëáí). ²Ûë ËݹÇñÁ ¹³ë³Ï³Ý ³ëáõóÛÇÝ Ñ³ßíÇ Ñ³Ù³ñ ÉáõÍí»É ¿ 2001 Ã.-ÇÝ ². âáõµ³ñÛ³ÝÇ ÏáÕÙÇó. êáõÛÝ Ñá¹í³ÍáõÙ ³å³óáõóí³Í ¿, áñ í»ñáÝßÛ³É »ñÏáõ ѳٳϳñ·»ñÁ ÆÝïáõÇóÇáÝÇëï³Ï³Ý ¨ ØÇÝÇÙ³É ³ëáõóÛÇÝ Ñ³ßÇíÝ»ñÇ Ñ³Ù³ñ ÝáõÛÝå»ë µ³½Ù³Ý¹³Ùáñ»Ý ѳٳñÅ»ù »Ý: