基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究

基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究

ID:33534926

大?。?.26 MB

頁(yè)數(shù):76頁(yè)

時(shí)間:2019-02-26

基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究_第1頁(yè)
基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究_第2頁(yè)
基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究_第3頁(yè)
基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究_第4頁(yè)
基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究_第5頁(yè)
資源描述:

《基于mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究》由會(huì)員上傳分享,免費(fèi)在線閱讀,更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫(kù)。

1、基于Mjzar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究.學(xué)位論文完成日期:指導(dǎo)教師簽字:答辯委員會(huì)成員簽字:—弋:范},f,,,¨\}青島科技人學(xué)研究生學(xué)位論文基于Mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究摘要Mizar系統(tǒng)起源于數(shù)學(xué)定理的機(jī)械化證明,它是用于證明和計(jì)算數(shù)學(xué)問(wèn)題的計(jì)算機(jī)語(yǔ)言系統(tǒng),專門用來(lái)構(gòu)建Mizar數(shù)學(xué)知識(shí)庫(kù)的自動(dòng)推理校驗(yàn)。Mizar系統(tǒng)擁有世界上最大的數(shù)學(xué)數(shù)據(jù)庫(kù)(刪L),其中已經(jīng)收錄兒26篇文章,2萬(wàn)多個(gè)數(shù)學(xué)概念,40多萬(wàn)條數(shù)學(xué)定理,幾乎涵蓋了數(shù)學(xué)科學(xué)的各個(gè)分支。當(dāng)前,Mizar系統(tǒng)已經(jīng)從單一定理證明發(fā)展到多學(xué)科多方面的交叉應(yīng)用,特別是在自動(dòng)控制、聲音和圖像識(shí)別等研究領(lǐng)域

2、有著更為廣泛的應(yīng)用。本文首先介紹了數(shù)學(xué)機(jī)械化證明的歷史及國(guó)內(nèi)外研究現(xiàn)狀,其次介紹了Mizar系統(tǒng)的發(fā)展歷程和研究?;跀?shù)學(xué)定理的機(jī)器證明和數(shù)學(xué)定理自動(dòng)推理系統(tǒng)M娩ar,對(duì)一些特殊函數(shù)類積分問(wèn)題和數(shù)論中的簡(jiǎn)化剩余系問(wèn)題進(jìn)行了Mizar表述和推證,且通過(guò)了M娩ar系統(tǒng)驗(yàn)證。主要研究成果和創(chuàng)新點(diǎn)如下:1.在M娩ar系統(tǒng)下給出了特殊函數(shù)積分公式的表述與論證,其中包括有理數(shù)函數(shù),.無(wú)理數(shù)函數(shù),三角函數(shù),反三角函數(shù),指數(shù)函數(shù),對(duì)數(shù)函數(shù),復(fù)合函數(shù)的Mizar表述與實(shí)現(xiàn);2.基于Mizar系統(tǒng)定義了以第一類間斷點(diǎn)為瑕點(diǎn)的廣義積分,并在此基礎(chǔ)上給出了積分區(qū)間端點(diǎn)同時(shí)為瑕點(diǎn)的瑕積分的M娩ar定義表述及證

3、明,論證了瑕積分的某些性質(zhì);3.定義了簡(jiǎn)化剩余系并證明了其部分性質(zhì);+4.討論了指數(shù)的某些性質(zhì),并結(jié)合簡(jiǎn)化剩余系的定義和性質(zhì)給出了原根的定義,從而根據(jù)兩者的關(guān)系闡述了簡(jiǎn)化剩余系的幾何級(jí)數(shù)的表示形式。以上結(jié)果都通過(guò)了M娩ar系統(tǒng)的驗(yàn)證,其中前一部分被收錄于最新的M沱ar數(shù)學(xué)數(shù)據(jù)庫(kù)MML中,并發(fā)表于2010年的凡啪嘲【砌耐朋砌冊(cè)m巧幫期刊。關(guān)鍵詞:算子瑕積分偏函數(shù)剩余類基數(shù)原根基于Mizar的特殊函數(shù)積分及簡(jiǎn)化剩余系的研究Ⅱ青島科技大學(xué)研究生學(xué)位論文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

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文

此文檔下載收益歸作者所有

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文
溫馨提示:
1. 部分包含數(shù)學(xué)公式或PPT動(dòng)畫的文件,查看預(yù)覽時(shí)可能會(huì)顯示錯(cuò)亂或異常,文件下載后無(wú)此問(wèn)題,請(qǐng)放心下載。
2. 本文檔由用戶上傳,版權(quán)歸屬用戶,天天文庫(kù)負(fù)責(zé)整理代發(fā)布。如果您對(duì)本文檔版權(quán)有爭(zhēng)議請(qǐng)及時(shí)聯(lián)系客服。
3. 下載前請(qǐng)仔細(xì)閱讀文檔內(nèi)容,確認(rèn)文檔內(nèi)容符合您的需求后進(jìn)行下載,若出現(xiàn)內(nèi)容與標(biāo)題不符可向本站投訴處理。
4. 下載文檔時(shí)可能由于網(wǎng)絡(luò)波動(dòng)等原因無(wú)法下載或下載錯(cuò)誤,付費(fèi)完成后未能成功下載的用戶請(qǐng)聯(lián)系客服處理。