| 0 前言 | 第1-8页 |
| 1 预备知识 | 第8-23页 |
| 1．1 一阶谓词演算的基本体系 | 第8-10页 |
| 1．1．1 概述 | 第8页 |
| 1．1．2 标准式的化简步骤 | 第8-9页 |
| 1．1．3 标准式的应用问题 | 第9-10页 |
| 1．2 归结原理 | 第10-16页 |
| 1．2．1 归结原理概述 | 第10-11页 |
| 1．2．2 命题逻辑的归结原理 | 第11页 |
| 1．2．3 一阶逻辑的归结原理 | 第11-16页 |
| 1．3 从归结证明树抽取信息 | 第16-23页 |
| 1．3．1 概述 | 第16页 |
| 1．3．2 Green的方法 | 第16-19页 |
| 1．3．3 Luckham的方法 | 第19-23页 |
| 2 从归结证明树抽取程序 | 第23-28页 |
| 2．1 术语介绍 | 第23页 |
| 2．2 抽取方法 | 第23-24页 |
| 2．3 举例 | 第24-28页 |
| 3 抽取算法的正确性证明 | 第28-35页 |
| 4 SKOLEM函数的消除 | 第35-40页 |
| 5 应用举例 | 第40-50页 |
| 5．1 程序综合 | 第40-46页 |
| 5．2 问题求解 | 第46-50页 |
| 6 总结与展望 | 第50-52页 |
| 6．1 总结 | 第50页 |
| 6．2 展望 | 第50-52页 |
| 致谢 | 第52-53页 |
| 参考文献 | 第53页 |