基于谓词逻辑的Prolog程序设计

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