| 摘要 | 第1-4页 |
| 英文摘要 | 第4-7页 |
| 1 绪论 | 第7-11页 |
| ·数学问题计算机证明的历史及发展现状 | 第7页 |
| ·Mizar系统的历史和发展现状 | 第7-8页 |
| ·课题研究的目的和意义 | 第8-9页 |
| ·课题研究的主要内容 | 第9-11页 |
| 2 Mizar语言 | 第11-21页 |
| ·Mizar文章结构 | 第11-13页 |
| ·Mizar语言系统的基本符号和语法词汇 | 第13-14页 |
| ·Mizar语言系统的证明方法 | 第14-18页 |
| ·Mizar语言系统中的定义 | 第18-21页 |
| 3 粗糙子群性质的计算机证明 | 第21-37页 |
| ·预备知识分析 | 第21-22页 |
| ·群的粗糙子集与粗糙子群性质的计算机证明 | 第22-35页 |
| ·群的子集关于子群的上、下近似的Mizar定义 | 第22-24页 |
| ·群的子集关于子群的上、下近似的性质 | 第24-27页 |
| ·群的子集关于子群的二重近似 | 第27-30页 |
| ·群的子群关于子群的上、下近似的计算机证明 | 第30-34页 |
| ·群的子群关于正规子群的二重近似 | 第34-35页 |
| ·最终实现的Mizar形式及成果出处的Mizar版本 | 第35-37页 |
| 4 幂零群性质的计算机证明 | 第37-49页 |
| ·预备知识分析 | 第37-38页 |
| ·幂零群性质的计算机证明 | 第38-47页 |
| ·环境部设置 | 第38页 |
| ·正文部分 | 第38-47页 |
| ·最终实现的Mizar形式及成果出处的Mizar版本 | 第47-49页 |
| 5 p-群性质的计算机证明 | 第49-57页 |
| ·预备知识分析 | 第49页 |
| ·p-群与p-交换群性质的计算机证明 | 第49-55页 |
| ·p-元素与p-群性质的计算机证明 | 第49-52页 |
| ·p-群幂指数的计算机证明 | 第52-53页 |
| ·p-交换群的计算机证明 | 第53-55页 |
| ·最终实现的Mizar形式及成果出处的Mizar版本 | 第55-57页 |
| 总结与展望 | 第57-58页 |
| 参考文献 | 第58-61页 |
| 致谢 | 第61-62页 |
| 攻读学位期间发表的学术论文目录 | 第62-64页 |
