中文摘要 | 第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页 |