基于Mizar的特殊函數(shù)積分及簡化剩余系的研究.pdf

1、Mizar系統(tǒng)起源于數(shù)學(xué)定理的機械化證明，它是用于證明和計算數(shù)學(xué)問題的計算機語言系統(tǒng)，專門用來構(gòu)建Mizar數(shù)學(xué)知識庫的自動推理校驗。Mizar系統(tǒng)擁有世界上最大的數(shù)學(xué)數(shù)據(jù)庫(MML)，其中已經(jīng)收錄1126篇文章，2萬多個數(shù)學(xué)概念，40多萬條數(shù)學(xué)定理，幾乎涵蓋了數(shù)學(xué)科學(xué)的各個分支。當前，Mizar系統(tǒng)已經(jīng)從單一定理證明發(fā)展到多學(xué)科多方面的交叉應(yīng)用，特別是在自動控制、聲音和圖像識別等研究領(lǐng)域有著更為廣泛的應(yīng)用。
　　 本文首先介紹

2、了數(shù)學(xué)機械化證明的歷史及國內(nèi)外研究現(xiàn)狀，其次介紹了Mizar系統(tǒng)的發(fā)展歷程和研究。基于數(shù)學(xué)定理的機器證明和數(shù)學(xué)定理自動推理系統(tǒng)Mizar，對一些特殊函數(shù)類積分問題和數(shù)論中的簡化剩余系問題進行了Mizar表述和推證，且通過了Mizar系統(tǒng)驗證。主要研究成果和創(chuàng)新點如下：
　　 1.在Mizar系統(tǒng)下給出了特殊函數(shù)積分公式的表述與論證，其中包括有理數(shù)函數(shù)，無理數(shù)函數(shù)，三角函數(shù)，反三角函數(shù)，指數(shù)函數(shù)，對數(shù)函數(shù)，復(fù)合函數(shù)的Mizar表述

3、與實現(xiàn)；
　　 2.基于Mizar系統(tǒng)定義了以第一類間斷點為瑕點的廣義積分，并在此基礎(chǔ)上給出了積分區(qū)間端點同時為瑕點的瑕積分的Mizar定義表述及證明，論證了瑕積分的某些性質(zhì)；
　　 3.定義了簡化剩余系并證明了其部分性質(zhì)；
　　 4.討論了指數(shù)的某些性質(zhì)，并結(jié)合簡化剩余系的定義和性質(zhì)給出了原根的定義，從而根據(jù)兩者的關(guān)系闡述了簡化剩余系的幾何級數(shù)的表示形式。
　　 以上結(jié)果都通過了Mizar系統(tǒng)的驗證，其