| 中文摘要 | 第1-6页 |
| Abstract | 第6-14页 |
| 第一章 绪论 | 第14-26页 |
| ·几何定理可读机器证明研究的历史与现状概述 | 第14-21页 |
| ·几何不变量方法 | 第15-20页 |
| ·基于数据库的搜索法 | 第20-21页 |
| ·几何代数发展概述 | 第21-24页 |
| ·什么是几何代数 | 第21页 |
| ·已有的几何代数 | 第21-22页 |
| ·作为几何代数的向量几何和质点几何 | 第22-24页 |
| ·本文内容概述 | 第24-26页 |
| 第二章 几何代数基础新视角 | 第26-38页 |
| ·欧氏平面点集上“平等”的加法 | 第27-28页 |
| ·加法在Ω_1 上的确定 | 第28-34页 |
| ·将Ω_1 扩充为阿贝尔群 | 第34-37页 |
| ·第二章小结 | 第37-38页 |
| 第三章 质点几何的可读机器证明——希尔伯特交点类命题 | 第38-66页 |
| ·实系数质点几何初步 | 第38-47页 |
| ·实系数质点几何的基本原理 | 第39-41页 |
| ·实系数质点几何解题的例子 | 第41-44页 |
| ·实系数质点几何的消点方法 | 第44-47页 |
| ·实系数质点几何方法描述 | 第47-51页 |
| ·希尔伯特交点类命题的构图语句 | 第47-49页 |
| ·结论的形式和检验语句 | 第49-51页 |
| ·消点算法MPM 的实现 | 第51-58页 |
| ·MPM 的设计思想 | 第51页 |
| ·MPM 的完全性 | 第51-52页 |
| ·MPM 的结构 | 第52-58页 |
| ·算法MPM 的Maple 实现及例子 | 第58-63页 |
| ·MPM的Maple实现 | 第58-59页 |
| ·运行希尔伯特交点类命题的例子 | 第59-63页 |
| ·第三章小结 | 第63-66页 |
| 第四章 质点几何的可读机器证明——线性构造型几何命题 | 第66-128页 |
| ·复系数质点几何 | 第66-85页 |
| ·复系数质点几何的基本思想 | 第66-68页 |
| ·复系数质点几何的基本性质 | 第68-72页 |
| ·复系数质点几何解题的例子 | 第72-80页 |
| ·复系数质点几何的消点方法 | 第80-85页 |
| ·复系数质点几何方法描述 | 第85-92页 |
| ·线性构造型几何命题的构图语句 | 第85-89页 |
| ·结论的形式和检验语句 | 第89-92页 |
| ·消点算法CMPM 的实现 | 第92-108页 |
| ·CMPM 的设计思想 | 第92-93页 |
| ·CMPM 的完全性 | 第93-94页 |
| ·CMPM 的结构 | 第94-108页 |
| ·算法CMPM 的Maple 实现及例子 | 第108-121页 |
| ·CMPM 的Maple 实现 | 第108-109页 |
| ·运行线性构造型几何命题的例子 | 第109-121页 |
| ·算法 CMPM 与 MPM 的比较 | 第121-124页 |
| ·质点法与面积法初步比较 | 第124-125页 |
| ·第四章小结 | 第125-128页 |
| 第五章 总结与展望 | 第128-132页 |
| ·总结 | 第128-130页 |
| ·经验数据统计 | 第128-129页 |
| ·本文工作总结 | 第129-130页 |
| ·进一步的问题和拟开展的工作 | 第130-132页 |
| ·几何代数基础方面 | 第130页 |
| ·基于质点几何的可读机器证明方面 | 第130-132页 |
| 参考文献 | 第132-140页 |
| 攻读博士学位期间发表的学术论文 | 第140-141页 |
| 致谢 | 第141页 |