双线性函数的度量矩阵及二次型在Mizar语言下的实现

中文摘要	第1-5页
英文摘要	第5-8页
1 绪论	第8-10页
·数学问题计算机证明的发展历程	第8页
·Mizar系统简介	第8-9页
·课题研究的目的和意义	第9页
·课题研究的主要内容	第9-10页
2 Mizar语言	第10-21页
·Mizar文章结构	第10-12页
·Mizar语言的数据类型和关键字	第12-13页
·Mizar语言的数据类型	第12页
·Mizar语言的关键字	第12-13页
·Mizar语言系统中的定义模块	第13-15页
·定义类型的代表字符	第13-14页
·Mizar语言的数据类型	第14-15页
·Mizar语言系统的定理证明	第15-19页
·Mizar语言的数据类型	第15-18页
·一般命题的Mizar表述及证明格式和方法	第18-19页
·Mizar语言系统的安装	第19-20页
·Mizar语言系统的逻辑推理检验及优化命令	第20-21页
3 双线性函数的度量矩阵在Mizar语言下的实现	第21-42页
·预备知识	第21-22页
·双线性函数的度量矩阵在Mizar下的实现	第22-40页
·环境部设置	第22-24页
·双线性函数的度量矩阵在Mizar系统下的实现	第24-35页
·双线性函数的基本性质	第35-40页
·最终实现的Mizar形式	第40-42页
4 二次型的 Mizar 实现	第42-47页
·预备知识	第42-43页
·二次型的Mizar实现	第43-45页
·二次型在Mizar下的定义	第43-44页
·正定二次型、负定二次型等在Mizar下的实现	第44-45页
·正定矩阵和负定矩阵的Mizar实现	第45页
·实现的Mizar形式	第45-47页
总结与展望	第47-48页
参考文献	第48-51页
致谢	第51-52页
攻读学位期间发表的学术论文目录	第52-53页