| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-7页 |
| 第一章 绪论 | 第7-9页 |
| ·论文的研究背景 | 第7-8页 |
| ·问题的提出 | 第8页 |
| ·主要工作 | 第8页 |
| ·论文提纲 | 第8-9页 |
| 第二章 定理机器证明简介 | 第9-14页 |
| ·定理机器证明 | 第9页 |
| ·定理机器证明的研究概况 | 第9-13页 |
| ·定理证明器的分类 | 第13-14页 |
| 第三章 Isabelle简介 | 第14-31页 |
| ·Isabelle系统结构 | 第14-20页 |
| ·ML语言 | 第15-17页 |
| ·Isabelle的逻辑 | 第17-18页 |
| ·提升规则(lifting rule) | 第18-20页 |
| ·Isabelle定理证明方法 | 第20-23页 |
| ·Isabelle证明理论 | 第23-25页 |
| ·Isabelle的策略和策略算子 | 第25-31页 |
| 第四章 自动化证明策略的设计和实现 | 第31-54页 |
| ·系统结构 | 第31-43页 |
| ·用户接口 | 第43-46页 |
| ·算法设计 | 第46-54页 |
| 第五章 总结与展望 | 第54-58页 |
| 致谢 | 第58页 |