基于归结原理的程序综合设计与实现

论文摘要

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

论文目录

• 摘要
• Abstract
• 1 绪论
• 1.1 论文的研究背景
• 1.2 研究的目的和意义
• 1.3 相关历史回顾国内外研究现状
• 1.4 本文的主要研究内容和内容组织
• 2 预备知识
• 2.1 一阶谓词演算的基本体系
• 2.1.1 概述
• 2.1.2 标准式化简步骤
• 2.1.3 标准式应用问题
• 2.2 归结原理概述
• 2.3 命题逻辑的归结原理
• 2.4 一阶逻辑的归结原理
• 2.4.1 替换与合一替换
• 2.4.2 一阶逻辑中的归结原理
• 2.4.3 一阶逻辑中的归结过程
• 2.4.4 演绎树
• 2.5 归结策略
• 2.6 从归结证明树中抽取程序
• 2.6.1 从归结证明树中抽取程序概述
• 2.6.2 从归结证明树抽取程序
• 3 一阶公式的计算机内部表示及结构
• 3.1 输入规范
• 3.2 合一替换的内部表示以及相关操作
• 3.3 谓词的计算机内部表示
• 3.4 子句的内部表示和实现
• 3.4.1 子句类数据成员的定义
• 3.4.2 子句类数据成员的定义
• 3.5 子句集的内部表示及实现
• 3.5.1 子句集的功能
• 3.5.2 子句集的用到的常量
• 3.5.3 子句集的数据成员定义
• 3.5.4 子句集的操作
• 3.6 总结
• 4 归结原理实现
• 4.1 归结流程概述
• 4.2 子句的输入与新子句生成
• 4.3 归结控制
• 4.3.1 两个子句之间归结的控制流程
• 4.3.2 整体归结控制流程
• 4.4 子句间归结与新子句生成
• 4.4.1 MGU集合的计算
• 4.4.2 新子句的生成
• 4.5 总结
• 5 程序抽取过程实现
• 5.1 归结证明树的转化
• 5.2 从转化的归结证明树中抽取程序
• 5.3 总结
• 6 利用数学归纳法抽取循环程序
• 6.1 数学归纳法抽取循环程序方法
• 6.2 应用举例
• 6.3 总结
• 7 应用举例
• 7.1 问题描述
• 7.2 程序实现
• 结论
• 参考文献
• 附录A 程序内容列表
• 攻读硕士学位期间发表学术论文情况
• 致谢
• 大连理工大学学位论文版权使用授权书