| 摘要 | 第1-4页 |
| Abstract | 第4-9页 |
| 1 绪论 | 第9-13页 |
| ·数学命题的机械化证明的历史 | 第9-10页 |
| ·国内外研究动态 | 第10-11页 |
| ·Mizar系统的历史发展过程及现状 | 第11-13页 |
| ·Mizar系统概述 | 第11页 |
| ·Mizar系统的发展历史 | 第11-13页 |
| ·本文内容及安排 | 第13页 |
| 2 Mizsr系统简介 | 第13-26页 |
| ·Mizar论文结构 | 第13-15页 |
| ·Mizar语言的基本语法结构 | 第15-16页 |
| ·Mizar语言的数据类型 | 第15页 |
| ·Mizar语言的公式 | 第15-16页 |
| ·定理证明的方法 | 第16-21页 |
| ·简单依据 | 第16页 |
| ·证明方法 | 第16-19页 |
| ·数据类型的改变 | 第19页 |
| ·一些惯例 | 第19-20页 |
| ·连等于的使用 | 第20-21页 |
| ·扩散陈述 | 第21页 |
| ·模式 | 第21页 |
| ·定义 | 第21-26页 |
| ·词汇表文件的书写方法 | 第21-23页 |
| ·结构的定义 | 第23页 |
| ·mode的定义 | 第23-24页 |
| ·属性(attr)的定义 | 第24页 |
| ·cluster的定义 | 第24页 |
| ·谓词的定义 | 第24-25页 |
| ·函数的定义 | 第25页 |
| ·重定义 | 第25-26页 |
| 3 Mizsr数据库与系统 | 第26-28页 |
| ·Mizar数据库 | 第26页 |
| ·Mizar系统 | 第26-27页 |
| ·Mizar系统的安装 | 第27页 |
| ·Mizar系统中常用的几个命令 | 第27-28页 |
| 4 四元数及其性质在Mizar语言系统上的实现 | 第28-66页 |
| ·四元数的基本知识 | 第28-37页 |
| ·四元数的发现及应用 | 第28-29页 |
| ·四元数的定义、四元数的运算 | 第29-32页 |
| ·四元数的复数表示和相似关系 | 第32-34页 |
| ·四元数体 | 第34页 |
| ·四元数矩阵 | 第34-37页 |
| ·四元数、四元数的运算、模、共轭、内积及相关性质在Mizar系统上的实现 | 第37-43页 |
| ·环境部的设置和变量的声明 | 第37-38页 |
| ·四元数的定义 | 第38-39页 |
| ·虚数单位i,j,k在计算机上的定义 | 第39-42页 |
| ·如何让系统识别新定义的四元数数据类型 | 第42页 |
| ·四元数在计算机上的表示 | 第42-43页 |
| ·四元数的运算在Mizar系统上的实现 | 第43-50页 |
| ·四元数的加法 | 第43-45页 |
| ·四元书的相反数 | 第45-46页 |
| ·四元数的减法 | 第46页 |
| ·四元数的乘法 | 第46-47页 |
| ·四元数的除法 | 第47-49页 |
| ·四元数的逆 | 第49页 |
| ·虚数单位i,j,k在计算机上的表示 | 第49-50页 |
| ·实部和虚部的定义 | 第50-55页 |
| ·零元素和单位元 | 第55-56页 |
| ·一个重要定理的证明 | 第56-58页 |
| ·四元数运算的另一种表示 | 第58-62页 |
| ·四元数的加法 | 第58页 |
| ·四元数的相反数 | 第58页 |
| ·四元数的减法 | 第58-59页 |
| ·四元数的乘法 | 第59-60页 |
| ·四元数的除法 | 第60-61页 |
| ·四元数的逆 | 第61-62页 |
| ·四元数的共轭 | 第62-63页 |
| ·四元数的模 | 第63-64页 |
| ·四元数的内积 | 第64-65页 |
| ·最终实现的Mizar形式 | 第65-66页 |
| 5 四元数的代数结构在Mizar语言系统里的实现 | 第66-75页 |
| ·代数结构的组成与四元数的二元运算 | 第66-67页 |
| ·四元数群的代数结构的定义和证明 | 第67-70页 |
| ·四元数环的代数结构的定义和证明 | 第70-72页 |
| ·相关定理的证明 | 第72-73页 |
| ·四元数环中元素的共轭与模 | 第73-74页 |
| ·最终实现的Mizar形式 | 第74-75页 |
| 总结与展望 | 第75-77页 |
| 参考文献 | 第77-80页 |
| 致谢 | 第80-81页 |
| 攻读学位期间发表(完成)的学术论文目录 | 第81-82页 |