【作者】 马骏；

【导师】 徐扬；

【作者基本信息】 西南交通大学 ， 交通信息工程及控制， 2002， 博士

【摘要】 非经典逻辑的研究一直是人工智能领域中一个非常引人关注的研究方向。目前，基于非经典逻辑的自动定理证明理论和技术不断发展，并已得到许多应用。本文基于国内外许多学者的研究工作，对格蕴涵代数及以格蕴涵代数为真值域的格值逻辑系统中的归结方法进行了较系统深入的研究，主要在下述三个方面取得了研究成果： 一、关于格蕴涵代数的研究 1、讨论了格蕴涵代数中的余元问题，得到了寻找余元的一种通用有效方法； 2、证明了◇₅，◇₆，◇₇，◇₈和◇_8+k等几类特殊的分配格不能构成格蕴涵代数； 3、讨论了非链和非布尔型格蕴涵代数的结构特点，证明了只有唯一对偶原产的格蕴涵代数是链。 二、关于基于格蕴涵代数的格值逻辑系统自动推理的研究 1、分析了经典逻辑归结原理在语义和语法方面的特点，指出了格值归结方法和经典归结方法在语义及语法方面的异同； 2、给出了经典逻辑归结方法的一个代数化实现方案，从而将经典命题逻辑的归结问题转化为同余方程组解的判定问题； 3、研究了格值命题逻辑系统LP（X）中简单子句和复杂子句的归结问题，提出了基于蕴涵滤子的归结概念，构造了一种有效的归结方法，并证明了该归结方法的可靠性和完备性； 4、讨论了格值一阶逻辑系统SLF（X）中关于蕴涵滤子的归结概念和方法，提出了格值一阶逻辑归结原理的Skolem标准化，Herbrand域等概念，并讨论了它们的性质； 5、讨论了格值逻辑中直接使用经典逻辑归结方法的局限，提出了限制归结概念。 三、关于格值逻辑系统L_vp的研究第 n页 西南交通大学博士研究生学位论文 1、提出并研究了(（。，川－语义导出概念、逻辑公式集合保持…，q）－规则的慨念和条件； 2、分析了格值逻辑系统Kp中选取公理集合和推理规则的条件；提出并研究了与赋值相关的证明概念，证明了系统的可靠性定理、弱演绎定理； ：3、提出并研究了与赋值相关的逻辑公式集的协调性概念，证明了赋值下的协调性定理．更多还原

【Abstract】 The research ofnon－classical lope has always been a very attractive dlrec－ non of Artificial Intelligence．In recent years，theory and technology of automated theorenlprovinghased on non－classlcalloglcs are developingrapldlyand many automated theorem provers have been tised successfully In matllelnatlcs，engineer－ lug and other areas．Used Previous Internal and external outcome ofresearches In these direction for reference。the allthor stlldled the properties oflattlce Inl－ l）licatlon algebra and lattice－vallled logical systelll wltll trllth－valllesfield belllg a lattice lmpllcatlon algebra，andon the base ofwhich，the authordlscussed In de－ tails about the lattice－valued resolution principle oflattlce－valued logical system． The specific contents are s follows： Part One The Study of Lattice Implication Algebra On the basis of previous results of lattice implication algebra．the part（：on－ sists of＊theili＊lliereallwffollilli＊＊【＾、000taltal＊ fOllowingthree points： l．A lllethod ofconlputingthe colllplelllentary elemellt ofally one In alattlce implication algebra was discussed In details and a practicable approach was given． 2．The theorem was shown that lattice lmpllcatlon algebra can not be con－ Stl·lit：tAtl Off CAlt3lll SI＞eC181 dlstl’lhlltlV618tt1Ces；Sllf：h s《5．心6，心7，令8 3lidO8＋k． 3．The structural feature ofnon－chain－type and non－Boolean－algebratype lattice lmpllcatlon algebra was discussed and the result that ifa lattice implication algebrahas alld only has onedual atom then It Is a chain was proved． Part Two The Study of ReResolution Principle in L8ttice－v古ined Logic based on Lattice Implication Algebra Ill this P8ft；th6 3llthof d！SCilSS6d th6 f6SOI［ltlOll－b8S6d Ih6thod Of slltoinst6d f6Anolllllg．ThiS psft COliSIStS Ofth6 follOWlllg poilltS： 1．The semantical andsyntactlcalfeatures ofresolutlon－basedautomated reasoningln classical logic was analyzed．The difference on resolution－basediv Jgmethod between the classical logic and lattice-valued logic was discussed in details.2. A algebraical method about resolution-based automated reasoning in classical logic was given. That method translated the decidability of satisfiability of logical formula into the decidability of solution of congruence equation array.3. The resolution-based automated reasoning method of simple and complicate clause sets in LP(X) was discussed in details. The concept of resolution on filter was given and a practicable approach was attained. The soundness and weak completeness theorem of that method was proved.4. The concept and method of resolution on filter in lattice- valued first-order logic SLF(X] was discussed and the concepts and properties of Skolemlzation and Herbrand field in it was discussed too.5. The concept of constrained resolution was give after the analyzing of resolution-based method of classical logic in lattice-valued logic.Part Three The Study of Lattice- Valued Logical SystemIn this part, the author constructed a lattice- valued prepositional logical system Jz?,,p with the truth-field of it is a lattice implication algebra. This part consists of the following points:1 . The concepts and properties of (a, /3)-semantical implication were discussed; the concepts and condition of keeping (a, /3)-rule of lattice- valued logical formula were given too.2. The condition of choosing axioms and inference rule in ^fvp was analyzed.3. The concepts of proof under valuation and its properties were given. The soundness and weak deduction theorems were proved.4. The concepts of consistency of lattice-valued logical formula under valuation was given and the consistent theorem of it was proved also.更多还原