| 原创性声明 | 第1-3页 |
| 关于学位论文使用授权的声明 | 第3-4页 |
| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-7页 |
| 第一章 研究背景 | 第7-10页 |
| 1．1 背景简介 | 第7-8页 |
| 1．2 问题的提出 | 第8页 |
| 1．3 论文的主要工作 | 第8-9页 |
| 1．4 论文结构 | 第9-10页 |
| 第二章 机器定理证明简介 | 第10-24页 |
| 2．1 定理证明的基本方法及搜索问题 | 第10-14页 |
| 2．2 并行定理证明概况 | 第14-16页 |
| 2．3 Isabelle简介 | 第16-24页 |
| 第三章 系统的总体结构 | 第24-40页 |
| 3．1 并行证明环境的总体结构 | 第24-28页 |
| 3．2 并行证明环境的通信结构 | 第28-40页 |
| 第四章 并行策略的设计和实现 | 第40-51页 |
| 4．1 策略管理语言 | 第40-41页 |
| 4．2 blast并行策略 | 第41-42页 |
| 4．3 并行证明策略 | 第42-43页 |
| 4．4 OR并行策略 | 第43-47页 |
| 4．5 并行搜索策略 | 第47-51页 |
| 第五章 将来的工作 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 致谢 | 第55页 |