| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-9页 |
| 1 绪论 | 第9-13页 |
| ·定理机器证明的历史及研究现状 | 第9-10页 |
| ·Mizar系统的历史和研究现状 | 第10-11页 |
| ·课题研究的主要内容 | 第11页 |
| ·课题研究的目的和意义 | 第11-13页 |
| 2 Mizar语言 | 第13-20页 |
| ·Mizar语言的安装和升级 | 第13页 |
| ·Mizar语言的安装 | 第13页 |
| ·Mizar语言的升级 | 第13页 |
| ·Mizar语言的基本词汇和表达符号 | 第13-15页 |
| ·Mizar语言的基本词汇 | 第14页 |
| ·Mizar系统的表达符号 | 第14-15页 |
| ·Mizar系统中的定义 | 第15-17页 |
| ·Voc文件 | 第15-16页 |
| ·定义分类 | 第16页 |
| ·重新定义 | 第16-17页 |
| ·Mizar系统中的证明方法 | 第17-18页 |
| ·Mizar系统的文章结构 | 第18页 |
| ·Mizar系统的优化及检测命 | 第18-20页 |
| 3 四元数混合运算的Mizar实现 | 第20-51页 |
| ·预备知识 | 第20-21页 |
| ·几个定义 | 第20-21页 |
| ·四元数的加减乘除运算 | 第21页 |
| ·四元数运算的基本法则 | 第21页 |
| ·四元数在Mizar中的表述 | 第21-22页 |
| ·环境部的设置 | 第22-23页 |
| ·四元数混合运算的Mizar实现 | 第23-51页 |
| ·Mizar系统中四元数的09,19和符号数 | 第23-28页 |
| ·四元数混合运算的Mizar实现 | 第28-40页 |
| ·四元数的几个定义和模的一些补充的Mizar实现 | 第40-45页 |
| ·四元数若干性质的Mizar实现 | 第45-50页 |
| ·本节最终检测结果 | 第50-51页 |
| 4 特殊函数的微分公式和洛尔定理运用的Mizar实现 | 第51-62页 |
| ·预备知识 | 第51页 |
| ·微分和洛尔定理在Mizar系统中的简单说明 | 第51页 |
| ·环境部的设置 | 第51-52页 |
| ·特殊函数微分公式的Mizar实现 | 第52-57页 |
| ·洛尔定理运用的Mizar实现 | 第57-61页 |
| ·本节最终检测结果 | 第61-62页 |
| 5 总结与展望 | 第62-63页 |
| 参考文献 | 第63-67页 |
| 致谢 | 第67-68页 |
| 攻读学位期间发表的学术论文目录 | 第68-69页 |