格值一阶逻辑LF(X)中的α-语义归结方法  

α-Semantic Resolution Method Based on Lattice-valued First-order Logic LF(X)

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

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

出　　处：《计算机科学》2014年第9期274-278,共5页Computer Science

基　　金：国家自然科学基金资助项目(61175055);四川省科技支撑计划项目(2011FZ0051);贵州省科学技术基金项目(黔科合J字LKB[2012]02号)资助

摘　　要：自动推理是人工智能的一个重要研究方向,基于归结原理的自动推理因易于在计算机上实现而得到广泛研究。语义归结是对归结原理的一种改进,它利用限制参与归结子句类型和归结文字顺序的方法来提高推理效率。为了提高基于格蕴涵代数的格值逻辑的α-归结原理的效率,将语义归结策略应用于α-归结原理。首先给出了格值一阶逻辑系统中的α-语义归结概念和α-语义归结演绎概念,接着讨论了格值一阶逻辑系统的α-语义归结方法,并证明了其可靠性和条件完备性,最后通过实例说明了其有效性。Automated reasoning is one of the most important research directions in artificial intelligence. Resolution- based automated reasoning has been extensively studied because of its easy implement on computer. Semantic resolution method is one of the most important modified methods for resolution principle in semantic resolution method, and it utilizes the technology that restrains 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. For improving the efficiency of α-resolution principle in lattice-valued logic based on lattice implication algebra, we applied the semantic resolution strategy to α-resolution principle. Firstly, this paper gave the conceptions of a-semantic resolution and α-semantic resolution deduction in LF（X）. Subsequently, the semantic resolution method on it was investigated and sound theorem and conditional complete theorem of this semantic resolution method were proved. At last, the effectiveness of α-semantic resolution method was illustrated through an example.

关 键 词：自动推理 语义归结 格值逻辑 格蕴涵代数 

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