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

摘要：

基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一.针对格值一阶逻辑LF(X)中归结自动推理问题,以格值一阶逻辑LF(X)的α-归结原理为理论基础,通过对例子进行分析,提出了LF(X)中简单广义子句集的归结自动推理算法,并证明了该算法的可靠性和完备性.

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

所属期刊栏目：46

分类号：TP301.6(计算技术、计算机技术)

资助基金：国家自然科学基金the National Natural Science Foundation of China under Crant 60474022,60875034;高等学校博士学科点专项科研基金项目20060613007

在线出版日期：2010-11-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：18-20,49