格值语义归结推理方法  

Lattice-valued Semantic Resolution Reasoning Method

作　　者：张家锋[1,2] 徐扬[1] 何星星[1] 

机构地区：[1]西南交通大学智能控制开发中心,成都610031 [2]毕节学院逻辑语言与认知中心,毕节551700

出　　处：《计算机科学》2011年第9期201-203,210,共4页Computer Science

基　　金：国家自然科学基金(60875034);贵州省科学技术项目(2010GZ43286);2011年西南交通大学博士生创新基金项目资助

摘　　要：归结自动推理是人工智能领域的一个重要研究方向,语义归结方法是对归结原理的一种改进,它利用限制参与归结子句类型和归结文字顺序的方法来提高推理效率。基于格蕴涵代数的格值逻辑系统的α-归结原理提供了一种处理带有模糊性和不可比较性信息的工具,它能对格值逻辑系统中在一定真值水平下的不可满足逻辑公式给出反驳证明。首先研究了格值逻辑系统上一类广义子句集的性质,该类子句集在任意赋值下能分为两个非空子集,接着讨论了这类广义子句集的语义归结方法,并证明了其可靠性和完备性。Resolution-based automated reasoning is one of most important research directions in AI,semantic method is one of the most important reform methods for resolution principle,in semantic resolution method,it utilizes the techno-logy restraining the type of clauses and the order of literals participated in resolution procedure to reduce the redundant clauses,and can improve the efficiency of reasoning,α-resolution principle on lattice-valued logic based on lattice implication algebra provides a alternative tool to handle the automated reasoning problem with uncomparability and fuzziness information.It can refutably prove the unsatisfiability of logical formulae in lattice-valued logic system.Firstly,this paper discussed the property of one class of generalized clause set on lattice-valued propositional logic LP（X）,this genera-lized clause set can be divided into two non-empty sets,the semantic resolution method on it was investigated and sound theorem and weak complete theorem of this semantic resolution method were proved.

关 键 词：格蕴涵代数 格值命题逻辑系统LP(X) 自动推理 语义归结方法 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]