广义上,程序设计过程就是定理证明过程,因而程序综合与机器定理证明关系密切。通过一般情况下,构造性的证明过程才能抽取程序。归结原理是一种反证法,人们早已知道可以从归结证明中抽取顺序程序,并且已经证明可以从归结证明树抽取分支程序。由于归结原理的反证法本质,不能保证其证明是构造性的,因此不能保证能够抽取循环程序,但是利用数学归纳法可以使用归结原理来抽取循环体,从而抽取循环程序。本文利用归结原理进行计算机定理证明,然后从归结证明树中抽取程序。 这篇论文主要做了如下工作:第一,用C/C++语言设计和实现基于归结原理的定理计算机证明系统,该系统能够证明一阶谓词逻辑公式,并构造归结证明树。第二,针对形如(?)(?)P((?),(?))的定理证明问题,设计并实现程序综合的程序,该程序可以从归结证明树中抽取程序,抽取的程序能够根据输入(?)计算输出(?)且满足P((?),(?))。该抽取程序的工作过程是变换归结证明树,从变换后的归结证明树的叶结点开始,向树根的方向逐个结点抽取程序,每个结点抽取的程序与其子结点抽取的程序和本身相关,最终根结点的程序就是计算输出(?)的程序。第三,本文阐述了如何利用数学归纳法抽取循环程序的方法,该方法能够从递归描述的问题中抽取循环程序。 本文的实现是考虑计算机资源限制的,并不对所有定理证明都能给予很好的解答,因此有些定理的程序可能无法抽取。本文提出了基于归结原理实现定理自动证明和程序抽取方面有待解决的问题,这些问题的解决将使得定理机器证明和程序综合从理论走向实用。