（應(yīng)用數(shù)學(xué)專業(yè)論文）特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的mizar實(shí)現(xiàn)研究.pdf

青島科技大學(xué)研究生學(xué)位論文 特殊函數(shù)差分差商積分及函數(shù)正交性與 函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 摘要 從定理自動證明的發(fā)展過程中產(chǎn)生和發(fā)展起來的m i z a r 系統(tǒng)，是用來構(gòu)建 m i z a r 數(shù)學(xué)知識庫的證明校驗(yàn)系統(tǒng)，也是一個數(shù)學(xué)定理證明工具。m i z a r 系統(tǒng)的邏 輯框架基于j a k o w s k i 自然演繹推理的古典邏輯。m i z a r 如今已經(jīng)成為集邏輯證明、 校驗(yàn)、排版功能于一體的數(shù)學(xué)知識處理的形式化系統(tǒng)，擁有自己的數(shù)據(jù)庫m m l ， 其中收錄了一千多篇數(shù)學(xué)論文，幾乎涵蓋了數(shù)學(xué)科學(xué)的各個分支。 本文首先介紹了定理機(jī)器證明及m i z a r 系統(tǒng)的歷史，其次對如何利用m i z a r 語 言完成數(shù)學(xué)論文和進(jìn)行自動推理校驗(yàn)給出了簡要的說明。本文主要研究了以m i z a r 系統(tǒng)為平臺，證明特殊函數(shù)的差分差商、特殊函數(shù)的積分和實(shí)現(xiàn)函數(shù)正交性與函 數(shù)范數(shù)。本文主要的創(chuàng)新點(diǎn)如下： 1 完成了特殊函數(shù)的差分差商在m i z a r 系統(tǒng)中的實(shí)現(xiàn)； 2 根據(jù)特殊函數(shù)的微分公式及可積性，在m i z a r 中實(shí)現(xiàn)多種特殊函數(shù)的積分； 3 首次在m i z a r 中定義了函數(shù)的正交性與函數(shù)范數(shù)，并討論了有關(guān)性質(zhì)，應(yīng) 用m i z a r 語言完成了相關(guān)定理的自動推理證明，并驗(yàn)證其正確性。 以上結(jié)果均通過m i z a r 系統(tǒng)的驗(yàn)證，被收錄到最新的m i z a r 數(shù)據(jù)庫( m m l ) 中， 并發(fā)表于2 0 0 8 年和2 0 0 9 年的f o r m a l i z e dm a t h e m a t i c s 。 關(guān)鍵詞：m i z a r 定理機(jī)器證明差分差商積分函數(shù)正交性函數(shù)范數(shù) 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i m r 實(shí)現(xiàn)研究 t h es p e c i a lf u n c t i o nd i f f e r e n c e ， d i f f e r e n c eq u o t i e n t , i n t e g r a la n d o r t h o g o n a l ，n o r m f u n c t i o ni nm i z a r a bs t r a c t t h em i z a rp r o j e c ti sc r e a t e da n dd e v e l o p sw i t ht h ed e v e l o p m e n to fa u t o m a t e d t h e o r e mp r o v i n gw h i c hi sab r a n c ho fa r t i f i c i a li n t e l l i g e n c e m i z a ri sap r o o fc h e c k e r w h i c hi su s e di nb u i l d i n gm i z a rm a t h e m a t i c a ll i b r a r y 1 1 1 eo r i g i n a lm i z a ri sd e s i g n e d t oh e l pm a t h e m a t i c i a n sw r i t em a t h e m a t i c a lp a p e r sa n di tb a s e so nt h ej a 童k o w s k is 夠l e o fn a t u r a ld e d u c t i o n t o d a ym i z a rh a sb e c o m eaf o r m a l i z a t i o no fm a t h e m a t i c a l k n o w l e d g e ，w i t ht h ef u n c t i o no fp r o v i n g ，v e r i f y i n ga n dt y p e s e t t i n g m i z a rs y s t e m h a sa l a r g em i z a rm a t h e m a t i c a ll i b r a r y , i n c l u d i n gm o r et h a no n et h o u s a n da r t i c l e s ，a l m o s t c o v e r i n ga l lb r a n c h e so fm a t h e m a t i c s t l l i sd i s s e r t a t i o nd e s c r i b e st h eh i s t o r yo ft h e o r e ma u t o m a t i cp r o v i n ga n dm i z a r s y s t e ma n dh o wt ow r i t ea r t i c l e si nm i z a rs y s t e m 刀鹼m a i nw o r ko ft h ep a p e ri s s u m m a r i z e da sf o l l o w i n g ： 1 d i f f e r e n c ea n dd i f f e r e n c eq u o t i e n to fs o m es p e c i a lf u n c t i o n sa r ei m p l e m e n t e d i nm i z a rs y s t e m 2 b a s e do nd i f f e r e n t i a l sa n di n t e g r a b i l i t yo fs p e c i a lf u n c t i o n s ，s e v e r a li n t e g r a l s a r ep r e s e n t e da n d i m p l e m e n t e di nm i z a rs y s t e m 3 f o rt h ef i r s tt i m et h eo r t h o g o n a l i t yo ff u n c t i o n sa n dt h en o r r l lo ff u n c t i o n sa t e d e f i n e d i na d d i t i o n ，t h ep r o p e r t i e so fr e l a t e dt h e o r e m sa l ev e r i f i e di nm i z a rs y s t e m t h ea u t o m a t i cr e a s o n i n ga n dp r o v i n gp r o c e s sr e l a t e dt ot h ea b o v ea s p e c t sh a v e b e e nc o m p l e t e da n dv e r i f i e dt ob ec o r r e c ti nm i z a rs y s t e m k e yw o r d s ： q u o t i e n ti n t e g r a l m i z a ra u t o m a t e dt h e o r e mp r o v i n gd i f f e r e n c ea n dd i f f e r e n c e i i 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 聲明 獨(dú)創(chuàng)性聲明 本人聲明所呈交的論文是我個人在導(dǎo)師指導(dǎo)下進(jìn)行的研究工作及取得的研 究成果。盡我所知，除了文中特別加以標(biāo)注和致謝中所羅列的內(nèi)容以外，論文中 不包含其他人已經(jīng)發(fā)表或撰寫過的研究成果，也不包含本人已用于其他學(xué)位申請 的論文或成果。與我一同工作的同志對本研究所做的任何貢獻(xiàn)均已在論文中做了 明確的說明并表示了謝意。 申請學(xué)位論文與資料若有不實(shí)之處，本人承擔(dān)一切相關(guān)責(zé)任。 本人簽名：日期： 年月日 關(guān)于論文使用授權(quán)的說明 本學(xué)位論文作者完全了解青島科技大學(xué)有關(guān)保留、使用學(xué)位論文的規(guī)定，有 權(quán)保留并向國家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和磁盤，允許論文被查閱和借 閱。本人授權(quán)學(xué)?？梢詫W(xué)位論文的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索， 可以采用影印、縮印或掃描等復(fù)制手段保存、匯編學(xué)位論文。本人離校后發(fā)表或 使用學(xué)位論文或與該論文直接相關(guān)的學(xué)術(shù)論文或成果時，署名單位仍然為青島科 技大學(xué)。( 保密的學(xué)位論文在解密后適用本授權(quán)書) 本學(xué)位論文屬于： 保密口，在 年解密后適用于本聲明。 不保密口。 ( 請?jiān)谝陨戏娇騼?nèi)打“”) 本人簽名： 導(dǎo)師簽名： 麴 日期： 日期： 月日 月，之日 ， 青島科技大學(xué)研究生學(xué)位論文 1 緒論 1 1 定理機(jī)器證i t 乒l ( a u t o m a t e dt h e o r e mp r o v i n g ) 的歷史及研究現(xiàn)狀 數(shù)學(xué)不但是整個人類文化的重要組成部分，而且始終是推進(jìn)人類文明的重要 力量 1 】。數(shù)學(xué)是對現(xiàn)實(shí)世界數(shù)與形的最簡潔有效的描述，也是高新技術(shù)的理論基 礎(chǔ)，是聯(lián)系科學(xué)與技術(shù)的紐帶。數(shù)學(xué)具有表達(dá)精確，論證嚴(yán)謹(jǐn)?shù)奶攸c(diǎn)，其主要形 式是數(shù)值計算和定理證明 2 】。 電子計算機(jī)是人腦的延伸，它的飛速發(fā)展為人類實(shí)現(xiàn)腦力勞動的機(jī)械化創(chuàng)造 了物質(zhì)條件。實(shí)現(xiàn)腦力勞動的機(jī)械化，將使科研工作者擺脫繁重的甚至是人力難 以勝任的工作，為在科學(xué)和高新技術(shù)方面進(jìn)行更高層次的創(chuàng)新性研究提供有力的 工具，進(jìn)而提高我國知識創(chuàng)新的效率。實(shí)現(xiàn)數(shù)學(xué)的機(jī)械化是實(shí)現(xiàn)腦力勞動機(jī)械化 的理論基礎(chǔ)。數(shù)學(xué)機(jī)械化理論和方法的建立，是深層次的知識創(chuàng)新，將極大地推 動相關(guān)學(xué)科的發(fā)展。數(shù)學(xué)機(jī)械化研究，不僅為數(shù)學(xué)的發(fā)展提出了一種戰(zhàn)略構(gòu)想， 也將為我國信息技術(shù)的創(chuàng)新發(fā)揮重要作用。 數(shù)學(xué)機(jī)械化又稱為機(jī)械化方法或機(jī)器證明，就是將數(shù)學(xué)的主要內(nèi)容轉(zhuǎn)換為計 算機(jī)可接受的形式并利用計算機(jī)強(qiáng)大的計算功能解決數(shù)學(xué)與高新技術(shù)中的基礎(chǔ) 理論問題。主要是實(shí)現(xiàn)數(shù)值計算和定理證明的機(jī)械化。目前，定理機(jī)器證明是數(shù) 學(xué)機(jī)械化研究的重點(diǎn)，同時也在人工智能的發(fā)展中有著舉足輕重的影響。定理機(jī) 器證明( a t p ：a u t o m a t e dt h e o r e mp r o v i n g ) 就是把一系列定理( 這一系列定理可能 可數(shù)，也可能不可數(shù)) 當(dāng)作一個整體加以考慮，建立一種統(tǒng)一而且確定的程序， 使得此系列中的每一個定理，只要按照這個程序機(jī)械地、按部就班地一步一步進(jìn) 行下去，經(jīng)過有限步后就可從數(shù)學(xué)命題的假設(shè)推斷出數(shù)學(xué)命題的結(jié)論是否為真。 這種統(tǒng)一的、確定的方法稱為定理證明的機(jī)械化方法 3 】。事實(shí)上，定理機(jī)器證明 的實(shí)質(zhì)就是把具有智能特點(diǎn)的推理演繹過程機(jī)械化。 用機(jī)械方法證明數(shù)學(xué)定理的構(gòu)想是從十七世紀(jì)時期的數(shù)學(xué)家笛卡兒與萊布尼 茨開始的。笛卡兒的解析幾何學(xué)建立了幾何的代數(shù)化，將無章可循的幾何定理的 證明按一定的步驟化為代數(shù)形式進(jìn)行解決，為幾何定理機(jī)器證明提供了簡明的方 法，也為幾何問題的證明方法走上機(jī)械化道路奠定了基礎(chǔ)。德國著名的數(shù)學(xué)家萊 布尼茲通過對邏輯的研究，設(shè)計并制造出能做乘法的計算器，進(jìn)而萌發(fā)了設(shè)計萬 能語言和造一臺能自動檢驗(yàn)數(shù)學(xué)命題正確性的通用機(jī)器_ 推理機(jī)器的構(gòu)想。盡 管他的這一宏偉設(shè)想，由于當(dāng)時條件的限制而未能實(shí)現(xiàn)；但對后來興起的布爾代 數(shù)和數(shù)理邏輯卻起到了促進(jìn)和完善作用，。正是沿著這一方向，通過人們的努力， 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 才形成了定理機(jī)器證明的邏輯方法。十九世紀(jì)末，希爾伯特( h i l b e r t ) 等人創(chuàng)立并發(fā) 展了數(shù)理邏輯，又為機(jī)器證明定理提供了理論和方法。 二十世紀(jì)三十年代，法國數(shù)學(xué)家賀布蘭特( h e r b r a n d ) 從數(shù)理邏輯角度奠定 了機(jī)器證明機(jī)械化的理論基礎(chǔ)，為人工智能的開發(fā)提供了條件。到了四十年代， 電子計算機(jī)的問世為數(shù)學(xué)定理機(jī)器證明提供了設(shè)備條件，機(jī)器證明開始崛起。波 蘭的著名邏輯學(xué)家、數(shù)學(xué)家塔斯基( a t a r s k i ) 在1 9 4 8 年的經(jīng)典著作初等代數(shù) 和幾何的判定法中，證明了計算機(jī)可以判斷所有初等代數(shù)和初等幾何范圍內(nèi)的 定理證明，并且給出了機(jī)器證明的具體方法，這為人類開始機(jī)器證明方面的可行 性研究樹立了信心。五十年代中期，美國開始嘗試?yán)糜嬎銠C(jī)來證明數(shù)學(xué)定理。 1 9 5 6 年可算為人類歷史上計算機(jī)證明以至于人工智能研究的開端，美國卡爾基大 學(xué)蘭德公司協(xié)作組的成員紐厄爾、西蒙和肖烏等人通過研究證明定理的心理 過程，創(chuàng)建了機(jī)器證明的啟發(fā)式搜索法，編制了一個“邏輯理論機(jī)”程序( 簡稱 l t ) ，成功證明了羅素( b a w r u s s e l l ) 和淮特海( a n w h i t e h e a d ) 所著的數(shù) 學(xué)原理第二章5 2 條定理中的3 8 條。這是機(jī)器證明史上第一項(xiàng)奠基性的突破。 五十年代末，美籍華人、美國洛克菲勒大學(xué)的數(shù)理邏輯學(xué)家、著名教授王浩 發(fā)明了王浩算法，使得機(jī)器證明開始規(guī)范化。19 5 9 年，他在i b m 7 0 4 計算機(jī)上僅僅 用了9 分鐘就證明了羅素( b a w r u s s e l l ) 和淮特海( a n w h i t e h e a d ) 所著的數(shù) 學(xué)原理中的三百五十多個命題，并明確地提出了“走向數(shù)學(xué)的機(jī)械化 的口號， 他是數(shù)學(xué)史上的第一人，當(dāng)時就在數(shù)學(xué)與數(shù)理邏輯界引起轟動。1 9 6 5 年，美國數(shù) 學(xué)家魯賓遜( j a r o b i n s o n ) 提出了“歸結(jié)原理 ，這是用邏輯方法證明數(shù)學(xué)定理 的一個重要進(jìn)展 4 】。到七十年代，機(jī)器證明獲得重大的新進(jìn)展。1 9 7 6 年美國伊利 諾斯大學(xué)的哈肯( w h a k e n ) 、科奇( j k 0 e 1 1 ) 和阿佩爾( k a p p e l ) 在三臺高速 計算機(jī)上花了一千二百小時，完成了構(gòu)造可約構(gòu)形的不可避免集的工作，證明了 一百二十四年未能解決的“四色問題 ( 德國數(shù)學(xué)家麥比烏斯于1 8 4 0 年提出了著 名的四色猜想：“如果只用四種顏色能否對球面上或平面上的任何地圖著色?！? 。 這表明利用計算機(jī)把人類思維中的邏輯推理能力推進(jìn)到前所未有的高度的可能 性。 七十年代，我國也參與到數(shù)學(xué)機(jī)械化這個新興領(lǐng)域魄研究中，并作出了巨大 的貢獻(xiàn)。1 9 7 7 年，我國著名數(shù)學(xué)家吳文俊院士在中國科學(xué)上發(fā)表了初等幾 何判定問題與機(jī)械化證明一文，文中提出了幾何定理的機(jī)器證明的新方法，從 而揭開了機(jī)器證明幾何定理的新的一頁。他首次在計算機(jī)上證明了一大批很不簡 單的初等幾何定理，開創(chuàng)了從公理化到機(jī)械化的新路，在國際上被譽(yù)為“吳方法 ， 在吳方法的影響下，美國等十幾個國家的數(shù)學(xué)家、科學(xué)家先后發(fā)表了數(shù)百篇這方 面的論文【5 】。1 9 8 5 年，吳文俊院士的關(guān)于代數(shù)方程組的零點(diǎn)的發(fā)表標(biāo)志著求 2 青島科技大學(xué)研究生學(xué)位論文 解多項(xiàng)式方程組的吳文俊消元法( 或“吳方法) 正式建立。與國際上流行的代數(shù) 理想論不同，吳文俊明確提出了具有中國特色的、以多項(xiàng)式零點(diǎn)集為基本點(diǎn)的學(xué) 術(shù)路線?！皡欠椒ā钡拇_立與廣泛應(yīng)用，復(fù)興了國際數(shù)學(xué)機(jī)械化的研究。 我國許多的數(shù)學(xué)家在吳文俊數(shù)學(xué)機(jī)械化思想方法的啟示下，在數(shù)學(xué)機(jī)械化領(lǐng) 域也作出了很多卓有成效的工作。1 9 9 9 年，我國數(shù)學(xué)家楊路創(chuàng)立了降維算法，并 研發(fā)出實(shí)現(xiàn)這種算法的數(shù)學(xué)軟件。他用這種軟件證明了兩千多個不等式，這是幾 何定理機(jī)械化證明領(lǐng)域的又一重大突破。2 0 0 0 年，張景中院士研制出第三代智能 數(shù)學(xué)平臺軟件，又稱為z + z ”智能教育平臺，開創(chuàng)了世界智能性數(shù)學(xué)教學(xué)軟件的 先河。 如今，隨著數(shù)學(xué)機(jī)械化研究的深入發(fā)展，人們已經(jīng)可以根據(jù)機(jī)械化方法創(chuàng)建 各種機(jī)器語言來編制程序，并能在計算機(jī)上進(jìn)行證明。短短幾十年內(nèi)，這一理論 不僅在不等式的機(jī)器證明、幾何定理的機(jī)器證明、微分幾何、方程組求解、力學(xué)、 理論物理等新領(lǐng)域得到成功的應(yīng)用，而且也為信息處理、曲匝造型、數(shù)控技術(shù)、 機(jī)器人學(xué)、計算機(jī)圖形與視覺等高科技領(lǐng)域提供了有力工具，并取得了一系列優(yōu) 秀成果。近年來上述理論又對三角函數(shù)、雙曲函數(shù)等超越函數(shù)公式實(shí)現(xiàn)了機(jī)械化 的定理證明。同時在集合論、分析拓?fù)鋵W(xué)以及遞歸函數(shù)等方面都使機(jī)器證明獲得 了成功的應(yīng)用。所以，隨著電子計算機(jī)運(yùn)行速度的不斷提高，以及計算機(jī)證明理 論研究的逐步深入，將會開辟機(jī)器證明的新時代。機(jī)器證明實(shí)現(xiàn)了用計算機(jī)來完 成數(shù)學(xué)命題的證明，成為數(shù)學(xué)機(jī)械化研究的一個重要組成部分，是現(xiàn)代人工智能 發(fā)展的一個重要方向。 迄今為止，全世界已有三百多種可以用來進(jìn)行定理機(jī)器證明的語言系統(tǒng) 6 1 ， 其中有十五種數(shù)學(xué)定理證明系統(tǒng)受到大多數(shù)專家及北美數(shù)學(xué)知識管理組織 ( m k m ) 協(xié)會的認(rèn)可，比如a u t o m a t h 系統(tǒng)【7 】、m i z a r 系統(tǒng) 8 ，9 】、n u p r l 系統(tǒng) 1 0 】 和t h e o r e m a 系統(tǒng)【1 1 等。這些語言系統(tǒng)各自的創(chuàng)建初衷不同，卻有著一個共同的 特征，就是人類使用機(jī)器語言來書寫、計算、推理和證明文本性質(zhì)的數(shù)學(xué)問題， 并使用計算機(jī)來驗(yàn)證其正確性。近年來，a c l 2 1 2 和p v s 1 3 】也越來越受人們的 關(guān)注。荷蘭著名的數(shù)學(xué)家f w i e d i j k 在 c o m p a r i n g m a t h e m a t i c a lp r o v e r s ” 1 4 中主 要從它們知識庫的大小、邏輯性表示的強(qiáng)弱和自動智能的水平三個方面比較 m i z a r ，p v s ，a l f a a g d a ，a c l 2 ，h o l ，c o q ，o t t e r i v y ，l e g o ，m e t a r n a t h ，t h e o r e m a ， n u p r l 、i s a b e l l e i s a r 、p h o x 、i m p s 、f 2 m e g a 這十五個數(shù)學(xué)定理機(jī)器證明系統(tǒng)。 此外還比較了十五個證明系統(tǒng)的數(shù)學(xué)化程度和自動化水平。f w i e d i j k 于2 0 0 6 年在 “t h es e v e n t e e np r o v e r so ft h ew o r l d 【1 5 】中又增加了bm e t h o d 系統(tǒng)( 由 d o m i n i q u ec a n s e l l g l j 建) 和m i n l o g 系統(tǒng)( 由h e l m u ts c h w k h t e n b e r g 創(chuàng)建) 這兩個重 要的數(shù)學(xué)定理證明系統(tǒng)。在以上十七個系統(tǒng)中，h o l 、m i z a r 、n u p r l 、bm e t h o d 、 3 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 p v s 、c o q 、i s a b e l l e i s a r 、i m p s 、m i i d o g 這9 個系統(tǒng)均需要龐大的數(shù)學(xué)領(lǐng)域知識庫 的支持。由此可以看出，數(shù)學(xué)定理的機(jī)器證明需要有龐大的數(shù)學(xué)知識庫來支持。 其中，m i z a r 具有龐大的數(shù)學(xué)領(lǐng)域知識庫m i z a rm a t h e m a t i c a ll i b r a r y ( 簡稱m m l ) 。 1 2m i z a r 系統(tǒng)的歷史和發(fā)展現(xiàn)狀 m i z a r 系統(tǒng)是一個利用計算機(jī)把所要處理的項(xiàng)目進(jìn)行形式化的系統(tǒng)。它是由 波蘭華沙大學(xué)的教授a n d r z e jt r y b u l e c 組織的m i z a r 協(xié)會領(lǐng)導(dǎo) 1 - 6 】的，到目前為止 已經(jīng)有三十多年的發(fā)展歷史。最初的m i z a r 系統(tǒng)并不是用來書寫和推證數(shù)學(xué)定理 證明，而是為了利用創(chuàng)建的一個軟件環(huán)境來幫助數(shù)學(xué)家們撰寫和驗(yàn)證數(shù)學(xué)論文， 因此發(fā)展的軟件環(huán)境一般是用來書寫傳統(tǒng)的數(shù)學(xué)論文的，古典數(shù)學(xué)與集合理論也 就相應(yīng)的成為軟件環(huán)境發(fā)展的基礎(chǔ)【1 7 】。 如今的m i z a r 系統(tǒng)是一個用來構(gòu)建m i z a r 數(shù)學(xué)知識庫的自動推理校驗(yàn)系統(tǒng)，擁 有龐大的數(shù)學(xué)數(shù)據(jù)庫( m i z a rm a t h e m a t i c a ll i b r a r y ，簡稱m m l ) ，同時此數(shù)學(xué)數(shù)據(jù)庫 也是期刊f o r m a l i z e dm a t h e m a t i c s 的o n 1 i n e 版本，在互聯(lián)網(wǎng)上即可隨時查閱。 1 9 7 3 年1 1 月1 4 日在波蘭華沙大學(xué)圖書館學(xué)和科學(xué)信息學(xué)院的一次研討會 上，m i z a r 系統(tǒng)第一次由a n d = e jt r y b u l e c 教授完整地提出來。他提出了設(shè)計建立 一種可以用來撰寫數(shù)學(xué)論文的計算機(jī)語言與它的可實(shí)現(xiàn)性，并提出此語言在功能 上的特點(diǎn)【1 8 】： = 1 能夠進(jìn)行存儲和編譯，即所寫文章可以存儲于計算機(jī)中，并可將其翻譯 成數(shù)學(xué)語言。 2 語言簡潔易懂，格式勻稱整齊。 3 具備支撐整個數(shù)學(xué)領(lǐng)域自動化信息系統(tǒng)的基本要素。 4 可檢測錯誤、查證參考文獻(xiàn)、刪除多余重復(fù)定理。 5 可根據(jù)有關(guān)定理的證明進(jìn)行一般的教學(xué)活動。 6 自動排版的實(shí)現(xiàn)。 在m i z a r 系統(tǒng)發(fā)展的初期，專家們更注重系統(tǒng)語言的編輯功能，而并非系統(tǒng) 的證明校驗(yàn)功能。1 9 7 4 年秋天。由a n d r z e jt r y b u l e c 、k r z y s z t o f l e b k o w s k i 和r o m a n m a t u s z e w s k i 設(shè)計的用于謂詞演算驗(yàn)證的o d r a 1 2 0 4 系統(tǒng)是第一個可以運(yùn)行的 m i z a r 系統(tǒng)。盡管當(dāng)時的系統(tǒng)十分脆弱，而且運(yùn)行時間較長，但最終還是實(shí)現(xiàn)了 完全正確的語義結(jié)構(gòu)和語法分析。 1 9 7 5 年6 月，a n d r z e jt r y b u l e c 教授第一次以文字的形式展示了他所創(chuàng)建的機(jī) 器證明語言- m i z a r 語言，并于同年1 1 月發(fā)表了一篇關(guān)于m i z a r - p c 的文章。文中 介紹了可以用j 矧( o w s k i 自然演繹推理方法撰寫，用邏輯謂詞驗(yàn)算的m i z a r 語言的 證明過程。那時的m i z a r 系統(tǒng)已經(jīng)可以用( 蛐魚世) 、( p r o o f e n d ) 、( 虹) 、 4 青島科技大學(xué)研究生學(xué)位論文 ( 叢) 、蝕擎o r h e n c e ) 這樣的語義詞來編寫下面這樣的證明過程了。 墊里! 墨 l p3 乓a q ) q ，3 p3r p r o o f 一 坐 a ：i p ) 哪at 鷹3 譬； t h e n - ：p q ； c ：q ) z 絲a ； 絲 p ； 塑q 墮b ； 塾竺登! 竺 r 壘呈c 1 1 匹 一 e n d 一 之后，在華沙大學(xué)的兩個學(xué)院，m i z a r - p c 被應(yīng)用于命題邏輯課程的教學(xué)中。 1 9 7 7 年，m i z a r 系統(tǒng)的發(fā)展進(jìn)程雖然艱難，但仍然完成了由m i z a r - p c 到 m i z a r - q c 1 2 0 4 ( q c o p q u a n t i f i e rc a l c u l u s 的縮寫) 的進(jìn)化，并實(shí)現(xiàn)了系統(tǒng)發(fā)展成 為m i z a r - q c 6 0 0 0 的目標(biāo)。m i z a r 系統(tǒng)已經(jīng)可以完成部分簡單定理的證明，如關(guān)于 集合的交、并、補(bǔ)和格論中的偏序集的定理等，并開始研究幾何學(xué)定理的證明。 1 9 7 8 年，m i z a r 系統(tǒng)在語義與語法上做了大量地充實(shí)、改進(jìn)。在語義方面定義 了謂詞、結(jié)構(gòu)、預(yù)聲明、絕對相等的概念，系統(tǒng)升級為m i z a r - m s ( 即m u l t is o r t e d 的縮寫) ，很多命題已不再需要討論就能完成系統(tǒng)的自行驗(yàn)證了 1 9 7 8 1 9 7 9 年，在s t a n i s t a w 穸u k o w s k i ，c z e s l a wb y l i f i s k i ，a n d r z c jt r y b u l e c ， r o m a nm a m s z e w s k i ，p i o t rr u d n i c k i ，e l 之b i e t ar a m m ，e d m u n dw o r o n o w i c z 七位 教授的努力下，m i z a r 系統(tǒng)實(shí)現(xiàn)了m i z a r - f c 的升級。 1 9 8 1 年，m i z a r 系統(tǒng)升級為m i z a r - 2 階段。為了使文章的內(nèi)容更加規(guī)范、清晰， m i z a r 文章中出現(xiàn)了環(huán)境部部分。m i z a r 系統(tǒng)在i b m 、和u n i x 和o d r a 1 3 0 5 ( i c l 1 9 0 0 ) 等多種不同的機(jī)器上試驗(yàn)運(yùn)行，充分驗(yàn)證了m i z a r 語法的正確性及邏輯的合 理性。 19 8 2 年，m i z a r - m s e ( m u l t i s o r t e dp r e d i c a t ec a l c u l u sw i t he q u a l i t y 的縮寫) 階 段的m i z a r 系統(tǒng)升級成功，此系統(tǒng)次年8 月的華沙國際數(shù)學(xué)家會議上深受矚目。同 年，系統(tǒng)接著完成了至u m i z a r - 3 ( m i z a r - 2 的擴(kuò)充版本) 的進(jìn)_ 步完善。m i z a r 系統(tǒng) 在1 9 8 3 1 9 8 4 年和1 9 8 6 1 9 8 8 年分別實(shí)現(xiàn)了m i z a r - h p f 和m i z a r - 4 兩次重大的突破。 現(xiàn)今所用版本就是由m i z a r - 4 ( m i z a r - 3 的再次升級) 演化而來的 1 9 】。 1 9 8 8 1 9 8 9 年是m i z a r 系統(tǒng)蛻變的重要時期。1 9 8 8 年，m i z a r - 4 被稱之為 p c m i z a r ，并在p c 機(jī)上成功運(yùn)行。19 8 9 年初，m i z a r 數(shù)學(xué)數(shù)據(jù)庫m i z a rm a t h e m a t i c a l l i b r a r y ( m m l ) 開始正式使用。其中，第一篇標(biāo)準(zhǔn)的m i z a r 文章于1 月6 日被收錄 于m m l 中。同年4 5 月，t r y b u l e c 教授在加拿大的艾特蒙頓開始了新一篇m i z a r 文 章的撰寫，并著手將m i z a r 系統(tǒng)中加入跫撂，$ 1 1 強(qiáng)y m i z a r 文章的可讀性。隨著m i z a r 數(shù)據(jù)庫的不斷擴(kuò)大，m i z a r 系統(tǒng)也在進(jìn)行更新升級。1 9 9 0 年，m i z a r 系統(tǒng)的文本期 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 刊( ( f o r m a l i z e dm a t h e m a t i c s ) ) 開始正式出版發(fā)行。1 9 9 5 1 9 9 7 年， f o r m a l i z e d m a t h e m a t i c s ) ) 得到美國o f f i c eo f n a v a lr e s e a r c h 的資金支持 1 9 】。到2 0 0 0 年，m i z a r 數(shù)學(xué)百科全書問世。第二年，m i z a r 協(xié)會的教授g r z e g o r zb a n c e r e k 將m m lq u e r y 增加到m i z a r 系統(tǒng)中，作為在語義方面進(jìn)行問題查詢的瀏覽工具。2 0 0 2 年，m i z a r 數(shù)學(xué)百科全書e m m ( e n c y c l o p e d i ao f m a t h e m a t i c si nm i z a r ) 完成【1 9 】。如今，m i z a r 系統(tǒng)已經(jīng)升級為7 1 1 0 l 版本，m m l 中也已收錄了一千余篇文章，二萬多個數(shù)學(xué)定 義，四十多萬條數(shù)學(xué)定理 2 0 】。 1 3 課題研究的目的和意義 本課題的研究是建立在對數(shù)學(xué)定理的機(jī)器證明和數(shù)學(xué)定理自動推理系統(tǒng) m i z a r 及其語義、語法的深刻理解之上的，在m i z a r 系統(tǒng)中利用其語言及龐大的數(shù) 學(xué)數(shù)據(jù)庫( m m l ) ，對特殊函數(shù)差分差商、特殊函數(shù)積分、函數(shù)正交性與函數(shù)范 數(shù)做進(jìn)一步研究和應(yīng)用。通過對數(shù)學(xué)機(jī)械化與m i z a r 系統(tǒng)的探索研究，為分析學(xué)、 規(guī)劃論、數(shù)值逼近等方面問題在m i z a r 系統(tǒng)中的解決實(shí)現(xiàn)奠定理論與實(shí)踐基礎(chǔ)。 從定理自動證明的發(fā)展過程中產(chǎn)生和發(fā)展起來的m i z a r 系統(tǒng)，是一個既可撰寫 數(shù)學(xué)文章又可對其進(jìn)行檢驗(yàn)的軟件，絕大多數(shù)數(shù)學(xué)學(xué)科中的問題都能用m i z a r 語言 來證明。除了本身重要之外，m i z a r 系統(tǒng)還為研究廣泛領(lǐng)域的機(jī)械化數(shù)學(xué)和數(shù)學(xué)機(jī) 械化研究提供了新方法、新工具、新思路。日本數(shù)學(xué)家和計算機(jī)科學(xué)專家y a ：t s u k a n a k a m u r a 教授利用m i z a r 系統(tǒng)的自動推理完成了j o r d a n 曲線定理的證明，并應(yīng)用在 人工智能方面，使得m i z a r 參與實(shí)現(xiàn)了微型機(jī)器人、音像識別系統(tǒng)、自動化控制、 數(shù)字信號傳輸?shù)榷喾矫娴某晒芯俊?現(xiàn)在的m i z a r 系統(tǒng)已經(jīng)從單獨(dú)定理證明發(fā)展到多學(xué)科多方面的交叉應(yīng)用，其發(fā) 展主要包括以下內(nèi)容： 1 m i z a r 語言的開發(fā)； 2 m i z a r 數(shù)據(jù)庫的擴(kuò)充； 3 m i z a r 自動推理能力的提高； 4 m i z a r 翻譯形式的多樣化處理。 通過對這些方面的研究與完善，m i z a r 語言的理解能力逐步提升，m m l 的知 識儲備得到擴(kuò)充，m i z a r 系統(tǒng)的邏輯推理和校驗(yàn)糾錯的能力得到增強(qiáng)，翻譯機(jī)制更 加完善，與其他機(jī)器證明工具的交叉研究和相互轉(zhuǎn)化不斷加強(qiáng)。m i z a r 的發(fā)展需要 龐大的數(shù)學(xué)領(lǐng)域知識庫( m m l ) 支持，數(shù)學(xué)學(xué)科的發(fā)展也將推動數(shù)學(xué)定理機(jī)器證 明系統(tǒng)m i z a r 的發(fā)展。隨著社會進(jìn)步與計算機(jī)信息產(chǎn)業(yè)的發(fā)展，m i z a r 系統(tǒng)將 會在更多領(lǐng)域得到應(yīng)用。 6 青島科技大學(xué)研究生學(xué)位論文 1 4 課題研究的主要內(nèi)容 m i z a r 系統(tǒng)從1 9 8 9 年建立以來，成功的完成了多次升級，同時數(shù)據(jù)庫m i z a r m a t h e m a t i c a ll i b r a r y ( m m l ) 也不斷進(jìn)行著充實(shí)和改進(jìn)。m i z a r 數(shù)據(jù)庫m m 膨及 到數(shù)學(xué)領(lǐng)域中的多個學(xué)科，如數(shù)學(xué)分析、代數(shù)學(xué)、幾何學(xué)、拓?fù)鋵W(xué)、數(shù)論、圖論、 集合論等。但關(guān)于特殊函數(shù)差分差商、特殊函數(shù)積分及函數(shù)正交性與函數(shù)范數(shù)方 面的定理鮮有涉及。 本文的主要內(nèi)容如下： 1 基于m i z a r 中差分差商的定義與性質(zhì)，完成一次函數(shù)、二次函數(shù)j 反比例 函數(shù)、三角函數(shù)等特殊函數(shù)的差分差商在m i z a r 系統(tǒng)中的實(shí)現(xiàn)。 l 2 根據(jù)指數(shù)函數(shù)、三角函數(shù)、冪函數(shù)、雙曲函數(shù)、無理函數(shù)、反三角函數(shù) 等特殊函數(shù)的微分公式及可積性，運(yùn)用牛頓萊布尼茨公式，在m i z a r 系統(tǒng)中實(shí)現(xiàn)多 種特殊函數(shù)的積分。 3 為了實(shí)現(xiàn)以p ( x ) = 1 為權(quán)函數(shù)時函數(shù)正交性的m i z a r 推理，首先在m i z a r 系 統(tǒng)中定義了內(nèi)積，并論證了其性質(zhì)。再使用m i z a r 語言給出函數(shù)正交性與函數(shù)范數(shù) 的定義，并描述了其性質(zhì)，同時完成以上內(nèi)容的m i z a r 系統(tǒng)證明。 本文主要通過研究特殊函數(shù)差分差商、特殊函數(shù)積分及函數(shù)正交性與函數(shù)范 數(shù)，完成相關(guān)定理的m i z a r 論證，并實(shí)現(xiàn)有關(guān)數(shù)學(xué)理論的m i z a r 轉(zhuǎn)化。 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i m r 實(shí)現(xiàn)研究 2m i z a r 語言 2 1m i z a r 語言 m i z a r 語言是一種數(shù)學(xué)邏輯推理演繹的計算機(jī)語言，它包括英文字母、數(shù)字和 各類標(biāo)號在內(nèi)的a s c i i 碼，這些基本符號是依據(jù)常用的數(shù)學(xué)符號與一般的a s c i i 碼相結(jié)合的原則來定義的。m i z a r 語言是計算機(jī)可編譯、人類可識別的一種程序化 語言。其主要按如下學(xué)科分類 2 l 】：數(shù)的集合、集合論、一般函數(shù)( 或關(guān)系) 、算術(shù) 運(yùn)算、特殊常量、復(fù)數(shù)及基本函數(shù)、極限和序y u ( 級數(shù)) 、邏輯、微積分、幾何學(xué)、 概率、向量和矩陣。 常用的m i z a r 語言詞匯和基本的語法句型主要有：r e s e r v e ( 數(shù)據(jù)屬性預(yù)聲明) 、 l e t ( “任意取定 詞) 、c o n s i d e r ( “存在取定 詞) 、r e c o n s i d e r a s ( 數(shù)據(jù)屬性轉(zhuǎn) 換詞) 、f o r h o l d s ( 全稱命題) 、i m p l i e s ( 直接推導(dǎo)詞) 、s u p p o s e ( 分類討論引 導(dǎo)詞) 、a s s u m e ( 假設(shè)詞) 、g i v e n ( 存在條件引導(dǎo)詞) 、n o w t h u s ( 擴(kuò)散陳述 命題) 、s u c ht h a t 與s t ( 條件引導(dǎo)詞) 、t h e n ( 因果連接詞) 、b y ( 簡單依據(jù)引導(dǎo)詞) 、 f r o m ( 結(jié)構(gòu)依據(jù)引導(dǎo)詞) 、t h u s 與h e n c e ( 結(jié)論引導(dǎo)詞) 等等。 任何一個命題大多是由這些詞語連接命題的表述和證明的。語法詞匯也基本 蘊(yùn)含在各個具體的證明方法中，如分類討論法、數(shù)學(xué)歸納法、反證法、同一性證 明法等等。 2 2m i z a r 文章結(jié)構(gòu) m i z a r 3 之章是使用m i z a r i 吾言進(jìn)行定義、計算、推理演繹以及數(shù)學(xué)定理證明而 形成的文章，利用m i z a r 系統(tǒng)提供的軟件可以在計算機(jī)上對其進(jìn)行檢驗(yàn)和優(yōu)化。通 過系統(tǒng)驗(yàn)證準(zhǔn)確無誤的m i z a r 論文將被發(fā)表在期刊雜志 f o r m a l i z e d m a t h e m a t i c s 上，并收錄至l j m i z a r 數(shù)學(xué)數(shù)據(jù)庫( m m l ) 中。每一篇m i z a r 文章都是文本文件，可以 在任何一個文本編輯軟件中進(jìn)行編寫編輯。m i z a r 文章包括兩部分環(huán)境部( t h e e n v i r o n m e n t ) 與正文部分( m a i ns e c t i o n ) 。環(huán)境部以“e n v i r o n ”開始，以分號結(jié)束。 正文部分以“b e g i n 開始，以分號結(jié)束。若正文部分的內(nèi)容較多，還可根據(jù)需要 用“b e g i n ”將正文部分分成幾個小專題，每一個小專題都同樣以b e g i n 開始，以分 號結(jié)束( 如圖2 1 所示) 。 青島科技大學(xué)研究生學(xué)位論文 ： e n v i r o n ： the e n v i r o ns e c t i o n ； ； ； b e g i n !the m a i ns e c t i o nl ； ； b e g i ni ；t h e m a i n s e c t i o n 2 ； i ： ： ii b 啦 i themains e c t i o n n ：i 圖2 1m i z a r 文章的一般結(jié)構(gòu) f i g 2 - 1t h ef l a m eo f m i z a r a r t i c l e s 環(huán)境部( “e n v i r o n 部分) 主要對論文中所引用的詞匯、符號、定理、初定 義及結(jié)構(gòu)的出處進(jìn)行聲明( 如圖2 - 2 所示) ?！皏 o c a b u l a r i e s 部分是文章引用的詞 匯列表，同時也表明了算符詞匯的運(yùn)算優(yōu)先級，如數(shù)學(xué)運(yùn)算符的優(yōu)先級就是通過 文章名排列的先后順序體現(xiàn)出來的。這就意味著作者可以使用數(shù)據(jù)庫里已定義好 的數(shù)百個詞匯，也可以根據(jù)需要自己定義新的詞匯?！皊 i g n a t u r e ”部分( 包括 n o t a t i o n s ，c o n s t r u c t o r s ，r e g i s t r a t i o n s ，r e q u i r e m e n t s 四部分) 通知m i z a r 處理器這篇 文章可以使用此處列出的文章里的符號。任一篇文章都可以根據(jù)需要，使用詞匯 列表中的詞匯來生成各種形式的新的m i z a r 表達(dá)式?！癲 e f i n i t i o n s 、“t h e o r e m s 和 “s c h e m e s 就是告訴m i z a r 處理器可以使用這些列表文章中的定義、定理和模式 世 霄0 在m i z a r 文章中若要使用系統(tǒng)中已存在的定義或定理，必須將定義或定理的出 處分別添加到環(huán)境部的相應(yīng)分類中。如果在文章中定義了新概念、新符號或新結(jié) 構(gòu)等，同樣需要將本篇文章的縮寫名寫入環(huán)境部中相應(yīng)的位置?？s寫名可由自己 命名，便于在m i z a r 系統(tǒng)中的調(diào)用與檢驗(yàn)。 9 特殊函數(shù)差分差商積分及函數(shù)正交性與函數(shù)范數(shù)的m i z a r 實(shí)現(xiàn)研究 詞匯 v o c a ：b u l 撕c s q ，a 2 ，； ； 輒二 n o t a t i o n s ：c 0 n s t r u c t o r s ! r e g i s t r a t i o n s r e q u i r e m e n t s d e f i n i t i o l l s t h e o r e m s ；s c h e m e s 6 l ，b e ，； c l ，c 2 ，吒； 4 ，吃，d b ； e t ，e 2 ， 氣； z ，以，丘； ，9 2 ，g n 7 ； 啊，吃，k ； 圖2 - 2 環(huán)境部引用分類詞匯 f i g 2 - 2t h ev o c a b u l a r yo fe n v i r o n m e n t 其中a i ，嚷，噍，吃，吃。，表示被引用的m i z a r 文章名。 m i z a r 文章的正文部分一般包含以下幾個模塊： 1 預(yù)聲明模塊。用來聲明變量( 標(biāo)識符) 的類型。 2 定義模塊。用來定義或者重新定義m i z a r 的語法構(gòu)造，包括f u n c t i o n s ( 數(shù) 學(xué)算子的構(gòu)造) 、p r e d i c a t e s ( 公式構(gòu)造) 和m o d e s ( 類型構(gòu)造) 等。 3 結(jié)構(gòu)定義模塊。用來定義新結(jié)構(gòu)。一個由各種域構(gòu)成的實(shí)體就是一個結(jié) 構(gòu)。 4 定理的證明。用來對數(shù)學(xué)命題進(jìn)行證明。借助m i z a r 語言編寫的數(shù)學(xué)命題 通過驗(yàn)證無誤后即可被其它定理或文章引用。 5 輔助信息。包含了一些本篇文章可以使用的引論或引理，但這些內(nèi)容不 會被收錄到數(shù)據(jù)庫中，其它文章也不能引用。 m i z a r 文章的正文部分主要由定義d e f i n i t i o n s $ l 】定理t h e o r e m s 構(gòu)成。定理的證明 以“p r o o f 開頭，以“e n d ；”結(jié)束，二者成對出現(xiàn)。如果證明過程中需要證明一 些小命題，那么這些小命題的證明也采取同樣的格式，如圖2 3 ： l o 青島科技大學(xué)研究生學(xué)位論文 圖2 3 定理證明的一般結(jié)構(gòu) f i g 2 - 3t h ef r a m eo f t h ed e m o n s t r a t i o n 特別說明：m i z a r 文章中，“：( 雙冒號) 表示對問題的評論，檢驗(yàn)系統(tǒng)不對 其后內(nèi)容的正確性與合理性進(jìn)行驗(yàn)證?！?”是免檢符號，放在“p r o o f 前，表 示校驗(yàn)系統(tǒng)對該“p r o o f 和與它成對出現(xiàn)的“e n d ”之間的證明過程不予檢驗(yàn)， 默認(rèn)是正確的。 二 2 3m i z a r 語言的基本表達(dá)符號與基本語法詞匯 2 3 1m i z a r 語言的基本表達(dá)符號 m i z a r 語言中的符號基于純粹的數(shù)學(xué)符號，這些符號的英文表述和一般的 a s c i i 字符相結(jié)合來進(jìn)行定義與編寫。舉例如下表： 普通數(shù)學(xué)命題中v 3 - - nb yx r e a l1 ：3 ； 因?yàn)閙 沒有在r e s e r v e 中預(yù)先聲明數(shù)據(jù)類型，所以每次提及時需要說明b e i n g e l e m e n to f n a t ( 自然數(shù)集的元素) 。 2 、推導(dǎo)詞i m p l i e s i m p l i e s 用于定理的表述，是條件與結(jié)論之間的連接詞。如：a j b 可表示為 a i m p l i e sb 這里不要求a 、b 間有直接的因果關(guān)系。 3 、全稱命題f o r h o l d s ( 1 ) 一般的定理表述 f o rx b e i n gs e th o l d sa ( x ) ( 任給x ，能推出a ( x ) )