| 中文摘要 | 第1-4页 |
| 英文摘要 | 第4-7页 |
| 1 绪论 | 第7-14页 |
| ·定理机器证明(Automated Theorem Proving)的历史及研究现状 | 第7-10页 |
| ·Mizar 系统的历史和发展现状 | 第10-12页 |
| ·课题研究的目的和意义 | 第12-13页 |
| ·课题研究的主要内容 | 第13-14页 |
| 2 Mizar 语言 | 第14-28页 |
| ·Mizar 语言 | 第14页 |
| ·Mizar 文章结构 | 第14-17页 |
| ·Mizar 语言的基本表达符号与基本语法词汇 | 第17-20页 |
| ·Mizar 语言的基本表达符号 | 第17页 |
| ·Mizar 语言的基本语法词汇 | 第17-20页 |
| ·Mizar 系统的证明方法 | 第20-24页 |
| ·一般表述与证明格式 | 第21-22页 |
| ·基本证明方法 | 第22-23页 |
| ·特殊命题的证明方法 | 第23-24页 |
| ·Mizar 语言中的定义(Definition) | 第24-26页 |
| ·Mizar 系统的逻辑推理检验及优化命令 | 第26-27页 |
| ·Mizar 语言系统的更新升级 | 第27-28页 |
| 3 特殊函数差分差商的Mizar实现 | 第28-40页 |
| ·特殊函数的差分差商 | 第28页 |
| ·特殊函数差分差商的 Mizar 实现 | 第28-38页 |
| ·特殊函数差分差商的环境部设置与变量声明 | 第28-29页 |
| ·特殊函数差分差商的 Mizar 表述与实现 | 第29-33页 |
| ·特殊函数差分差商的 Mizar 证明 | 第33-38页 |
| ·Mizar 实现的最终形式 | 第38-39页 |
| ·成果出处 | 第39-40页 |
| 4 特殊函数积分的 Mizar 实现 | 第40-57页 |
| ·积分公式 | 第40页 |
| 4 2 函数积分的 Mizar 实现 | 第40-55页 |
| ·特殊函数积分的环境部设置与变量声明 | 第40-42页 |
| ·特殊函数积分的 Mizar 表述与实现 | 第42-45页 |
| ·特殊函数积分的 Mizar 证明 | 第45-55页 |
| ·Mizar 实现的最终形式 | 第55-56页 |
| ·成果出处 | 第56-57页 |
| 5 函数正交性与函数范数的 Mizar 实现与论证 | 第57-70页 |
| ·函数正交性与函数范数 | 第57-59页 |
| ·函数正交性及性质 | 第57-58页 |
| ·函数范数及性质 | 第58-59页 |
| ·函数正交性与函数范数的 Mizar 实现 | 第59-68页 |
| ·函数正交性、函数范数的环境部设置与变量声明 | 第59-60页 |
| ·函数正交性的 Mizar 实现 | 第60-66页 |
| ·函数范数的 Mizar 实现 | 第66-68页 |
| ·Mizar 实现的最终形式 | 第68-69页 |
| ·成果出处 | 第69-70页 |
| 总结与展望 | 第70-72页 |
| 参考文献 | 第72-76页 |
| 致谢 | 第76-77页 |
| 攻读学位期间发表的学术论文目录 | 第77-79页 |
