D:\User\sbornik_38_pdf\19.DVI


Mathematical Problems of Computer Science 38, 44{45, 2012.

Some N ew P r opositional P r oof Systems for

I ntuitionistic and M inimal Logics

A n a h it Ch u b a r ya n , S e r g e y S a ya d ya n

Department of Informatics and Applied Mathematics, Yerevan State University, Armenia
achubaryan@ysu.am, sayadyan@gmail.com

On e o f t h e m o s t fu n d a m e n t a l p r o b le m s o f t h e p r o o f c o m p le xit y t h e o r y is t o ¯ n d a n e ± -
c ie n t p r o o f s ys t e m fo r p r o p o s it io n a l c a lc u lu s . Th e in ve s t ig a t io n s o f p r o o f c o m p le xit y s t a r t fo r
t h e s ys t e m s o f Cla s s ic a l P r o p o s it io n a l L o g ic ( CP L ) . H o we ve r , n a t u r a l r e a l c o n c lu s io n s h a ve
c o n s t r u c t ive c h a r a c t e r in m o s t c a s e s . Th e r e fo r e t h e in ve s t ig a t io n o f t h e p r o o fs c o m p le xit ie s
is im p o r t a n t fo r s ys t e m s o f In t u it io n is t ic P r o p o s it io n a l L o g ic ( IP L ) a n d in s o m e c a s e s a ls o
fo r Min im a l ( Jo h a n s s o n 's ) P r o p o s it io n a l L o g ic ( MP L ) .

Ma n y o f t h e 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 u s e p r e s e n t a t io n o f t a u t o lo g ie s
o r c o n t r a d ic t io n s in d is ju n c t ive n o r m a l fo r m s ( D N F) o r in c o n ju n c t ive n o r m a l fo r m s ( CN F) ,
b u t s u c h p r e s e n t a t io n s fo r n o n -c la s s ic a l t a u t o lo g ie s a r e n o t e n t ir e ly c o r r e c t .

B y a n a lo g y wit h t h e n o t io n s o f d e t e r m in a t ive c o n ju n c t s a n d d e t e r m in a t ive D N F, g ive n
in [1 ] fo r c la s s ic a l t a u t o lo g ie s , we in t r o d u c e t h e s a m e n o t io n s fo r n o n -c la s s ic a l t a u t o lo g ie s
a n d g ive t h e a lg o r it h m s fo r c o n s t r u c t io n o f I-d e t e r m in a t ive D N F a n d M-d e t e r m in a t ive D N F
fo r in t u it io n is t ic a n d m in im a l t a u t o lo g ie s a c c o r d in g ly [2 ].

On t h e b a s e o f in t r o d u c e d n o n -c la s s ic a l d e t e r m in a t ive D N F we c a n d e ¯ n e fo r IP L a n d
MP L t h e a n a lo g ie s o f we ll-kn o wn c la s s ic a l p r o o f s ys t e m s R e s ( k) , R ( lin ) , Cu t t in g P la n n e s
( CP ) , wic h a r e d i®e r e n t g e n e r a liz a t io n s o f r e s o lu t io n s ys t e m R .

W e d e n o t e t h e in t r o d u c e d s ys t e m s b y IR e s ( k) , IR ( lin ) , ICP a n d MR e s ( k) , MR ( lin ) , MCP
fo r IP L a n d MP L a c c o r d in g ly.

To c o m p a r e t h e e ± c ie n c ie s o f in t r o d u c e d s ys t e m s wit h t h e kn o wn n o n -c la s s ic a l r e s o lu t io n
s ys t e m s IR a n d MR we u s e t h e we ll-kn o wn n o t io n o f e xp o n e n t ia l s p e e d -u p fr o m [3 ].

M ain T heor em

1 . Th e s ys t e m s IR e s ( k) , IR ( lin ) , ICP h a ve e xp o n e n t ia l s p e e d -u p o ve r t h e s ys t e m IR .
2 . Th e s ys t e m s MR e s ( k) , MR ( lin ) , MCP h a ve e xp o n e n t ia l s p e e d -u p o ve r t h e s ys t e m MR .

Acknowledgment. Th is wo r k is s u p p o r t e d b y Gr a n t 1 1 -1 b 0 2 3 o f S S C o f Go ve r m e n t o f
A r m e n ia .

4 4



A. Chubaryan, S. Sayadyan 4 5

R e fe r e n c e s

[1 ] A n . Ch u b a r ya n , A r m . Ch u b a r ya n , A n e w c o n c e p t io n o f e qu a lit y o f t a u t o lo g ie s , L &P S ,
V o l.V , N o 1 , Tr ie s t , It a ly, 2 0 0 7 , 3 -8 .

[2 ] A n . 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 , S . S a ya d ya n , A h ie r a r c h y o f r e s o lu t io n
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 , Co m p u t e r Te c h n o lg y a n d A p p lic a t io n 3 , D a vid
P u b lis h in g , U S A , 2 0 1 2 , 3 3 0 -3 3 6 .

[3 ] S . Co o k, 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 fs s ys t e m s , Jo u r n a l o f
S ym b o lic L o g ic , 4 4 , 1 9 7 9 , 3 6 -5 0 .