探索格值命题逻辑系统lp（x）中基于α-归结原理的自动推理方法的研究

《探索格值命题逻辑系统lp（x）中基于α-归结原理的自动推理方法的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学博士学位论文格值命题逻辑系统LP（X）中基于α-归结原理的自动推理方法的研究姓名：王伟申请学位级别：博士专业：交通信息工程及控制指导教师：徐扬2002.11.1西南交通太学研究然博士学雠仑文1摘要本交基于徐扬帮秦竞云秘美予格蕴涵代数和疆格蕴涵代数为冀僖域静辛箨值命题逻辑系统LP(X)的研究工作，对格蕴涵代数以及格值命题逻辑系统LP(X)孛基予技一羟结窳毽舞妻淤攘瑾方法遘嚣了慕统深入懿研究，主要鸯豁下覆穷瑟的研究成果：一、关予襁蕴涵健数静磷究1、对格蕴涵代数的格论性质进行了研究。得到了当五为完备格蕴涵代数嚣孛，关予v，A，

2、o运算静一些结果l2、对格蕴涵代数的窀幂等元进行了研究’证明了格蕴涵代数五可以分解为经簿—令发暴等嚣溪对应瓣左浃瓣夔德集会．每其霹褒棱熬誊秘{3、对格蕴涵代数的滤子的性质进行了研究，诚明了滤乎的结树相似于逻辑学中的Hypotheticalsyllogism规则秘替换悫理；4、给出了格骧涵代数中弱滤予躺概念，对弱滤予的性质个结构进行了研究^=、关予格值命慧逻辑系统LP(X)中8一巍动推璞方法的莽}竞可以科甩矩阵的列变揍对予旬集合的不可满足性进行判定。最羼，证甥了该方法静可靠髋稀完备馥；，5、对格值命蹶逻辑蓑统LP(X)中基予。一归缩原

3、理的。一自动推理方法i获嚣了臻究滞出了尾簿号矩箨表承一类餐攀秘广爻子每集食(灾含命题变嚣稀非正则1一IESF广义文字)的方法，把口一归结原理转换成矩阵的列变换．从ii西南交通大学研究生博士学位论文而，可以利用矩阵的列变换掰广义子句集合的。一不可满足性进行判定．最后证明了该方法的完备性．V关键词：智能控制，格蕴涵代数，对偶分子，滤子，格值命题逻辑，不可分极简式，。一归结域，不可满足性，梃可满足的l、西南交通大学研究生博士学位论文iiiAbstractBasedontheoutcomeofXuYangandQinKeyunaboutla

4、tticeimplicational-gebraandlattice-valuedpropositionallogicLP(X)withtruth-valueinalatticeim·plicationalgebra，theauthorstudiedthepropertiesoflatticeimplicationalgebraandthea-automatedreasoningmethodbasedona—resolutionprincipleofLP(X)．Thespecificcontentsareasfollows：TheS

5、tudyofLatticeImplicationAlgebraOnthebasisofpreviousresultsoflatticeimplicationalgebra，thispartconsistsofthefollowingthreepoints：1．SomepropertiesoflatticeimplicationalgebraLwerediscussed，andsomeimportantresultsweregivenifLwasacompletelatticeimplicationalgebra．2．Theprope

6、rtiesofleftidempotentelementsoflatticeimplicationalgebraswerediscussed，andtheconclusionthatlatticeimplicationalgebraLw∞equalsofthedi．rectedsumoftherangeanddualkernelofaleftmapconstructedbyaleftidempotentelementwasproved．3．Thepropertiesofthefiltersoflatticeimplicational

7、gebrawerediscussed，thetheoremwasshownthattheysatisfythehypotheticalsyllogismandsubstitutetheoremofthepropositionallogic．4．Theconceptofweakfiltersoflatticeimplicationalgebrasandtheirpropertiesandstructuresarediscussed．Itisprovedthatallweakfiltersofalatticeimplicationalg

8、ebraformatopologyandtheimplicationisomorphismbetweemtwolatticeimplicationalgebrasisatopologicalmappingbetweentheirtop