HORN集上基于广义归结方法的定理机器证明  

作　　者：戴望州[1] 

机构地区：[1]西北工业大学理学院应用数学系,陕西西安710126

出　　处：《湘潭师范学院学报（自然科学版）》2009年第1期31-34,共4页Journal of Xiangtan Normal University (Natural Science Edition)

摘　　要：设计了一个Horn集上基于广义归结方法的定理机器证明系统。在算法中使用广度优先与深度优先结合避免了传统归结的组合爆炸。分析了该系统的优缺点,在前人研究的基础上地提出了几点优化的建议。

关 键 词：广义归结 HORN集 机器证明 

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