| 中文摘要 | 第1-5页 |
| 英文摘要 | 第5-9页 |
| 1、绪论 | 第9-17页 |
| ·数学问题机械化证明的历史及国内外发展现状 | 第9-12页 |
| ·Mizar 系统的发展历史和研究现状 | 第12-14页 |
| ·课题研究的目的和意义 | 第14-16页 |
| ·课题研究的主要内容 | 第16-17页 |
| 2 关于 Mizar | 第17-30页 |
| ·Mizar 的文化发展背景 | 第17-18页 |
| ·Mizar 系统简介 | 第18页 |
| ·Mizar 语言 | 第18-20页 |
| ·Mizar 语言的数据类型 | 第18-19页 |
| ·Mizar 语言中的逻辑符号 | 第19页 |
| ·Mizar 语言中的约定词汇 | 第19-20页 |
| ·免检符号 | 第20页 |
| ·Mizar 论文的结构构成 | 第20-23页 |
| ·总体结构 | 第21页 |
| ·环境部结构 | 第21-22页 |
| ·正文结构 | 第22-23页 |
| ·Mizar 系统中的定理证明 | 第23-25页 |
| ·Mizar 系统中的定义及其证明 | 第25-26页 |
| ·VOC 文件 | 第25-26页 |
| ·Mizar 系统中的定义 | 第26页 |
| ·Mizar 系统的安装与更新 | 第26-27页 |
| ·Mizar 系统的安装 | 第26-27页 |
| ·Mizar 系统的更新 | 第27页 |
| ·Mizar 论文的检测与优化 | 第27-30页 |
| ·Mizar 验证系统中的常用命令 | 第27页 |
| ·Mizar 论文的检测 | 第27-28页 |
| ·Mizar 论文的优化 | 第28-30页 |
| 3、环境部的设置 | 第30-33页 |
| ·DIFF_3 的环境部 | 第30-32页 |
| ·DIFF_4 的环境部 | 第32-33页 |
| 4、特殊函数的差分差商及差分差商的性质定理在 Mizar 系统下的实现 | 第33-68页 |
| ·差分与差商 | 第33-37页 |
| ·特殊函数的差分差商在Mizar 系统下的实现 | 第37-47页 |
| ·变量的声明 | 第37-38页 |
| ·特殊函数的差分差商在Mizar 中的表述 | 第38-47页 |
| ·差分差商有关性质的Mizar 实现 | 第47-52页 |
| ·零阶及高阶差分在Mizar 下的实现 | 第52-66页 |
| ·变量的声明 | 第52-53页 |
| ·零阶差分及高阶差分的定义 | 第53-54页 |
| ·零阶差分及高阶差分的有关性质 | 第54-61页 |
| ·差分的另一种表达 | 第61-64页 |
| ·连乘 | 第64-66页 |
| ·最终实现的Mizar 形式 | 第66-67页 |
| ·成果出处的Mizar 版本 | 第67-68页 |
| 总结与展望 | 第68-70页 |
| 参考文献 | 第70-73页 |
| 致谢 | 第73-74页 |
| 攻读学位期间发表的学术论文目录 | 第74-75页 |