基于Mizar的特殊函数积分及简化剩余系的研究

摘要

Mizar系统起源于数学定理的机械化证明，它是用于证明和计算数学问题的计算机语言系统，专门用来构建Mizar数学知识库的自动推理校验。Mizar系统拥有世界上最大的数学数据库(MML)，其中已经收录1126篇文章，2万多个数学概念，40多万条数学定理，几乎涵盖了数学科学的各个分支。当前，Mizar系统已经从单一定理证明发展到多学科多方面的交叉应用，特别是在自动控制、声音和图像识别等研究领域有着更为广泛的应用。
　　 本文首先介绍了数学机械化证明的历史及国内外研究现状，其次介绍了Mizar系统的发展历程和研究。基于数学定理的机器证明和数学定理自动推理系统Mizar，对一些特殊函数类积分问题和数论中的简化剩余系问题进行了Mizar表述和推证，且通过了Mizar系统验证。主要研究成果和创新点如下：
　　 1.在Mizar系统下给出了特殊函数积分公式的表述与论证，其中包括有理数函数，无理数函数，三角函数，反三角函数，指数函数，对数函数，复合函数的Mizar表述与实现；
　　 2.基于Mizar系统定义了以第一类间断点为瑕点的广义积分，并在此基础上给出了积分区间端点同时为瑕点的瑕积分的Mizar定义表述及证明，论证了瑕积分的某些性质；
　　 3.定义了简化剩余系并证明了其部分性质；
　　 4.讨论了指数的某些性质，并结合简化剩余系的定义和性质给出了原根的定义，从而根据两者的关系阐述了简化剩余系的几何级数的表示形式。
　　 以上结果都通过了Mizar系统的验证，其中前一部分被收录于最新的Mizar数学数据库MML中，并发表于2010年的Formalized Mathematics期刊。