（计算机应用技术专业论文）max（k）中公式改名的复杂性.pdf

， 摘要 对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。我 们对极小不可满足公式集感兴趣主要基于两方面的原因：一是大多数的消解难例 公式都是极小不可满足的；二是对于极小不可满足公式的深入理解，有助于我们 构造新的难例公式以及新的满足性算法。 一个c n f 公式，称为极小不可满足的( m u ) ，如果，是不可满足，并且在， 中删去任意一个子句后所得到的公式是可满足的。一个m u 中的公式f 称为最大 的，如果对于任意一个子句f f 且对于任意一个文字l ，工，将l 添加 到f 中，公式f 变为可满足的。最大的极小不可满足公式类记作m a x ， m a x ( k ) = m u ( k ) n m a x 公式f 的一个改名是一个定义在v a r ( f ) 上的函数p ，使 得对每个变元x ，武x ) s l x ，一x ) ；公式f 的一个变元改名是v a r ( f ) 上的个胃换； 公式f 的一个文字改名是一个变元改名和一个改名的组合。可以看出以上这三种 改名不改变公式的可满足性 ， 改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重 要作用。许道云教授已经证明：m v ( k ) 中的变元和文字改名都等价于图同构的判 定问题。众所周知，图同构的判定问题是n p 问题。近年来，人们一直寻找某些 极小不可满足公式的子类，使其变元和文字改名的判定问题可以在多项式时间内 完成。 在本文中，我们找到了一个能递归构造的极小不可满足公式的子类m a x + ， m a x + = f m a xij z v a r ( f ) v s p l i t t i n g s ( 只，e ：) ：e ，f 。m a x + u u ) ) ，其中u 代表空子句。m a x + ( ) = m a x + n m a x ( k ) 。显然，m a x + 是m a x 中 分裂公式的闭包，即公式的分裂在m a x + 中是封闭的。而且证明了这种递归构 造方法具有可靠性和完备性。 另一方面，我们将研究关于 z 4 戈+ ( ) 中公式改名的判定问题的复杂性。基 于分裂技术并通过证明m a x ( 1 ) 中公式改名问题在多项式时间内可以判定。我们 证明了：m a x + ) 中公式的改名问题在多项式时间内可以判定，并给出相应的 算法。最后，我们给出了一个文字改名的应用，以此来说明改名问题在证明系统 中起到的重要作用。 关键词：判定问题的复杂性，改名极小不可满足公式m a x ( k ) 一公式 中图分类号：0 1 4 1 1 文献标识码：a a b s t r a c t r e s e a r c ho nm i n i m a lu n s a t i s f i a b l ef o r m u l aa n di t ss u b c l a s s e si sa na c t i v et o p i c t h a tb e g i n st os u r f a c ei nr e c e n ty e a r s w ea r ei n t e r e s t e di ns u b c l a s s e so fm um a i n l y f o rt w or e a s o n s o n ei st h a ta l m o s ta l lh a r df o r m u l a sf o rr e s o l u t i o na r em i n i m a l u n s a t i s f i a b l ef o r m u l a s ，t h eo t h e ri st h a tad e e p e ru n d e r s t a n d i n go fm u f o r m u l a s m a yh e l pt od e v e l o pn e wh a r df o r m u l a sa n dn e ws a t i s f i a b i l i t ya l g o r i t h m s ac ff o r m u l afi sm i n i m a fu n s a t i s f i a b l e ( j i f 矿) i ffi su n s a t i s f i a b l ea n d d e l e t i n ga na r b i t r a r yc l a u s er e s u l t sas a t i s f i a b l ef o r m u l a ，af o r m u l af i nm ui 8 c a l l e dm a x i m a l , i ff o ra n yc l a u s e ，fa n da n yh t e r a lla n d1 l ，lq ，a d d i n g lt o ，y i e l d sas a t i s f i a b l ef o r m u l a t h es e to fm a x i m a lm i n i m a lu n s a t i s f i a b l ei s d e n o t e da sm x ar e n a m i n go ff o r m u l afi sam a p p i n gi po v e rv a r ( f ) s u c h t h a tl p ( z ) z ，1 z ) f o re v e r yv a r i a b l ez av a r i a b l er e n a m i n gi 8ap e r m u t a t i o n o fv a r i a b l e s al i t e r a lr e n a m i n gi sac o m b i n a t i o no fav a r i a b l er e n a m i n ga n da r e n a m i n g t h er e n a m i n g so ff o n n u l a sd o n tc h a n g et h es a t i s f i a b i l i t yo ff o r m u l a s t h er e n a m i n g sh a sp l a y e das i g n i f i c a n tr o l ei ns i m p l i f y i n gr e s o l u t i o np r o o f so f s o m eh a r df o r m u l a sa n dc o n s t r u c t i n gt h ee f f i c i e n ts a t i s f i a b i l i t ya l g o r i t h m s t h e v a r i a b l ea n dl i t e r a lr e n a m i n gp r o b l e m so ff o r m u l a si nm u ( k ) i se q u i v a l e n tt ot h e g r a p hi s o m o r p h i s mp r o b l e m a sw ek n o w n ，t h eg r a p hi s o m o r p h i s mp r o b l e m i ss t i l li n p s oc o m p u t e rs c i e n t i s t sa r et r y i n gt os e e ks o m ep o l y n o m i a l l ys o l v a b l es u b c l a s s e s o fm i n i m a lu n s a t i s f i a b l ef o r m u l a sa l lt h ew h i l e i nt h i st h e s i s w es e e kas u b c l a s sm a x + o fm a x i m a lm i n i m a lu n s a t l s f i a b l e f o r m u l a sa n dt h ef o r m u l a si ni tc a nb ec o n s t r u c t e dr e c u r s i v e l y m a x + = f m a x i3 z v a r ( f ) v s v h t t i n g s ( f x ，f q ) ：b ，f q a f a x + u u ) ) ，w h e r el ji s e m p t yc l a u s e d e n o t em a x + ( 七) = ，a x + nm a x ( k ) o b v i o u s l y , t h es u b c l a s s ma x + i sc l o s u r eo nt h es p l i t t i n go ff o r m u l a si nm a x ，m o r e o v e r w es h o wt h a t t h em e t h o dc o n s t r u c t i n gr e c u r s i v e l yt h ef o r m u l a si nm a x + i sp r o v i d e dw i t hc o m - p l e t e n e s sa n ds o u n d n e s s o nt h eo t h e rh a n d ，w ew i l li n v e s t i g a t et h ec o m p l e x i t yo fd e c i s i o np r o b l e m s f o rr e n a m i n gp r o b l e m s ( 1 i t e r a lr e n a m i n g ；v a r i a b l er e n a m i n g ) o ft h ef o r m u l a si n m a x + ( ) w ew i l lp r e s e n ta l g o r i t h m ss o l v i n gt h ea b o v em e n t i o n e dp r o b l e m si n p o l y n o m i a lt i m ef o r 丘x e dk t h ep r o o fi sb a s e do nt h es p l i t t i n gt e c h n o l o g ya n d t h ef a c tt h a tt h ec o m p l e x i t i e so fr e n a m i n g so ff o r m u l a si nm a x ( i ) a r ep o l y n o m i a l t i m e f i n a l l y , w eq u o t ea p p l i e a t i o no ft h el i t e r a lr e n a m i n gt oi l l u m i n a t et h ep o w e r o ft h er e n a m i n g sf o rp r o p o s i t i o n a lp r o o fs y s t e m s k e yw o r d s ：c o m p l e z i t yo ，d e c i s i o np r o b l e m , r e n a m i n g , m i n i m a lu n s a t i s f i a b l e f o r m u l a s , f x + ( ) - f o r r n u 妇 c h a p t e r1 i n t r o d u c t i o n al i t e r a l 妇口p r o p o s i t i o n a lv a r i a b l ed ran e g a t e dp r o p o s d i o n a lv a r i a b l e ac l a u s e c 话ad i s j u n c t i o no fl i t e r a i s , c = ( l 1v v 厶n ) ，af o r m u l af 讯c o n j u n c t i o n n o r m a lf o m 何州妇ac o n j u n c t i v ed ，c l a u s e s , f = ( a ， g ) ，v a r ( f ) i s t h e s e to fv a r i a b l e so c c u 咖讯矾ef o r m u l af ，a n dl i t ( p ) i st h es e td ，l i t e r a l s o e c u 仃i 姐 他t h ef o r m u l af w ed e n o t e # v a t ( f ) a n d 铲c f ( f ) 0 , 8t h en u m b e ro f v a r i a b l e sa n dt h en u m b e rd ，c l a u s e s 讥fr e s p e c t i v e l y , a n dp o s ( z ，f ) m 印n e g ( x ，f ) ) a 8t h en u m b e ro yv a r i a b l ez o c c u r r i n gp o s i t i v e l y 阮s p n e g a t i v e l y ) 轨f w ed e n o t e o c c ( x ，f ) = ( p o s ( x ，f ) ，n e a ( x ，f ) ) f o rn ，r21 ，l e tc n f ( n ，r ) 6 et h ec l a s so fg ff o r m u l a s 砸地礼v a r i a b l e sa n d rc l a u s e s g e n e r a l l y , w ec o n s i d e rt h ec l a s so y f o r m u l a sf ( 七) = u 。1c n f ( n ，礼+ 七) j 1 ，w h e r et h ei n t e g e r c a l l e dt h ed e f t c i e n c yo y f o r m u l a s f o rf ( k ) t h es a t _ 。s f i - a b d 。t yp r o b l e mr e m a i n sn p c o m p l e t e ac n f1 0 r m u l af 妇m i n i m a lu n s a t i s f i a b l e ( m u ) 矿f i su n s a t i s f i a b l ea n dd e l e t i n ga na r b z t r a r yc l a u s er e s u l t sas a t i s f i a b l ef o r - m u l a t h ep r o b l e mw h e t h e rac nff o r m u l a 话m i n i m a lu n s a t i s f i a b l ei sk n o w nt ob e d p c o m p l e t e 2 吼w h e r ed p 妇t h ec l a s so fp r o b l e m sw h i c hc a nb e d e s c r i b e da st h e d z f f e r e n c eo ft w on p - p r o b l e m s 2 谚l e tm u ( k ) b et h es e to fm i n i m a lu n s a t i s f i a b l e y o r m u l a s 研砘nv a r i a b l ea n d n + 七c l a u s e s1 0 r 触e d ah o r nc l a u s ei sac l a u s e 加z 琥a tm o s to n ep o s i t i v eh t e r a l ah o r ny o r m u l ai sac o n j u n c t w no yh o r nc l a u s e s i n 嘲。g d a v y d o v t1 d a v y d o v aa n dh k l e i n eb i i n m gp r o v e dt h a tn of o r m u l ai n f ( o ) i sm i m m a lu n s a t i s f i a b l e am m z m a lu n s a t i s f i a b l eh o r ny o r m u l ai si nf ( 1 ) ， a n df o ra n ym i n i m a lu n s a t i s f i a b l ef o r m u l a 讥f ( 1 、t h e r i ee x i s t sa tl e a s to n ev a r i a b l e o c c u r r i n ge x a c t l yo n c ep o s i t i v e l ya n do n c en e g a t i v e l yi 仃d i s t i n c tc l a u s e s f o rs u b c l a s s e sl i k eh o r m - f o r m u l a 肼f o r m u l a s 讯2 c n ft h em i n i m a lu n s a t z s f i a b l ep r o b l e m c a nb es o l v e di nq u a d r a t i ct i m e 0 k u l l m a n ns h o w e dt h a tt h em m i m a lu n s a t i s f i a b l e p r o b l e mf o rf ( k ) i sd e c i d a b l e 讯p o l y n o m i a lt i m e 肼 c ，h p a p a d i m i t r i o ua n dd w o r y e 2 s h o w e dt h a ty o re v e r yf o r m u l afo n e l 2 c a nc o n s t r u c t 轨p o l y n o m i a lt i m eay o r m u l a ( f 1s u c ht h a t ： fi ss a t i s f i a b l e 谚a n do n l yi yf ( n ss a t i s f i a b l e ； fi su n s a t i s f i a b l e 毽a n do n l y 毽o fi sm i n i m a lu n s a t i s f i a b l e ； i no t h e rw o r d s ，a nu n s a t z s f i a b l ef o r m u l ac a nb et r a n s f o r m e di n t oam m i m a lu n - s a t z s f i a b l ef o r m u l ai np o l y n o m i a lt l r n e b oi t 妇s i g n i f i c a n tt h a tw ei n v e s t i g a t et h e u n s a t i s f i a b l ei o r m u l ab ym i n i m a lu n s a t i s f i a b l ef o r m u l a ac l a u s el fi sm a x i m a l 讯f 毽| o ta n yl i t e r a llo c c u 嘲gn e i t h e rp o s i t w e l y n o rn e g a t i v e l yi n it h ef o r m u l ao b t a i n e df r o mf b ya d d i n glt of 证s a t i s f i a b l e a 1 0 r m u l af 伽m c ，缸m a x i m a lm i n i m a lt m s a t i s f i a b l e 矿a n yc l a u s e 协f 妇m a x i m a l t h a ti ss t r o n g l ym m 4 m a lu n s a t i s f i a b l e | o r m u l ad e f i n e d 诹 2 8 1 w ed e n o t et h es e t o fm a x i m a lm i n i m a lu n s a t i s f i a b l ea 8m a x ，a n dm a x ( k ) = m u ( k ) nm a x i n f 1 5 1 , am e t h o dc o n s t r u c t i n gam a x i m a l m i n i m a lu n s a t i s f i a b l e o r m u l a 如mam i n - i m a lu n s a t i s f i a b l ef o r m u l ai si n t r o d u c e d i nt 3 0 l i th a sp r o v e dt h a tt h ev a r i a b l e r e n a m i n ga n dl i t e r a lr e n a m i n gp r o b l e my o rf o r m u l a s 轨m a xa r ea sh a r d t h e g r a p hi s o m o r p h i s mp r o b l e mg i w ec a l lap e r m u t a t i o no | v a r i a b l e sav a r i a b l er e n a m i n g i n s t e a do yap e r m u t a l i o no i v a r i a b l e sw ec a nm a k eu s eo y am o r eg e n e r a lr e n a m i n g , n a m e l ya8 0c a l l e dl i t - e r a lr e n a m i n g 吼时m e a n sw eh a v eap e r m u t a t i o n 吖v a r i a b l e sa n da d d i t i o n a l l yv a r i - a b l e sc a nb es i m u l t a n e o u s l yr e p l a c e db y 伽c o m p l e m e n t s m o r ef o r m a l l y , 如r f o r m u l a s fa n dgav a r i a b l er e n a m i n g 妒i sao n e t o o n em a p p i n g ：v a r ( f ) _ p a r ( g ) a n i la l i t e r a lr e n a m i n g 妒i sao n e t o o n em a p p i n g ：l i t ( f ) l i t ( a ) ，w h e r e 妒( - z ) 1 妒( z ) i o ta n yv a r i a b l e 置，ar e n a m i n gi saf u n c t i o n 峄m a p p i n gap r o p o s i t i o nv a r i a b l ez t o 薯o r z t h er e n a m m g s0 1 o r m u l a sd o n tc h a n g et h es a t z s f i a b d z t yo f f o r m u l a s 1 1m o t i v a t i o n s t h er e n a m i n g sh a sp l a y e das i g n i f i c a n tr o l e 讥s i m p l i f y i n gr e s o l u t i o np r o o f so 8 0 m e h a r di o r r n u l a sa n dc o n s t r u c t i n gt h ee f f i c i e n ts a t 2 s f i a b i l i t ya l g o r i t h m s t h er u l eo ys y m m e t r ya l l o w st h e o l l o w i n gi n f e r e n c e ：l | ac l a u s e | h a sb e e n d e r i v e df r o mas e to c l a u s e sfa n d 诂ap e r m u t a t i o no v e rt h es e to yv a r i a b l e so c c u t t i n g 饥f ，t h e nt h ec l a u s e 妒( ，) c a nb ei n f e r r e d0 , 8t h en e x ts t e p 饥t h ed e r i v a t i o n i n s t e a do fap e r m u t a t i o no yv a r i a b l e sw ec a nm a k eu s eo fam o r eg e n e r a lr e n a m i n g , n a m e l yl i t e r a lr e n a m i n g i n 2 l j k r i s h n a m u r t h yi l l u s t r a t e dt h ep o w e ro js y m m e - t r yf o rp r o p o s i t i o n a lp r o o s y s t e m s ，h ea d d e dt ot h er e s o l u t i o nc a l c u l u st h er u l eo f s y m m e t r ya n dg i v es h o r tp r o o f s o rs o m eh a r df o r m u l a s a sw ek n o w n , s o m eh a r d e x a m p l e sh a v eap e r f e c ts y m m e t r i c a ls t r u c t u r e f o re x a m p l e ，t h ep i g e o nh o l ef o r - m u l a sh a v e 伽t h i se x t e n d e dc a l c u l u sap , o l0 ，p o l y n o m i a ls i z e f u r t h e ri n t e r e s t i n g 1 2 p r o b l e m sa n dr e s u i 卫s3 r e s u l t sc d nb ef o u n d 讥u r c u h a r t sp a p e r p t l w ei n v e s t i g a t et h er e n a m i n gp r o b l e m sm a yh e l pt oi m p r o v es o m ea l g o r i t h m f o r e x a m p l e , t h ed i f f e r e n tr e n a m i n g sc a nb eu s e d 讯d a m s - p u t n a m l o v e p a n d - l o g e m a n a l g o r # h m ( d p l l ) 5 s u p p o s e 饥t h es p l i t t i n gt r e eo ft h ed p l l a l g o r i t h m st w oy o r m u l c t sa r eg e n e r a t e da ts o m en o d e si o rw h i c ho n eo ft h ef o r m u l a sc b nb em a p p e d t ot h eo t h e ro n eb ydr e n a m i n g t h e nw ec a nr e p l a c eo n eo ft h ef o r m u l a sb yt h e e m p t yc l a u s ea n dc o n t i n u et f ，f 纨t h er e n a m i n gf o r m u l a s ，s ov i ec a nr e d u c et h en o d e s o fs p h t t i n 9t r e ea n dt h ep r o o fo | t h ef o r m u l a sh a v eb e e ns i m p l i f i e d 1 2p r o b l e m sa n dr e s u l t s w h e nu s i n gt h er u l eo is y m m e t r y 轨p r o p o s i t i o n a lc a l c u l u s , w ew i l ln a t u r a l l yf a l l a c r o s st h ed e c i s i o np r o b l e m ：f o rf o r m u l a sha n dfi nc nf w h e t h e ro rn o tt h e r e e x i s t sdr e n a m i n g p ，s u c h t h a t l p ( = f7 1 n 3o 】，t h ea u t h o rh a sp r o v e dt h a t ： ( 1 ) t h ev a r i a b l ea n dl i t e r a lr e n a m i n gp r o b l e m sd ，f o r m u l a s 伽m u ( 1 ) ( e v e n 矿h o r n f o r m u l a s ) i se q u i v a l e n tt ot h eg r a p hi s o m o r p h i s mp r o b l e m ( e ) t h ev a r i a b l ea n dl i t e r a lr e n a m i n gp r o b l e m sd ，f o r m u l a s 轨m a x 话e q u i v a l e n tt o t h eg r a p hi s o m o r p h i s mp r o b l e m 俐t h e v a r i a b l ea n d l i t e r a l r e n a m i n g p r o b l e m s o f f o r m u l a s 伽m a x ( 1 ) a n d m a r g ( 1 ) a r es o l v a b l ei np o l y n o m i a l a sw ek n o w n , t h ec o m p l e x z t yo fd e c i s i o np r o b l e my o rt h eg r a p hi s o m o r p h i s m 妇s t i l l ao p e np r o b l e m 2 2 w eo n l yk n o wt h a ti t 诂i nn p ，b u t , u pt ot h ep r e s e n t , w ed o n t k n o ww h e t h e ro rn o ti tc a nb ed e c i d a b l e 讥p o l y n o m z a lt i m e 。竹d r 妇i tn p c o m p l e t e s ow ew i l ls e e kas u b c l a s so m i n i m a lu n s a t 2 s f i a b l ef o r m u l a s , i nw h ：c ht h ed e c i s i o np r o b l e m sf o rr e n a m i n g so ft h ef o r m u l a sa r es o l v a b l e 饥p o l y n o m m lt z m e i nt h i st h e s i s , w ed e f i n eas u b c l a s s0 1m a m m a lm i n i m a lu n s a t i s f i a b l ef o r m u l a s a sf o l l o w ： m a x + = f m a x ij z v a r ( f ) v s p l i t t i n g s ( 疋，f k ) ：r ，f k m a x + u u ， w h e r eu 妇e m p 留c l a u s e o b v i o u s l y ，t h es u b c l a s sm a x 十i sc l o s u r eo nt h es p l i t t i n g o f f o r m u l a si nm a x w ed e n o t em a x + ( ) = m a x + nm a x ( k ) m o r e o v e rw e w i l lc o n s i d e rt h e o u o w i n 9p r o b l e m ： p r o b l e m1 ；m a x + ( ) 一r ( r e n a m i n gf o r f o r m u l a s 讥m a x + ( k ) ， i n s t a n c e ：f o r m u l a s 日a n df 轨m a x + ( ) q u e s t i o n ：d o e st h e r ee x i s tar e n a m i n g 妒s u c ht h a t 妒( 日) = f p p r o b l e m2 ：m a x + ( ) y r ( v a r i a b l er e n a m i n g o rf o r m u l a s 讥m a x + ( ) ， 4 c h a p t e r1 i n t r o d u c t i o n i n s t a n c e ：f o r m u a sha n dfi nm a x + ( k ) q u e s t i o n ：d o e st h e r e 删口v a r i a b l er e n a m i n g 妒s u c ht h a ti o c h ) ：f p p m 矗a 鲫l 占：m a x + ( 七) 上兄( 1 i t e r a lr e n a m i n gf o rf o r m u l a si n 肘a x + ( 七) ， i n s t a n c e ：f o r m u a s 日a n dfi nm a x + ( k ) q u e s t i o n ：d o e st h e r ee x i s t 口l i t e r a lr e n a m i n g 妒s u c ht h a t 妒( 脚：p p 耽p 御e 耐口m e t h o dt oc o n s t r u c tr e c u r s i v e l yt h e o r m u t o a 讥m a x + n dp m 口e t h a tt h em e t h o di sp m m d 耐w i t hc o m p l e t e n e s sa n d 8 0 u 圮如啪 砘t h es p l i t t i n gt e c h n o l o g ya n dt h e a c tt h a tt h ec o m p l e x i t i e so yr e n a m i n g so y i o r m u l a s 协m a x ( 1 ) a r ep o l y n o m i a lt i m e ，加es h o wt h o tt i t e o o b l ea n dl i t e m l 他n o m 卉wo h o r m u t a si nm a x + a r e d e c i d a b l e 轨p o l y n o m i a lt 打础f o rf = e f i 七 c h a p t e r2 毒 m i n i m a lu n s a t i s f i a b l ef o r m u l a s i nt h i sc h a p t e r , w eu a l lg i v es o m eb a s i cn o t a t i o n sa n db a s i cd e f i n i t i o n s 竹p r o p o s i - t i o n a l 切记a n dm u ( k ) m o r e o v e r , w ew i l ls h o ws o m en e wd e v e l o p m e n to nm u ( k ) 2 1 p r o p o s i t i o n a ll o g i c p r o p o s i t z o n sa r ej u s ts t a t e m e n t sa n dp r o p o s i t w n a ll o g i c 妇t h e 姆co yc o m p o u n ds e n - t e n c e sf o r m e dw i t hc o n n e c t i v e ss u c ha s 缸竹d ：，d r ：d t ： i m p l i e s a n dva n do n l y 矿 b u tw i t h o u tc o n m d e r a 缸o no f t h eq u a n t z f i e r 8 f o ra l l ：a n d ”t h e r ee x i s t s ”i tc o m p r i s e s s y n t a xp a r t , w h i c h 诂af o r m a ln o t a t i o ny o rw r z 坑n ga s s e r t i o n sa n ds e m a n t i c sp a r t , w h i c hg i v e sam e a n i n gt oa s s e r t i o n s t h es y n t a c t i cp a r to y p r o p o s i t i o n a ll o g i cc a nb e r e g a r d e da st h ew a y 饥w h i c hs t a t e m e n t sa r ec o m b i n e dt oy o mo t h e rs t a t e m e n t s t h e s e m a n t i c sp a r to yi ti sc o n c e r n e d 埘巩a s c r i b i n gm e a n i n gt ot h es y m b o l s 饥v a r i o u s w a y s am a j o rt h e m eo nt h ed e v e l o p m e n t 吖l o g i c 妇t h er e l a t i o n s h i pb e t w e e nt h e s e t w oa s p e c t so l a n g u a g e ， i np r o p o s i t i o n a ll o g i c , t h em e a n i n gg i v e nt ot h ec o n n e c t i v e s 诂e n t i r e l yu n a m - b 匆u o u s n o w , w ei n t r o d u c e o r m a ls y m b o l sy o rt h e s ec o n n e c t w e s0 , 8 o l l