| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 1 绪论 | 第7-15页 |
| ·数学机械化的发展过程 | 第7-10页 |
| ·Mizar系统的历史和发展现状 | 第10-13页 |
| ·课题研究的目的和意义 | 第13-14页 |
| ·课题研究的主要内容 | 第14-15页 |
| 2 Mizar语言 | 第15-31页 |
| ·Mizar系统的安装 | 第15页 |
| ·Mizar文章结构 | 第15-17页 |
| ·Mizar语言的基本符号和语法词汇 | 第17-20页 |
| ·基本符号 | 第17页 |
| ·基本语法词汇 | 第17-20页 |
| ·Mizar语言的证明方法 | 第20-23页 |
| ·Mizar语言的一般表述与证明格式 | 第20-22页 |
| ·基本证明方法 | 第22-23页 |
| ·Mizar语言系统中的定义(Definition) | 第23-28页 |
| ·Mizar中的逻辑推理检验及优化命令 | 第28-30页 |
| ·Mizar系统的人机对话功能 | 第30-31页 |
| 3 BCI-代数理想的Mizar实现 | 第31-33页 |
| ·BCI-代数理想 | 第31页 |
| ·BCI-代数理想的Mizar实现 | 第31-33页 |
| 4 几类特殊BCI理想的定义 | 第33-38页 |
| ·p-理想定义的Mizar实现 | 第33-34页 |
| ·结合理想定义的Mizar实现 | 第34-35页 |
| ·可换理想定义的Mizar实现 | 第35-36页 |
| ·关联理想及正定关联理想定义的Mizar实现 | 第36-38页 |
| 5 几类特殊BCI理想的性质 | 第38-44页 |
| ·p-理想的相关性质定理的Mizar实现 | 第38页 |
| ·结合理想及拟结合理想的相关性质定理的Mizar实现 | 第38-40页 |
| ·结合理想的相关性质的Mizar实现 | 第38-39页 |
| ·拟结合理想的相关性质的Mizar实现 | 第39-40页 |
| ·可换理想相关性质定理的Mizar实现 | 第40-41页 |
| ·关联理想及正定关联理想的相关性质定理的Mizar实现 | 第41-42页 |
| ·闭理想的Mizar实现 | 第42-43页 |
| ·最终实现的Mizar形式 | 第43-44页 |
| 结论与展望 | 第44-46页 |
| 参考文献 | 第46-49页 |
| 致谢 | 第49-50页 |
| 攻读学位期间发表的学术论文目录 | 第50-51页 |
