（计算机应用技术专业论文）中间逻辑中的范式研究.pdf

摘要 中间逻辑是强弱介于经典逻辑与直觉主义逻辑之间的一大类命题 逻辑近年来，这些逻辑在计算机科学领域中受到极大的重视而范 式在逻辑及其相关领域中起着很重要的作用，特别是对于自动定理证 明、自动推理和逻辑程序领域。本论文的主要目的是：寻找一些可以 应用到基于中间逻辑的自动定理证明、自动推理和逻辑程序等领域的 有用范式；研究这些范式在各中间逻辑中的存在性；设计一些用来对 公式进行以上范式化简的算法 在本论文中，我们深入地研究了中间逻辑中的范式问题共涉及 到六种范式，包括：蕴舍范式、扩展合取与析取范式，弱合取、析取 与蕴含范式我们证明了h t 逻辑是唯一的具有蕴含范式的非经典中间 逻辑，同时研究了三种弱范式在g s d e l 逻辑中的存在性对于公式的 范式化简，我们提出了两类范式化简算法，一类是基于模型刻画公式 的语义方法，另一类是基于重写系统的语法方法作为以上研究的附 加结果，我们得到了四种模型刻画公式，引入了k r i p k e 模型之间初等 蕴舍的概念，并给出了一个初等蕴舍的充分必要条件最后，我们研 究了关于以上范式化简问题的复杂性 关键词：范式；中间逻辑；g 6 d e l 逻辑；模型刻画公式；初等蕴 含；范式化简；计算复杂性 中图分类号：t p l 8 1 a b s t r a c t i n t 唧a e m a t el o g i c sa r ea ne x t e n s i v ec l a s so fp r o p o s i t i o n a ll o g i c sw h i c hh a v er e c e n t l y r e c e i v e ds i g n i f i c a n ta t t e n t i o ni nc o m p u t e rs c i e n c e n o r m a lf o r mp l a y sa ni m p o r t a n t r o l ei nl o g i ca n dr e l a t e dr e s e a r c ha r e a s ，e s p e c i a l l yi na u t o m a t e dt h e o r e mp r o v i n g ， a u t o m a t e dr e a s o n i n ga n dl o g i cp r o g r a m m i n g t h ep u r p o s e so ft h et h e s i sa r et o d i s c o v e rs o m eu s e f u ln o r m a lf o r m sf o rt h e s ea r e a si ni n t e r m e d i a t el o g i c s ；t oo b t a i n t h ee x i s t e n c er e s u l t sf o rt h e s en o r m a lf o r m si nm t e r m e d i a t el o g i c s ；a n dt od e v i s e s o m ea l g o r i t h m st or e d u c ea 1 1a r b i t r a r yf o r m u l at ot h ea b o v en o r m a lf o r m s i nt h i st h e s i sw ec a r r yat h o r o u g hi n v e s t i g a t i o ni n t on o r l i l a lf o r m si ni n t e r m e - d i a t el o g i c s s i xk i n d so fn o r m a lf o r m sa l ef o c u s e d ，i n c l u d i n gi m p l i c a t i o n a ln o r m a l f o r m ，e x t e n d e dc o n j u n c t i v ea n dd i s j u n c t i v en o r m a lf o r m s ，a n dw e a kc o n j u n c t i v e ， d i s j u n c t i v ea n di m p l i c a t i o n a ln o r m a lf o r m s t h ew e a k e s ti n t e r m e d i a t el o g i cw i t h i m p l i c a t i o n a ln o r m a lf o r mi sp r o v e dt ob et h el o g i co fh e r e 口以t h e r e ，a n dt h ee x i s - t e n c eo ft h r e ek i n d so fw e a kn o r m a lf o r m si ng s d e ll o g i c si sa l s oi n v e s t i g a t e d t o r e d u c eaf o r m u l at oe v e r yn o r m a lf o r mm e n t i o n e da b o v e t w ok i n d so fr e d u c t i o n m e t h o d sa r ep r e s e n t e d ，o n eo fw h i c hi sb a s e d0 1 1m o d e l - c h a r a c t e r i z i n gf o r m u l a sa n d t h eo t h e ro i lr e w r i t i n gs y s t e m s a sb y p r o d u c t so ft h e s ei n v e s t i g a t i o n s ，f o u rk i n d s o fm o d e l - c h a r a c t e r i z i n gf o r m u l a sa r eo b t a i n e d ；ac o n c e p to fe l e m e n t a r yi m p l i c a t i o n b e t w e e nt w ok r i p k em o d e l sa r ei n t r o d u c e d ；a n dt h es l l 伍e ea n dn e c e s s a r yc o n d i t i o n o fe l e m e n t a r yi m p l i c a t i o nb e t w e e nl i n e a rk r i p k em o d e l si sa l s og i v e n i nt h ee n d ， w es t u d yt h ec o m p l e x i t i e so fr e d u c t i o n st 0t h e s en o r m a lf o r m s k e yw o r d s ：n o r m a lf o r m ；i n t e r m e d i a t el o g i c ；g s d e ll o g i c ；m o d e l - c h a r a c t e r i z i n g f o r m u l a ；e l e m e n t a r yi m p l i c a t i o n ；n c n v a a lf o r mr e d u c t i o n ；c o m p u t a t i o n a lc o m p l e x i t y c h i n e s el i b r a r yc l a s s i f i c a t i o n ：t p l 8 1 附：学位论文原创性声明和关于学位论文使用授权的声明 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究所取得的成果。除文中已经注明引用的内容外，本 论文不包含任何其他个人或集体已经发表或撰写过的科研成果。 对本文的研究在做出重要贡献的个人和集体，均已在文中以明确 方式标明。本人完全意识到本声明的法律责任由本人承担。 论文作者签名： 关于学位论文使用授权的声明 本人完全了解贵州大学有关保留、使用学位论文的规定，同意学 校保留或向国家有关部门或机构送交论文的复印件和电子版，允许论 文被查阅和借阅；本人授权贵州大学可以将本学位论文的全部或部分 内容编入有关数据库进行检索，可以采用影印、缩印或其他复制手段 保存论文并口汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名： c h a p t e r1 i n t r o d u c t i o n 1 1 b a c k g r o u n d i n t e r m e d i a t el o g i c sa l ea ne x t e n s i v ed a s so fp r o p o s i t i o n a ll o g i c se x t e n d i n gi n t u - i t i o i n s t i ep r o p o s i t i o n a ll o g i ca n dw e a i 【e rt h a nc l a s s i c a lp r o p o s i t i o n a ll o g i cr i n c l u d i n g i n t u i t i o n i s t i c l o g i c a n d c l a s s i c a l l o g i c ) ( s e e ，e g ， 3 1 ，3 】) t h e e a r l y w o r k m t h i s f i e l d i s d e v o t e dt ou n d e r s t a n d i n gt h er e l a t i o n s h i pb e t w e e nc l a s s i c a la n di n t u i t i o n i s t i cl o g i c s ， a n di n t e r m e d i a t el o g i c sw e , r eo n l ys t u d i e db yaf e wr e s e a x c h e si na p u r et h e o r e t i c a l v i e w b u tt h i ss i t u a t i o ni sd r a m a t i c a l l yc h a n g i n gs i n c es o i l 2 ei n t e r e s t i n gc o n n e c t i o n s w i t hc o m p u t e rs c i e n c eh a v eb 咖d i s c o v e r e dr e c e n t l y p e r h a p st h em o s ti n t e r e s t i n go n eo ft h e s ec o n n e c t i o n si st h er e l a t i o n s h i pb e t w e e n i n t e r m e d i a t el o 百c sa n dp a r a l l e lp r o g r 椰t h ew e l l - k n o w nc u r r y - h o w a r di s o m o r - p h i s ms h o w s ，i ni n t u i t i o i n s t i cl o g i c ，e v e r yp r o o fi nn a t u r a ld e d u c t i o nc o r r e s p o n d s t oa t y p e dat e r m ( f u n c t i o n a lp r o g r a m ) ，a n dt h a t o m a b z 8 缸o no ft h ep r o o fc o l t e - s p o n d st or e d u c t i o no ft h ec o r r e s p o n d i n gt e r mt oan o r m a lf o r m ( e x e c u t i o no ft h e p r o g r a m ) ( s e e 【2 9 】) a v r o n 【2 】s u g g e s t e d t h a t a s i m i l a r r e l a t i o n s h i p m a y h o l d b e t w e e n g s d e ll o g i c s ( ac l a s so fi m p o r t a n ti n t e r m e d i a t el o g i c s ) a n dp a r a l l e lp r o g r a m s a n o t h e rp r o m i s i n ga p p h c a t i o nt oc o m p u t e rs c i e n c em a yb ei nt h ea r e a so fa n - t o m a t e dd e d u c t i o nf o rr e a s o n i n gw i t hu n c e r t a i n t y , i nw h i c hf u z z yl o g i cp l a y sa l l i m p o r t a n tr o l e a si sw e l lk n o w n g 6 d e ll o g i c sa r eo n eo ft h ef a m i l i e so fl o g i c sw h i c h h a v eb e e nu s e da sab a s i so ff u z z yl o g i c ( s e e ，e g ， 5 ，1 5 】) c o m p a r i n gw i t ho t h e r 1 21 1 b a c k g r o u n d l o g i c sp l a y i n gt h es a m er o l e ( e g ，l u k a s i e w i c sa n dp r o d u c tl o g i c s ) ，g & i e ll o g i ci s a l s oc l o s e l yr e l a t e dt oi n t u i t i o n i s t i cl o g i c ：i ti st h el o g i co fh n e a r l y - o r d e r e dh e y t i n g a l g e b r a s ( s e e 【18 】) t h et h i r dr e a s o nm a k i n gu st a k es e r i o u si n t e r m e d i a t el o g i c si sd u et ot h ed i s c o v - e r i e so fp e a r c ea n dl i f s c h i z ee ta 1 t h e kr e s u l t si n 【2 7 ，2 2 s h o w ，t w of o r m u l a sa r e s t r o n g l ye q u i v a l e n ti ne q u i l i b r i u ml o g i c ( 8n o n - m o n o t o n i cl o g i cu n d e rs t a b l em o d e l s e m a n t i c s ) i fa n do n l yi ft h e na r el o g i c a l l ye q u i v a l e n ti nt h ei n t e r m e d i a t el o g i co f h t t h i si n d i c a t e st h a tt h e r ei sa l s oa l la m a z i n gc o n n e c t i o nb e t w e e ni n t e r m e d i a t e l o g i c sa n ds o m ef o r m a l i s m so fn o n - m o n o t o u i cr e a s o n i n ga n dl o g i cp r o g r a m m i n g n o r m a lf o r m sp l a yi m p o r t a n tr o l e si nm a n y & t e a so fm a t h e m a t i c s ，l i k el i n e a r a l g e b r a ，g r o u pt h e o r y , e s p e c i a l l ym a t h e m a t i c a ll o g i c g e n e r a l l ys p e a k i n g ，ac e r t a i n k i n do fn o r m a lf o r mi nal o g i cc o n s i s t so fas e to fl o g i c a lf o r m u l a s 硒t hs i m p l e s y n t a x ，w e l l - u n d e r s t o o ds e m a n t i c sa n ds o m e n i c e p r o p e r t i e s t h em a i np u r p o s e o fi n v e 武i g a t i o no nt h en o r m a lf o r mi st os i l n p l i 母p r o b l e m si nl o g i c f o re x a m p l e ， t od e c i d et h ev a l i d i t yo fa na r b i t r a r yf o r m u l ai nc l a s s i c a lp r o p o s i t i o n a ll o g i c t h e r e i 8n op o l y n o m i a lt i m ea l g o r i t h m b u tw ec a nd e v i s ea ne f f i c i e n ta l g o r i t h mt od e c i d e t h ev a l i d i t yo faf o r m u l ai nd i s j u n c t i v en o r m a lf o r m a n o t h e rr e a s o nt ou s en o r m a l f o r m si nl o g i ci st h a taf o r m u l ai nan o r m a lf o r mc a no f t e nb ee a s i l yu n d e r s t o o d i nt h i st h e s i s w ew i ns i m p l yr e g a r dan o r m lf o r ma sas e to ff o r m u l a w es a y af o r m u l ai s 饥ac e r t a i nn o r m a l f o r mi fi tb e l o n g st ot h ef o r m u l as e to ft h i sn o r m a l f o r m af o r m u l ai sr e d u c i b l et oan o r m a lf o r mi n8g i v e nl o g i ci ft h e f ei sa n o t h e r f o r m u l ai nt h a tn o r m a lf o r ms u c ht h a tt h et w of o r m u l a sa r ee q u i v a l e n ti nt h eg i v e n l o g i c a n dal o g i ci sr e d u c i b l et o8 c e r t a i nn o r m a lf o r m ，o rac e r t a i nn o r m a lf o r m e v s t si na l o g i c i fe v e r yf o r m u l ai sr e d u c i b l et ot h en o r m a lf o r mi nt h eg i v e nl o g i c i nc l a s s i c a lp r o p o s i t i o n a ll o g i c ，t h e r ea r e2k i n d so fw e l l - k n o w nn o r m a lf o r m s ： c o n j u n c t i v en o r m a lf o r m ( o rs i m p l yc n f ) a n dd i s j u n c t i v en o r m a lf o r m ( o rs i m p l y d n f ) af o r m u l ai ss a i dt ob e 伽c n fi fi ti 8ac o n j u n c t i o no fc o n j u n c t i v ec l a u s e s 3 12 m a i nr e s u 如r s w h i c ha r ed i s j u n c t i o n so fc l a s s i c a ll i t e r a l s h e r e i n ，ac l a s s i c a ll i t e r a l ( o rs i m p l yc m e 砌i se i t h e rap r o p o s i t i o n a lv a r i a b l eo rt h en e g a t i o no fap r o p o s i t i o n a lv a r i a b l e s i m i l a r l y , af o r m u l ai ss a i dt ob em d n ff li ti sad i s j u n c t i o no fd i s j u n c t i v ec l a u s e s w h i c ha r ec o n j u n c t i o n so fc l a s s i c a ll i t e r a l s t h e r ei sa l s oa n o t h e rn o r m a lf o r m ： i m p l i c a t i o n a ln o r m a lf o r m ，o rs i m p l yi n f ，w h i c hi su s u a l l yu s e di nt h ea r e ao fl o g i c p r o g r a m m i n g ( 8 【2 3 】) af o r m u l a 饥i n fi sac o n j u n c t i o no fi m p l i c a t i o n a ld a n s c s w h i c ha r ef o r m u l a si nt h ef o l l o w i n gf o r m ： ( z l a l 2 a a k ) 一( k + 1 v ，件2 v vz 。+ 。) ， w h e r eh ( 1si m + 7 1 ) a r ec l a s s i c a lh t e r a l sa n dm ，n 0 i ti se a s yt os e et h a t i m p h c a t i o n a ln o r m a lf o r mi sa ne x t e n s i o no fc o n j u n c t i v en o r m a lf o r m a sw ek n o w a l lt h ea b o v en o r m a lf o r m se x i s ti nc l a s s i c a lp r o p o s i t i o n a ll o g i c t oc o m p a r et h ee x p r e s s i v ep o w e ro fe q u i l i b r i u ml o g i cw i t hl o g i cp r o g r a m m i n g u n d e rs t a b l em o d e ls e m a n t i c s ，c a b a l a ra n d f e r r a r i s 【6 】h a v ec a r r i e da l li n v e s t i g a t i o n i n t on 0 1 2 n a lf o r m si nl o g i ch t t h e yh a v es h o w nt h a th ti sr e d u c i b l et oi n f ，a n d h a v ee x t e n d e dc n ft oa n o t h e rn o r m a lf o r m ( w h o mw ec a l le x t e n d e dd i s j u n c t i v e ，l d m 以加n ，o rs i m p l ye d n f ) b yr e g a r d i n gf o r m u l a sl i k e 节a n dp 。g h t e r a l s ( t o g e t h e rw i t hc l a s s i c a ll i t e r a l s ，w ec a l lt h e me x t e n d e dl i t e r a l s ，o rs i m p l ye 1 i t e r a l s ) ，a n dp r o v e nt h a th t i sr e d u c i b l et ot h i sn o r m a lf o r m t or e d u c eaf o r m u l a t ot h en o r m a lf o r mi n f ，c a b a l a xa n dp e a r c ee 七a l 【7 】g a v ean o r m a lf o r mr e d u c t i o n a l g o r i t h mf o ri n - fi nh t t oo l l rb e s tk n o w l e d g e ，t h e s ea r et h eo n l yw o r ko i l n o r m a lf o r m si ni n t e r m e d i a t el o g i c sb e f o r eo u rs t u d y 1 2m a i nr 凳s u l t s n o ww et u r nt oo u rw o r ki nt h i st h e s i s m o t i v a t e db yt h ew o r km e n t i o n e d a b o v e ，w e t r yt oc a r r yac o m p r e h e n s i v ei n v e s t i g a t i o ni n t on o r m a lf o r m si ni n t e r m e d i a t el o g i c s t h em a i np r o b l e m st h a tw ea r ei n t e r e s t e di na r e ： 。 41 2 m a i nr e s u l 月s 1 g i v e nac e r t a i nn o r m a lf o r m ，w h i c hi n t e r m e d i a t el o g i c sc a nb er e d u c i b l et ot h i s n o r m a lf o r m ? w ew i l ls i m p l yc a l lt h i st h ep r o b l e mo fe x i s t e n c eo fn o r m a lf o r m s 2 i ft h ea b o v en o r m a lf o r m sh a v en o te n o u g he x p r e s s i v ep o w e r h o wt oe x t e n d t h e mt om o r eg e n e r a ln o r m a lf o r m s ? n o t et h a tac a n o n i c a ln o r m a lf o r ms h o u l d h a v es i m p l es y n t a xa n dw e l l - u n d e r s t o o ds e m a n t i c s 3 g i v e n8c e r t a i nn o r m a lf o r ma n da , ni n t e r m e d i a t el o g i c h o wt or e d u c ea na n b i t r a a yf o r m u l at of l a eg i v 髓n o r m a lf o r mi nt h a tl o g i c ? a n dw h a ti st h et o m - p l e x i t yo fd o i n gt h i sr e d u c t i o n ? t h ef i r s tr e s u l to fo u i s t u d yi st h a ti - i ti st h eo n l yn o n o e l a s s i c a li n t e r m e d i a t e l o g i cw h i c hi sr e d u c i b l et od 旧( 8 e e 【3 5 】) s i m i l a rt ov , p n f ，w ee x t e n dc n f t o e x t e n d e dc o n j u n c t i v en o r m a lf o r m ( o rs i m p l ye c n f ) i nt h es a m ew a y , a n ds h o w e c n fa l s oe x i s t si ni - i t ( 舱e 阻】) b yi ；h ea i do fc o m p u t e r ，h o w e v e r ，w et l n d ，i t s e e l l l 8t h a tg 4 ，t h ei m m e d i a t es u c c e s s o ro fi - i ti ng 6 d e ll o g i c s ，c a n n o tb er e d u c i b l e t ob o t he ( 2 n i pa n d g d n f ，w h i c hl l l e s , l l st h e s en o r m a lf o r m so n l ye x i s ti naf e w i n t e r m e d i a t el o g i c s t h e r e f o r e ，w eh a v et oc o n s i d e rm o r eg e n e r a ln o r m a lf o r m s i nt h i st h e s i s w ee x t e n di 目, c n l 9a n de d n ft ow e a kc o n j u n c t i v ea n d d i s j u n c t i v e n o r m a lf o r m s ( d e n o t e db yw c n fa n d w d n f ) r e s p e c t i v e l yb yc o n s i d e r i n g f o r m u - l a sl i k e ( p q ) 。口蠲l i t e r a l s ( t o g e t h e rw i t he - l i t e r a l s ，砩c a l lt h e m w e a kl i t e r a l 【s ， o rs i m p l yw 4 i t e r a l s ) ，a n de x t e n di n ft ow e a ki m p l i c a t i o n a ln o r m a lf o r m ( o r s i m p l y v 旷叮f 1b yr e p l a c i n ge - l i t e r a lw i t hw - l i t e r a l t h er e s u l tt h a ta l lt h eg 6 d e ll o g i c s 8 f er e d u c i b l et ot h e s ew e a kn o r m a lf o r m sr e s p e c t i v e l y ( s e e1 3 3 ) i sa l s oo b t a i n e d a sb y p r o d u c t so ft h e s ei n v e s t i g a t i o n s ，f l o r a ei n t e r e s t i n gr e s u l t sa b o u tm o d e lt h e - o r y a l eo b t a i n e d f o re x a m p l e w ep u tf o r w a r dac o n c e p to fe l e m e n t a r yi m p l i c a t i o n b e t w e e nt w ok r i p k em o d e l s ，w h i c hi ss i m i l a rt ot h er e l a t i o no fe l e m e n t a r ye q u i v - a l e n e eb d 相岫t w of i r s t - o r d e rm o d e l s w es h o wt h a 七al i n e a rm o d e ld e m e ，a t a a i l y i m p l i e sa n o t h e rl i n e a rm o d e li fa n do n l yi ft h es e c o n do n ei sab i s i m u l a t i o ni m a g eo f 51 3 c o n t e n t s t h ef i r s to n e w ea l s og i v e3k i n d so fm o d e l - c h a r a c t e r i z i n gf o r m u l a s ，w h i c hp l a ya n i m p o r t a n tr o l ei np r b v i n gt h ee x i s t e n c eo fn o r m a lf o r m s t or e d u c eaf o r m u l at oac e r t a i nn o r m a lf o r m ，w ep r e s e n tt w ok i n d so fm e t h o d s ： o n ei sc a l l e ds e m a n t i c a lr e d u c t i o nw h i c hi sb a s e do i lm o d e l - c h a r a c t e r i z i n gf o r m u l a s ， a n dt h eo t h e ri ss y n t a c t i c a lr e d u c t i o nw h i c hi sb a s e do nr e w r i t i n gs y s t e m s e a c h r e d u c t i o nm e t h o dc a 以b ea p p l i e dt oe v e r yn o r m a lf o r mw h i c hi sm e n t i o n e da b o v e a n dt h et e n n i n a b i l i t ya n dc o r r e c t n e s sf o rt h e s en o r m a lf o r mr e d u c t i o n sa r ea l s o p r o v e d - i nt h ee n d w ep r o v et h a tt h e r ea r en op o l y n o m i a lt i m ea l g o r i t h m st od o e c n f ，e d n f ，w c n fa n dw d n fr e s p e c t i v e l y 1 3c o n t e n t s t h et h e s i si so r g a n i z e d 鹪f o l l o w s ：i nc h a p t e r2 w eg i v ea no v e r v i e wf o ri n t e r m e d i a t e l o g i c sa n dt h e i rs e m a n t i c s t h es y n t a xa n dk r i p k es e m a n t i c so fi n t e r m e d i a t el o g i c s b i ef i r s tr e v i e w e d t h e nw er e c a l lt h et o c h n o l o g yo fb i s i m u l a t i o n i nt h ee n do ft h i s c h a p t e r ，w er e d e f i n eg s d e ll o g i c s ，ac l a s so f w e l t - k n o w ni n t e r m e d i a t el o g i c s ，b yu s i n g k r i p k es e m a n t i c s w ew i l lc a r r ya l li n v e s t i g a t i o ni n t ot h ee x i s t e n c eo f s e v e r a lk i n d so f n o r m a lf o r m s i ni n t e r m e d i a t el o g i c si nc h a p t e r3 s o m en o r m a lf o r m sa n dm o d e l - c h a r a c t e r i z i n g f o r m u l a sf o rt h e s ea r ef i r s t l yd e f i n e d t h e nt h ef ! x i s t e n c eo ft h e s en o r m a lf o r m si n s o m ei n t e r m e d i a t el o g i c si ss t u d i e d i nt h ee n d w ew md i s c u s sh o wt op r o v et h a ta l o g i ci saw e a k e s ti n t e r m e d i a t el o g i cw h i c hi sr e d u c i b l et oa c e r t a i nn o m a lf o r m c h a p t e r4a r ec o n c e r n e dt h ep r o b l e mo fh e wt or e d u c s8 f o r m u l at oac e r t a i n n o r m a lf o r m t w ok i n d so fr e d u c t i o nm e t h o d s ，o n eo fw h i c hi sb a s e do nm o d e l - c h a r a c t e r i z i n gf o r m u l a sa n dt h eo t h e ro nr e w r i t i n gs y s t e m sa r ep r e s e n t e d a n dt h e c o m p l e x i t i e so fr e d u c t i o u sf o rt h e s en o m