探析基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究

《探析基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学博士学位论文基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究姓名：李文江申请学位级别：博士专业：交通信息工程及控制指导教师：徐扬20021201西南交通大学博士研究生学位论文第iT摘要格是一类重要的代数结构，现实世界中的很多现象都可以用格来刻画，尤其是不可比较性。而建立在格上的格值逻辑系统把己有多值逻辑的链状真值域拓展到较一般的格上，既能处理全序性信息，又能处理非全序性信息，从而更有效地描述人类推理、判断和决策的不确定性。广义模态逻辑属哲学逻辑范畴，对于刻画事物的“势态”、人物的“情态”和过程的“时态”是一种十分有效的工具。本文在格值命题逻辑系统LP

2、(X)和格值一阶逻辑系统LF(X)的基础上，讨论了广义格值模态逻辑系统的语义及语法性质，并对其a一归结原理做了初步探讨，主要在下述三个方面取得了研究成果:第一部分:关于格值模态命题逻辑系统及其归结方法的研究在此部分，把模态算子N(必然)和P(可能)引入格值命题逻辑系统LP(X)，建立了新的格值模态命题逻辑系统LMP(X)，并研究了它的语义刻画及语法结构，证明了在此语义解释和语法框架下的系统仍是a一可靠的和协调的:在此基础上，进一步研究了基于格值模态命题逻辑系统LMP(X)的a一归结原理，给出了计算a一直接归结式和a一自归结式的规则，并总结出具体的归结方法.第二部分:关

3、于格值时态命题逻辑系统及其归结方法的研究此部分的主要工作是在格值命题逻辑系统LP(X)中引进时态算子E(曾经)、F(将会)及其对偶算子H(曾经总是)、G(将会总是)，提出了以时轴为语境的格值时态命题逻辑系统LTP(X)，并给出其具体的语义解释和语法结构，并讨论了它的一些性质，证明了该系统的可靠性和协调性。此外，研究了与时间有关的(a,t卜归结原理，给出了计算时态归结式的规则，并提出了时态归结的具体方法第三部分:关于格值模态一阶逻辑系统及其归结原理的研究第ii页西南交通大学博士研究生学位论文这一部分主要是在格值模态命题逻辑系统LMP(X)中引进量词和谓词，建立格值模态一

4、阶逻辑系统LMF(X)，并给出其语义解释和语法结构，证明了系统的可靠性和协调性;另外，为了判断公式的可满足性，‘定义了格值模态一阶公式的Skolem标准型和H-解释;在此基础上，对基于系统LMF(X)的a一归结原理进行了初步探讨.〔关键词〕格蕴涵代数广义格值模态逻辑定理自动证明归结原理西南交通大学博士研究生学位论文第iii页AbstractThelaticeisakindofimportantalgebraicstructure.Inourlife,manyphenomenacanbedescribedbylatice,especiallynon-comparabil

5、ity.Latice-valuedlogicsystembasedonlaticeextendslinearvaluedfieldofmulti-valuedlogictolatice,thusnotonlycandealwithorderinformation,butalsocandealwithnon-orderinformation,consequentlydescribetheuncertaintyofhumanreasoning,judginganddecision-makingmoreefectively.Generalizedmodallogicbelo

6、ngstophilosophylogiccategory.Itisaveryefectivetooltodescribethetendencyofthings,atitudeofpeopleandtenseofcourse.Basedonlattice-valuedpropositionallogicsystemLP(X)andlatice-valuedfirst-orderlogicsystemLF(X),theauthorstudiedsemanticandsyntaxpropertiesofgeneralizedlatice-valuedmodallogicsy

7、stem,andprobedintoa一resolutionprinciple.Thespecificcontentsareasfollows:PartOneTheStudyofLattice-valuedModalPropositionalLogicSystemandItsResolutionMethodInthispart,weintroducedmodaloperatorsN(necessary)andP(possible)intolattice-valuedpropositionallogicsystemLP(X),setupanewlatt