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

《基于mizar的特殊函数积分及简化剩余系的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于Mjzar的特殊函数积分及简化剩余系的研究．学位论文完成日期：指导教师签字：答辩委员会成员签字：—弋：范}，f，，，¨＼}青岛科技人学研究生学位论文基于Mizar的特殊函数积分及简化剩余系的研究摘要Mizar系统起源于数学定理的机械化证明，它是用于证明和计算数学问题的计算机语言系统，专门用来构建Mizar数学知识库的自动推理校验。Mizar系统拥有世界上最大的数学数据库(删L)，其中已经收录儿26篇文章，2万多个数学概念，40多万条数学定理，几乎涵盖了数学科学的各个分支。当前，Mizar系统已经从单一定理证明发展到多学科多方面的交叉应用，特别是在自动控制、声音和图像识别等研究领域

2、有着更为广泛的应用。本文首先介绍了数学机械化证明的历史及国内外研究现状，其次介绍了Mizar系统的发展历程和研究。基于数学定理的机器证明和数学定理自动推理系统M娩ar，对一些特殊函数类积分问题和数论中的简化剩余系问题进行了Mizar表述和推证，且通过了M娩ar系统验证。主要研究成果和创新点如下：1．在M娩ar系统下给出了特殊函数积分公式的表述与论证，其中包括有理数函数，．无理数函数，三角函数，反三角函数，指数函数，对数函数，复合函数的Mizar表述与实现；2．基于Mizar系统定义了以第一类间断点为瑕点的广义积分，并在此基础上给出了积分区间端点同时为瑕点的瑕积分的M娩ar定义表述及证

3、明，论证了瑕积分的某些性质；3．定义了简化剩余系并证明了其部分性质；+4．讨论了指数的某些性质，并结合简化剩余系的定义和性质给出了原根的定义，从而根据两者的关系阐述了简化剩余系的几何级数的表示形式。以上结果都通过了M娩ar系统的验证，其中前一部分被收录于最新的M沱ar数学数据库MML中，并发表于2010年的凡啪嘲【砌耐朋砌册m巧帮期刊。关键词：算子瑕积分偏函数剩余类基数原根基于Mizar的特殊函数积分及简化剩余系的研究Ⅱ青岛科技大学研究生学位论文INTEGRAnONOFSOMESPECL气LFUNClrIONSANDREDUCEDRESIDUESYSTeMINMIZARABSTRAC

4、T。nleMizarsystemisaComputerlanguagesystemwllichiscreateda11ddevelopdewiththcdevelopment0fforIIlal娩emathematics，usedfofproViI培加dcalculatingmathematicalproblems．MizarisaproofcheckerwhichisusediIlbuildingM娩arMamematiCalUbrary．Mizarw弱createdt0des嘶bemamematicalconceptsandt：heoremsbydhecl【ingmemwimaM

5、娩盯pr00fcheckeronamM—PCforM娩arlibra巧re百stration．M娩arh弱aMizarMath锄aticalUbraryconta岫ing1126artides，morcth觚2millionmathConcepts，锄dmoreth锄40milliontheorem，almostcove血gallbmChesofmatllematiCs．ItisalsoappliediIlm觚y丘eldSsuCh筋autocon们l，Voice，iInageidentificationetC，aIldsetsag)odfoundationt0mathematics加

6、dmerelatedmajoL111isdisscn撕0ndescIibestheIlistory诬dⅡlepresentdomeStic锄d0verseasC0ndidonoffo蛐al咖：mathl浊atiCs锄d血eM泣arsystem．BasedonthereseafChofmamematicmechaIl娩ation锄dtlleM娩arsystem，meautllormakesadisctlssiononsomeproblemswllichhltegrationofsomesped“矗ln以。璐柚dthe川uoedresiduesystcminmenumbertlleory

7、'aIldproVidesmecoⅡespIoIldiIlgpr00f狃dcalcIllanonmethodSiIlMizarsyStem．1．1lemailIcontelltsaresu衄ar娩edasfbUOws：1．IIlte黟ationfo加ulaofsomespecialfuIlctio施isfo咖dl娩edconciselyinMizarsystem，iIlc：IudiIlgrationalfun(：tion，irrationalfIlncti