| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-8页 |
| 1 绪论 | 第8-14页 |
| ·Mizar 系统的发展历史 | 第8-10页 |
| ·Mizar论文简介 | 第10-12页 |
| ·论文结构 | 第10页 |
| ·环境部 | 第10-11页 |
| ·正文部分 | 第11页 |
| ·语言的综合使用 | 第11-12页 |
| ·课题研究的主要内容 | 第12页 |
| ·课题研究的目的和意义 | 第12-14页 |
| 2 向量函数的Mizar实现 | 第14-24页 |
| ·预备知识 | 第14-15页 |
| ·向量函数定义的Mizar实现及其性质的证明 | 第15-24页 |
| ·环境部的设置和变量的声明 | 第15-16页 |
| ·向量函数定义的Mizar实现 | 第16-18页 |
| ·向量函数有关性质的Mizar实现 | 第18-22页 |
| ·向量函数有关命题的Mizar表述 | 第22-24页 |
| 3 向量函数微分的计算机证明 | 第24-39页 |
| ·预备知识 | 第24-25页 |
| ·向量函数微分的定义和基本公式的Mizar实现 | 第25-39页 |
| ·向量函数微分的Mizar定义 | 第25-26页 |
| ·向量函数微分公式的Mizar实现 | 第26-39页 |
| 4 向量函数偏微分的Mizar证明 | 第39-48页 |
| ·实现向量函数偏微分的指导思想 | 第39页 |
| ·向量函数偏微分的 Mizar 实现及基本公式的计算机证明 | 第39-48页 |
| ·环境部的设置和变量的声明 | 第39-40页 |
| ·向量函数偏微分在Mizar系统中的定义 | 第40-41页 |
| ·向量函数偏微分基本公式的Mizar证明 | 第41-48页 |
| 总结与展望 | 第48-49页 |
| 参考文献 | 第49-52页 |
| 致谢 | 第52-53页 |
| 攻读学位期间发表(完成)的学术论文目录 | 第53-54页 |