特殊函数差分差商积分与函数正交性和函数范数mizar实现地研究

《特殊函数差分差商积分与函数正交性和函数范数mizar实现地研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、青岛科技大学研究生学位论文特殊函数差分差商积分及函数正交性与函数范数的Mizar实现研究摘要从定理自动证明的发展过程中产生和发展起来的Mizar系统，是用来构建Mizar数学知识库的证明校验系统，也是一个数学定理证明工具。Mizar系统的逻辑框架基于Ja§kowski自然演绎推理的古典逻辑。Mizar如今已经成为集逻辑证明、校验、排版功能于一体的数学知识处理的形式化系统，拥有自己的数据库MML，其中收录了一千多篇数学论文，几乎涵盖了数学科学的各个分支。本文首先介绍了定理机器证明及Mizar系统的历史，其次对如何利用

2、Mizar语言完成数学论文和进行自动推理校验给出了简要的说明。本文主要研究了以Mizar系统为平台，证明特殊函数的差分差商、特殊函数的积分和实现函数正交性与函数范数。本文主要的创新点如下：．1．完成了特殊函数的差分差商在Mizar系统中的实现；2．根据特殊函数的微分公式及可积性，在Mizar中实现多种特殊函数的积分；3．首次在Mizar中定义了函数的正交性与函数范数，并讨论了有关性质，应用Mizar语言完成了相关定理的自动推理证明，并验证其正确性。以上结果均通过Mizar系统的验证，被收录到最新的Mizar数据库(

3、MML)中，并发表于2008年和2009年的FormalizedMathematics。关键词：Mizar定理机器证明差分差商积分函数正交性函数范数特殊函数差分差商积分及函数正交性与函数范数的Mimr实现研究THESPECIALFUNCTIONDIFFERENCE，DIFFERENCEQUOTIENT,INTEGRALANDORTHOGONAL，NORMFUNCTIONINMIZARABSTRACTTheMizarprojectiscreatedanddevelopswiththedevelopmentofauto

4、matedtheoremprovingwhichisabranchofartificialintelligence．MizarisaproofcheckerwhichisusedinbuildingMizarMathematicalLibrary．111eoriginalMizarisdesignedtohelpmathematicianswritemathematicalpapersanditbasesontheJa童kowskis够leofnaturaldeduction．TodayMizarhasbecome

5、aformalizationofmathematicalknowledge，withthefunctionofproving，verifyingandtypesetting．MizarsystemhasalargeMizarMathematicalLibrary,includingmorethanonethousandarticles，almostcoveringallbranchesofmathematics．Tllisdissertationdescribesthehistoryoftheoremautomat

6、icprovingandMizarsystemandhowtowritearticlesinMizarsystem．刀硷mainworkofthepaperissummarizedasfollowing：1．DifferenceanddifferencequotientofsomespecialfunctionsareimplementedinMizarsystem．．2．Basedondifferentialsandintegrabilityofspecialfunctions，severalintegralsa

7、representedandimplementedinMizarsystem．3．Forthefirsttimetheorthogonalityoffunctionsandthenorrlloffunctionsatedefined．Inaddition，thepropertiesofrelatedtheoremsaleverifiedinMizarsystem．Theautomaticreasoningandprovingprocessrelatedtotheaboveaspectshavebeencomplet

8、edandverifiedtobecorrectinMizarsystem．KEYWORDS：quotientintegralMizarautomatedtheoremprovingdifferenceanddifferenceII特殊函数差分差商积分及函数正交性与函数范数的Mizar实现研究声明独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工