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