基于谓词逻辑的归结原理研究

：基于谓词逻辑的归结原理是实现机器推理或自动推理的有效途径，利用它可以证明定理和提取问题答案。分析了基于谓词逻辑的归结原理的理论基础，并论述了将基于谓词逻辑的归结原理应用于定理证明和问题答案提取的方法及步骤。

谓词逻辑是在命题逻辑的基础上发展而来的，通过引入量词，它比命题逻辑能更有效地表示和求证复杂问题。谓词逻辑采用形式化语言系统，通过一定的推理规则和控制策略，研究前提和结论之间的蕴涵关系。谓词逻辑具有严格的理论基础，可以保证推理过程和结论的正确性，同时它的形式化语言接近人类的自然语言，容易为人类所理解和接受[1]。

经典的演绎推理系统具有证明过程自然、易于理解、推理规则丰富、推理过程灵活等优点，但也存在推理过程中容易产生组合爆炸、证明方法难以判定等缺点[2,3]。

Robinson[4]于1965 年借助演绎推理反证法的思想提出了归结原理，它是一种形式单一、处理规则简单，可以在机器上实现的逻辑推理技术。归结原理的提出，为人类提供了一种简单易行的方法实现定理的证明和问题的求解，使定理证明可以在机器上机械现实，是自动推理的重大突破[5,6]。

本文从理论基础、求证问题的方法及步骤方面对基于谓词逻辑的归结原理进行了研究。论文的组织结构如下：第2 节分析了基于谓词逻辑的归结原理的理论基础；第3 节讨论了将基于谓词逻辑的归结原理应用于定理证明和问题答案提取的方法及步骤；最后对全文进行了总结。

2. 基于谓词逻辑的归结原理的理论基础 2.1. 归结原理的基本思想 根据谓词公式和其对应的子句集在不可满足的意义下是等价的，为了证明谓词公式是不可满足的，可