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