自动程序设计是计算机科学中的重要研究领域,在人工智能的自动规划、机器人学等分支有重要应用。在程序理论方面,程序综合与程序验证关系密切。程序综合就是从定理机器证明中抽取程序,即:为构造一个符合给定输入输出规范(通常表示为一组逻辑公式,例如一阶谓词公式)的程序,首先把程序设计问题转化为定理证明问题,然后从定理证明中抽取满足给定规范的程序。 对于形如(?)的定理证明问题,广义归结原理可以回答其是否为真,而对于“对每个确定的(?),(?)的值是什么?”这一经典的证明论问题,广义归结原理本身并没有给出解答。此前很多人研究从归结证明确定(?)的值的方法,但是由于他们的方法都不是从分析证明过程出发的,所以在很多情况下对问题的解不能做出很好的解释:只能完成顺序问题的求解,或者只能列出问题的可能解,却不能回答在任意给定条件下问题的解具体是什么。 这篇论文主要做了如下两项工作:第一,对于形如(?)的定理证明问题,本文从分析广义归结证明树的每个结点入手,提取广义归结证明的过程信息,生成问题求解程序。并且给出了所抽取出程序的部分正确性证明。这一方法的特点是:抽取算法所用的时间、空间复杂度与广义归结证明树包含结点数呈线性关系,并且抽取算法本身十分简单,易于实现。第二,对于形如(?)的定理证明问题,广义归结证明树中一般包含Skolem函数,而从这样的广义归结证明树中抽取的程序就可能包含Skolem函数。本文给出了是否能够抽取出不包含Skolem函数的程序的充分必要条件,同时给出了消除Skolem函数的算法。 本文给出的算法,主要适用于抽取顺序程序和分支程序,当定理是以递归形式给出时,也可以抽取递归程序。利用数学归纳法,使用本算法可以抽取循环程序。