| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第一章 绪论 | 第12-20页 |
| ·数学机械化简介 | 第12-15页 |
| ·数学机械化与计算机辅助证明 | 第15-16页 |
| ·论文的选题和主要工作 | 第16-20页 |
| 第二章 Isabelle的介绍 | 第20-30页 |
| ·Isabelle与LCF的发展历程 | 第20-21页 |
| ·Isabelle的理论基础 | 第21-26页 |
| ·使用Isabelle进行定理机器证明 | 第26-29页 |
| ·小结 | 第29-30页 |
| 第三章 基于Isabelle的一般拓扑学机械化 | 第30-70页 |
| ·拓扑空间的形式化及相关定理的机器证明 | 第30-46页 |
| ·Kuratowski闭包算子的形式化和Kuratowski定理的机器证明 | 第46-55页 |
| ·连续函数的形式化及黏结引理的机器证明 | 第55-61页 |
| ·导集的形式化及杨忠道定理的机器证明 | 第61-69页 |
| ·小结 | 第69-70页 |
| 第四章 基于Isabelle的拓扑动力系统机械化 | 第70-84页 |
| ·群论的形式化及相关定理的机器证明 | 第70-75页 |
| ·拓扑变换群和拓扑动力系统的形式化 | 第75-79页 |
| ·不变集的形式化及相关定理机器证明 | 第79-83页 |
| ·小结 | 第83-84页 |
| 第五章 IsabelleHelper自动定理证明工具 | 第84-110页 |
| ·IsabelleHelper的总体架构 | 第85-87页 |
| ·Isabelle引擎接口 | 第87-90页 |
| ·数学对象的符号表示 | 第90-96页 |
| ·基于知识的定理证明策略的研究 | 第96-102页 |
| ·Isabelle与Maple的集成 | 第102-109页 |
| ·小结 | 第109-110页 |
| 第六章 总结与展望 | 第110-112页 |
| 附录A 常用数学符号对照表 | 第112-114页 |
| 附录B type和term的XML Schema定义 | 第114-118页 |
| B.1 type的XML Schema定义 | 第114-115页 |
| B.2 term的的XML Schema定义 | 第115-118页 |
| 参考文献 | 第118-130页 |
| 攻读博士学位期间发表论文和参与科研情况 | 第130-132页 |
| 致谢 | 第132页 |
