基于归结原理的程序综合设计与实现
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 1 绪论 | 第7-11页 |
| 1．1 论文的研究背景 | 第7-8页 |
| 1．2 研究的目的和意义 | 第8页 |
| 1．3 相关历史回顾国内外研究现状 | 第8-9页 |
| 1．4 本文的主要研究内容和内容组织 | 第9-11页 |
| 2 预备知识 | 第11-22页 |
| 2．1 一阶谓词演算的基本体系 | 第11-13页 |
| 2．1．1 概述 | 第11页 |
| 2．1．2 标准式化简步骤 | 第11-12页 |
| 2．1．3 标准式应用问题 | 第12-13页 |
| 2．2 归结原理概述 | 第13页 |
| 2．3 命题逻辑的归结原理 | 第13-14页 |
| 2．4 一阶逻辑的归结原理 | 第14-18页 |
| 2．4．1 替换与合一替换 | 第14-15页 |
| 2．4．2 一阶逻辑中的归结原理 | 第15-16页 |
| 2．4．3 一阶逻辑中的归结过程 | 第16-17页 |
| 2．4．4 演绎树 | 第17-18页 |
| 2．5 归结策略 | 第18-19页 |
| 2．6 从归结证明树中抽取程序 | 第19-22页 |
| 2．6．1 从归结证明树中抽取程序概述 | 第19-20页 |
| 2．6．2 从归结证明树抽取程序 | 第20-22页 |
| 3 一阶公式的计算机内部表示及结构 | 第22-32页 |
| 3．1 输入规范 | 第22-24页 |
| 3．2 合一替换的内部表示以及相关操作 | 第24-25页 |
| 3．3 谓词的计算机内部表示 | 第25-27页 |
| 3．4 子句的内部表示和实现 | 第27-30页 |
| 3．4．1 子句类数据成员的定义 | 第28页 |
| 3．4．2 子句类数据成员的定义 | 第28-30页 |
| 3．5 子句集的内部表示及实现 | 第30-31页 |
| 3．5．1 子句集的功能 | 第30页 |
| 3．5．2 子句集的用到的常量 | 第30页 |
| 3．5．3 子句集的数据成员定义 | 第30-31页 |
| 3．5．4 子句集的操作 | 第31页 |
| 3．6 总结 | 第31-32页 |
| 4 归结原理实现 | 第32-44页 |
| 4．1 归结流程概述 | 第32-33页 |
| 4．2 子句的输入与新子句生成 | 第33-35页 |
| 4．3 归结控制 | 第35-39页 |
| 4．3．1 两个子句之间归结的控制流程 | 第35-36页 |
| 4．3．2 整体归结控制流程 | 第36-39页 |
| 4．4 子句间归结与新子句生成 | 第39-43页 |
| 4．4．1 MGU集合的计算 | 第40-42页 |
| 4．4．2 新子句的生成 | 第42-43页 |
| 4．5 总结 | 第43-44页 |
| 5 程序抽取过程实现 | 第44-50页 |
| 5．1 归结证明树的转化 | 第44-46页 |
| 5．2 从转化的归结证明树中抽取程序 | 第46-49页 |
| 5．3 总结 | 第49-50页 |
| 6 利用数学归纳法抽取循环程序 | 第50-54页 |
| 6．1 数学归纳法抽取循环程序方法 | 第50-51页 |
| 6．2 应用举例 | 第51-53页 |
| 6．3 总结 | 第53-54页 |
| 7 应用举例 | 第54-58页 |
| 7．1 问题描述 | 第54-55页 |
| 7．2 程序实现 | 第55-58页 |
| 结论 | 第58-60页 |
| 参考文献 | 第60-62页 |
| 附录A 程序内容列表 | 第62-65页 |
| 攻读硕士学位期间发表学术论文情况 | 第65-66页 |
| 致谢 | 第66-67页 |
| 大连理工大学学位论文版权使用授权书 | 第67页 |
