基于格值一阶逻辑LF(X)的自动推理算法  

Automated reasoning algorithm based on lattice-valued first-order logic LF(X)

作　　者：李晓冰[1] 徐扬[2] 

机构地区：[1]东北财经大学管理科学与工程学院,辽宁大连116025 [2]西南交通大学智能控制开发中心,成都610031

出　　处：《计算机工程与应用》2010年第23期18-20,49,共4页Computer Engineering and Applications

基　　金：国家自然科学基金No.60474022;No.60875034;高等学校博士学科点专项科研基金项目No.20060613007~~

摘　　要：基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑LF(X)中归结自动推理问题,以格值一阶逻辑LF(X)的α-归结原理为理论基础,通过对例子进行分析,提出了LF(X)中简单广义子句集的归结自动推理算法,并证明了该算法的可靠性和完备性。Resolution reasoning method based on predicate logic is one of methods which are well-developed and can be implemented on computer.In order to solve automated reasoning based on resolution principle in lattice-valued first-order logic,a resolution automated reasoning algorithm based on α-resolution principle in lattice-valued first-order logic is proposed by analyzing an example.Its soundness and completeness are proved.

关 键 词：格值一阶逻辑 自动推理 α-归结原理 简单广义子句集 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]