| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-9页 |
| 1 绪论 | 第9-16页 |
| ·数学机械化的历史及发展现状 | 第9-10页 |
| ·国内外研究现状 | 第10-11页 |
| ·Mizar系统的发展历史和研究现状 | 第11-13页 |
| ·课题研究的目的和意义 | 第13-14页 |
| ·课题研究的主要内容 | 第14-16页 |
| 2 Mizar系统概述 | 第16-25页 |
| ·Mizar系统简介 | 第16页 |
| ·Mizar语言 | 第16-17页 |
| ·Mizar文章结构 | 第17-19页 |
| ·Mizar基本命题表述词汇 | 第19页 |
| ·Mizar中定理证明的方法 | 第19-21页 |
| ·Mizar语言中命题表述的一般形式 | 第19-20页 |
| ·基本证明方法 | 第20-21页 |
| ·Mizar系统中的定义 | 第21-25页 |
| ·模式定义 | 第21-22页 |
| ·谓词定义 | 第22页 |
| ·算子定义 | 第22-23页 |
| ·属性定义 | 第23页 |
| ·cluster定义 | 第23-24页 |
| ·结构定义 | 第24页 |
| ·重新定义 | 第24-25页 |
| 3 二元函数偏微分的Mizar实现 | 第25-48页 |
| ·二元函数偏微分的基本知识 | 第25-27页 |
| ·二元函数偏微分的的Mizar实现及其性质的论证 | 第27-45页 |
| ·环境部的设置和变量的声明 | 第27-28页 |
| ·二元函数偏微分的Mizar表述 | 第28-43页 |
| ·二元函数偏微分性质定理在Mizar中的实现 | 第43-45页 |
| ·最终实现的Mizar形式 | 第45-47页 |
| ·成果出处的Mizar版本 | 第47-48页 |
| 4 函数高阶偏微分的Mizar实现 | 第48-65页 |
| ·实现函数高阶偏微分的指导思想 | 第48页 |
| ·二阶偏微分的Mizar实现及相关性质的讨论 | 第48-63页 |
| ·在Mizar系统下定义函数的二阶偏微分 | 第48-58页 |
| ·函数二阶偏微分的性质定理在Mizar中的实现 | 第58-63页 |
| ·最终实现的Mizar形式 | 第63-64页 |
| ·成果出处的Mizar版本 | 第64-65页 |
| 5 三元函数的偏微分及梯度、散度、旋度的Mizar实现 | 第65-85页 |
| ·预备知识 | 第65-69页 |
| ·梯度 | 第65-67页 |
| ·散度 | 第67-68页 |
| ·旋度 | 第68-69页 |
| ·关于三元函数偏微分的Mizar实现 | 第69-74页 |
| ·三维欧氏空间下的预备说明 | 第69-70页 |
| ·三元函数偏微分的Mizar实现 | 第70-73页 |
| ·三元函数偏微分性质的Mizar实现 | 第73-74页 |
| ·梯度、散度、旋度在Mizar系统下的实现 | 第74-84页 |
| ·梯度与方向导数的Mizar实现 | 第74-81页 |
| ·矢量场函数与散度、旋度的Mizar实现 | 第81-84页 |
| ·最终实现的Mizar形式 | 第84-85页 |
| 总结与展望 | 第85-87页 |
| 参考文献 | 第87-91页 |
| 致谢 | 第91-92页 |
| 攻读学位期间发表(完成)的学术论文目录 | 第92-93页 |