摘要：本文提出一种处理带等词的horn逻辑的新方法——目标类型驱动法,它显式地把一致化操作看作目标,并且一致化操作并入归结过程之中。本方法的优点有:(1)把归结和一致化看作多类型目标的求解过程,减化了控制问题,可望提高系统的实现效率;(2)相应的推理机的系统结构,可以得到简化;(3)开发逻辑程序与或并行性的任何技术,同时可应用到一致化过程之中;(4)本方法可用来合成函数程序设计和逻辑程序设计;(5)本方法可用来处理无限数据结构。

摘要：一阶谓词逻辑下的horn逻辑是人工智能程序语言Prolog的理论基础,利用Prolog在计算机上可实现机械化,从而使自动化求解问题和定理证明具备可行性。本文从horn逻辑和Prolog的基础理论出发,使用horn子句、SLD-归结、搜索和回溯等原理讨论了如何在计算机中实现数学函数、定理证明等自动推理的一些应用。

摘要：ＰＲＯＬＯＧ是基于Ｈｏｒｎ逻辑的通用搜索系统，是一种方便、高效的逻辑设计工具，但该系统却不具有完备性。从其理论基础和运行方式两方面，对ＰＲＯＬＯＧ系统进行剖析，分析系统完备性受到破坏的原因是：在该系统中采用了深度优先搜索策略和引入了ＣＵＴ控制机制。最后，提出了增强系统完备性的方法。