摘要
基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑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.
出处
《计算机工程与应用》
CSCD
北大核心
2010年第23期18-20,49,共4页
Computer Engineering and Applications
基金
国家自然科学基金No.60474022
No.60875034
高等学校博士学科点专项科研基金项目No.20060613007~~
关键词
格值一阶逻辑
自动推理
α-归结原理
简单广义子句集
lattice-valued first-order logic
automated reasoning
α -resolution principle
simple generalized clause set
