| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-8页 |
| 1 绪论 | 第8-12页 |
| ·机器证明的概念 | 第8页 |
| ·国内外研究现状 | 第8页 |
| ·Mizar系统的发展历史和研究现状 | 第8-9页 |
| ·课题研究的目的和意义 | 第9页 |
| ·课题研究的主要内容 | 第9-12页 |
| 2 Mizar概述 | 第12-20页 |
| ·Mizar语言 | 第12页 |
| ·Mizar语言的逻辑符号 | 第12页 |
| ·Mizar语言的数据类型 | 第12页 |
| ·Mizar文章结构 | 第12-14页 |
| ·Mizar基本命题表述词汇 | 第14-16页 |
| ·Mizar中定理证明的方法 | 第16-17页 |
| ·Mizar系统中的定义 | 第17-18页 |
| ·Mizar中的安装与更新 | 第18-19页 |
| ·Mizar系统自我验证的“人机对话”功能 | 第19-20页 |
| 3 线性空间中泛函的相关定义的Mizar实现及性质的论证 | 第20-33页 |
| ·环境部的设置和变量的声明 | 第20-22页 |
| ·泛函相关定义的Mizar表述 | 第22-29页 |
| ·泛函相关性质运算的Mi zar表述 | 第29-33页 |
| 4 对偶空间的定义及性质的Mizar实现 | 第33-51页 |
| ·对偶空间定义的Mizar实现 | 第33-45页 |
| ·对偶空间性质的Mizar实现 | 第45-49页 |
| ·最终实现的Mizar形式 | 第49-51页 |
| 总结与展望 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 致谢 | 第55-56页 |
| 攻读学位期间发表的学术论文目录 | 第56-57页 |