格值一阶逻辑中α-语义归结方法的相容性  

Comparability of α-semantic resolution metod based on lattice-valued first-order logic LF(X)

作　　者：张家锋[1] 徐扬[2] 曹发生 

机构地区：[1]贵州民族大学理学院,贵州贵阳550025 [2]西南交通大学智能控制开发中心,四川成都610031 [3]贵州工程应用技术学院理学院,贵州毕节551700

出　　处：《辽宁工程技术大学学报（自然科学版）》2016年第11期1335-1340,共6页Journal of Liaoning Technical University (Natural Science)

基　　金：国家自然科学基金项目(61305074);贵州省科学技术基金项目(黔科合J字LKB[2012]02号);贵州民族大学引进人才项目(15XRY006)

摘　　要：为优化基于格值逻辑的α-归结原理,将删除策略应用于α-语义归结方法,研究了基于格值逻辑的带有删除策略的α-语义归结方法.首先给出了带有删除策略的α-语义归结的完备性;接着,给出了带有删除策略的α-语义归结算法,并证明了该算法的可靠性和完备性;通过实例说明了该算法的可行性.For optimizing the α-resolution principle in lattice-valued logic,this paper applies the delete strategy to α-semantic resolution and investigates α-semantic resolution method with delete strategy in lattice-valued logic.The completeness of α-semantic resolution method with delete strategy is given.The α-semantic resolution algorithm is investigated and sound theorem and weak complete theorem of this semantic resolution algorithm are proved.The practicability effectiveness of α-semantic resolution algorithm is illustrated through an example.

关 键 词：自动推理 语义归结 删除策略 格值逻辑 相容性 

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