基于广义归结的程序综合

论文摘要

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

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 论文的研究背景
• 1.2 相关历史回顾及国内外研究现状
• 1.3 本文的主要研究内容及内容组织
• 2 预备知识
• 2.1 一阶谓词演算的基本体系
• 2.1.1 概述
• 2.1.2 标准式化简步骤
• 2.1.3 标准式应用问题
• 2.2 广义归结原理
• 2.2.1 广义归结原理概述
• 2.2.2 广义归结方法
• 2.2.3 广义归结证明树
• 2.2.4 降低广义归结方法复杂度策略
• 2.3 从广义归结证明树抽取信息
• 3 从广义归结证明树抽取信息
• 4 抽取算法的正确性证明
• 5 Skolem函数的消除
• 6 应用举例
• 6.1 程序综合
• 6.2 问题求解
• 结论
• 参考文献
• 攻读硕士学位期间发表学术论文情况
• 致谢
• 大连理工大学学位论文版权使用授权书