D:\User\sbornik_38_pdf\41.DVI
Mathematical Problems of Computer Science 38, 95{96, 2012.
On the H ier ar chies of Some P r opositional Systems for
Classical and N on-classical Logics ¤
A n a h it Ch u b a r ya n
Department of Informatics and Applied Mathematics,
Yerevan State University, Armenia
achubaryan@ysu.am
Th e fa m ilie s o f e lim in a t io n s ys t e m s wit h fu ll s u b s t it u t io n r u le a n d 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 a r e in t r o d u c e d fo r Cla s s ic a l, In t u it io n is t ic a n d Min im a l ( Io h a n s s o n 's ) p r o p o -
s it io n a l lo g ic s ( CP L , IP L ,MP L ) , a n d 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 a r e c o m p a r e d fo r
e ve r y m e n t io n e d lo g ic .
W e u s e 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 a n d d e t e r m in a t ive n o r m a l fo r m s , in t r o d u c e d
fo r CP L in [1 ], fo r IP L a n d MP L in [2 ].
L e t ' b e a p r o p o s it io n a l fo r m u la , P = fp1; p2; : : : ; png b e t h e s e t o f a ll va r ia b le s o f ',
a n d P 0 = fpi1; pi2 ; : : : ; pimg ( 1 · m · n) b e s o m e s u b s e t o f P .
De¯nition 1. Given ¾ = f¾1; : : : ; ¾mg ½ Em (unit B oolean cube), the conjunct K¾ =
fp¾1i1 ; p
¾2
i2
; : : : ; p¾mim g is called ' ¡ 1 -determinative (' ¡ 0 -determinative) if assigning ¾j ( 1 ·
j · m) to each pij we obtain the value of ' (1 or 0) independently of the values of the
remaining variables.
De¯nition 2. D NF D = fK1; K2; : : : ; Krg is called determinative D NF
(dD NF ) for ' if ' = D and every conjunct Ki ( 1 · i · r ) is 1-determinative for '.
Th e in ve s t ig a t e d s ys t e m s a r e t h e fo llo win g s ys t e m s E C, E I a n d E M a n d t h e ir g e n e r a l-
iz a t io n s . Th e a xio m s o f EC a r e n o t ¯ xe d , b u t fo r e ve r y fo r m u la ' e a c h c o n ju n c t fr o m s o m e
d D N F o f ' c a n b e c o n s id e r e d a s a n a xio m .
Th e elimination rule ( "-r u le ) in fe r s K0 [ K00 fr o m c o n ju n c t s K0 [fpg a n d K0 [fpg, wh e r e
K0 a n d K00 a r e c o n ju n c t s a n d p is a va r ia b le .
D N F D = fK1; K2; : : : ; Klg is c a lle d fu ll ( t a u t o lo g y) if u s in g "-r u le c a n b e p r o ve d t h e
e m p t y c o n ju n c t io n ( ;) fr o m t h e a xio m s fK1; K2; : : : ; Klg.
Th e a n a lo g ie s o f t h e d e t e r m in a t ive c o n ju n c t s a n d d D N F fo r IP L a n d MP L ( I-d D N F a n d
M-d D N F a c c o r d in g ly ) a r e c o n s t r u c t e d in [2 ]. N o t e t h a t t h e lit e r a ls in t h e la t t e r c o n ju n c t s
a r e o n ly va r ia b le s wit h n e g a t io n o r wit h d o u b le n e g a t io n s .
B y a n a lo g y t h e c o r r e s p o n d in g p r o o f s ys t e m EI ( EM ) c a n b e c o n s t r u c t e d fo r IP L ( MP L ) .
A s a xio m is c o n s id e r e d e ve r y I-d e t e r m in a t ive ( M -d e t e r m in a t ive ) c o n ju n c t fr o m s o m e
I-d e t e r m in a t ive ( M-d e t e r m in a t ive ) DNF .
¤This work is supported by Grant 11-1b023 of SSC of Goverment of Armenia.
9 5
9 6 On the Hierarchies of Some Propositional Systems for Classical and Non-classical Logics
Fo r EI ( EM ) we t a ke t h e fo llo win g in fe r e n c e r u le
K0 [ p K00 [ p
K0 [ K00 I² ¡ rule
Ã
K0 [ ( p ¾ ? ) ¾ ? K00 [ ( p ¾ ? )
K0 [ K00 M² ¡ rule
!
;
wh e r e K0 a n d K00 a r e c o n ju n c t s a n d p is a va r ia b le . L e t u s in t r o d u c e t h e s u b s t it u t io n r u le
fo r t h e s e t o f c o n ju n c t s C a s fo llo win g
C
S ( C ) Ap
;
wh e r e S ( C ) Ap d e n o t e s t h e s e t o f r e s u lt s o f s u b s t it u t io n o f fo r m u la A in s t e a d o f va r ia b le p
e ve r ywh e r e in t h e c o n ju n c t s o f t h e s e t C , a n d t h e r e fo r e we h a ve t h e generalized e lim in a t io n
r u le fo r a fo r m u la A
C1 [ fAg C2 [ fAg
C1 [ C2
; wh e r e A is a lit e r a l o r o n a n y s t e p s u b s t it u t e d fo r m u la :
B y SEC we d e n o t e t h e s ys t e m E C wit h s u b s t it u t io n r u le a n d g e n e r a liz e d e lim in a t io n r u le .
If t h e n u m b e r o f c o n n e c t ive s o f s u b s t it u t e d fo r m u la s is b o u n d e d b y `, t h e n t h e c o r r e s p o n d in g
s ys t e m is d e n o t e d b y S`EC.
Th e s ys t e m s SEI, SEM, S`EI, S`EM a r e d e ¯ n e d b y a n a lo g y o n t h e b a s e o f t h e s ys t e m s
E I a n d E M, u s in g t h e c o r r e s p o n d in g g e n e r a liz e d e lim in a t io n r u le s .
W e d e ¯ n e t h e c o m p le xit y t o b e t h e s iz e o f a p r o o f ( = t h e t o t a l n u m b e r o f s ym b o ls ) .
Th e m in im a l c o m p le xit y o f a fo r m u la ' ( o r it s r e p r e s e n t a t io n ) in a p r o o f s ys t e m © we
d e n o t e b y l©' .
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 we u s e t h e we ll-kn o wn n o t io n s o f p -
s im u la t io n , p -e qu iva le n c e a n d e xp o n e n t ia l s p e e d -u p fr o m [3 ].
W e u s e a ls o t h e we ll-kn o wn n o t io n s o f Fr e g e s ys t e m s FC, FI a n d FM fo r CP L , IP L a n d
MP L a c c o r d in g ly ( s e e fo r e xa m p le in [2 ]) .
M ain T heor em
1 . Fo r e ve r y l > 0 t h e s ys t e m S`+1EC ( S`+1EI, S`+1EM ) h a s 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 S`EC ( S`EI, S`EM ) in t r e e fo r m .
2 . Th e s ys t e m s SEC ( SEI, SEM ) a n d FC ( FI, FM) a r e p -e qu iva le n t .
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 .