中圖網(wǎng)小程序
一鍵登錄
更方便
本類五星書更多>
-
>
宇宙、量子和人類心靈
-
>
氣候文明史
-
>
南極100天
-
>
考研數(shù)學專題練1200題
-
>
希格斯:“上帝粒子”的發(fā)明與發(fā)現(xiàn)
-
>
神農(nóng)架疊層石:10多億年前遠古海洋微生物建造的大堡礁
-
>
聲音簡史
分析基礎(chǔ)機器證明系統(tǒng) 版權(quán)信息
- ISBN：9787030706713
- 條形碼：9787030706713 ; 978-7-03-070671-3
- 裝幀：一般膠版紙
- 冊數(shù)：暫無
- 重量：暫無
- 所屬分類：>>
分析基礎(chǔ)機器證明系統(tǒng) 內(nèi)容簡介
本書利用交互式定理證明工具Coq，在樸素集合論的基礎(chǔ)上，從Peano五條公設(shè)出發(fā)，完整實現(xiàn)Landau有名的《分析基礎(chǔ)》中實數(shù)理論的形式化系統(tǒng)，包括對該專著中全部5個公設(shè)、73條定義和301個定理的Coq描述，其中依次構(gòu)造了自然數(shù)、分數(shù)、分割、實數(shù)和復數(shù)，并建立了Dedekind實數(shù)完備性定理，從而迅速且自然地給出數(shù)學分析的堅實基礎(chǔ)。在分析基礎(chǔ)形式化系統(tǒng)下，給出Dedekind實數(shù)完備性定理與它的幾個有名等價命題間等價性的機器證明，這些命題包括確界存在定理、單調(diào)有界定理、Cauchy-Cantor閉區(qū)間套定理、Heine-Borel-Lebesgue有限覆蓋定理、Bolzano-Weierstrass聚點原理、Bolzano-Weierstrass列緊性定理及Bolzano-Cauchy收斂準則等，基于實數(shù)的完備性定理，作為應(yīng)用，進一步給出閉區(qū)間上連續(xù)函數(shù)的重要性質(zhì)——有界性定理、很值定理、介值定理、一致連續(xù)性定理——的機器證明。另外，還給出張景中院士提出的第三代微積分——不用極限的微積分——的形式化系統(tǒng)實現(xiàn)。在我們開發(fā)的系統(tǒng)中，全部定理無例外地給出Coq的機器證明代碼，所有形式化過程已被Coq驗證，并在計算機上運行通過，體現(xiàn)了基于Coq的數(shù)學定理機器證明具有可讀性和交互性的特點，其證明過程規(guī)范、嚴謹、可靠。該系統(tǒng)可方便地應(yīng)用于數(shù)學分析相關(guān)理論的形式化構(gòu)建。 本書可作為數(shù)學與計算機科學、信息科學相關(guān)專業(yè)的高年級本科生或研究生教材，也可供從事人工智能相關(guān)科研工作者參考。
分析基礎(chǔ)機器證明系統(tǒng) 目錄
目錄
前言
致謝
符號匯集
第1章引言1
1.1概述1
1.1.1證明輔助工具Coq1
1.1.2形式化數(shù)學2
1.1.3分析基礎(chǔ)3
1.1.4第三代微積分5
1.1.5本書結(jié)構(gòu)安排7
1.2基本Coq指令清單及邏輯預備知識7
1.3集合與映射的一些基本概念13
第2章分析基礎(chǔ)的形式化系統(tǒng)實現(xiàn)19
2.1自然數(shù)19
2.1.1公理19
2.1.2加法22
2.1.3序26
2.1.4乘法36
2.1.5補充材料:有限數(shù)的定義及性質(zhì)40
2.2分數(shù)44
2.2.1定義和等價44
2.2.2序46
2.2.3加法51
2.2.4乘法56
2.2.5有理數(shù)和整數(shù)61
2.3分割83
2.3.1定義83
2.3.2序86
2.3.3加法89
2.3.4乘法97
2.3.5有理分割和整分割106
2.4實數(shù)118
2.4.1定義118
2.4.2序.119
2.4.3加法125
2.4.4乘法139
2.4.5Dedekind基本定理146
2.4.6補充材料:實數(shù)運算的一些性質(zhì)151
2.4.7補充材料:實數(shù)序列的一些性質(zhì)166
2.5復數(shù)175
2.5.1定義175
2.5.2加法177
2.5.3乘法181
2.5.4減法186
2.5.5除法188
2.5.6共軛復數(shù)193
2.5.7絕對值195
2.5.8和與積200
2.5.9冪237
2.5.10將實數(shù)編排在復數(shù)系統(tǒng)中245
第3章實數(shù)完備性等價命題的機器證明251
3.1確界存在定理251
3.1.1用Dedekind基本定理證明確界存在定理251
3.1.2用確界存在定理證明Dedekind基本定理254
3.2單調(diào)有界定理255
3.3閉區(qū)間套定理256
3.4有限覆蓋定理258
3.5聚點原理264
3.6列緊性定理268
3.7Cauchy收斂準則272
3.8用Cauchy收斂準則證明Dedekind基本定理275
第4章閉區(qū)間上連續(xù)函數(shù)性質(zhì)的機器證明283
4.1基本定義283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致連續(xù)性定理300
第5章第三代微積分的形式化實現(xiàn)306
5.1預備知識307
5.1.1基本定義307
5.1.2一些引理308
5.2導數(shù)和定積分的初等定義315
5.3積分與微分的新視角324
5.4微積分系統(tǒng)的基本定理346
第6章總結(jié)與注記370
參考文獻375
附錄Coq指令說明386
A.1Coq專用術(shù)語386
A.2Coq證明指令387
A.3集成策略390
索引393
表索引
表1.1書中涉及常用Coq指令簡表8
表1.2書中涉及常用Coq術(shù)語的基本含義13
表6.1分析基礎(chǔ)形式化系統(tǒng)代碼量統(tǒng)計370
表6.2實數(shù)完備性及其等價命題形式系統(tǒng)化代碼量統(tǒng)計371
表6.3閉區(qū)間上連續(xù)函數(shù)性質(zhì)形式化系統(tǒng)代碼量統(tǒng)計371
表6.4第三代微積分形式化系統(tǒng)代碼量統(tǒng)計371
圖索引
圖1.1Landau《分析基礎(chǔ)》的德文-英文版和中文版封面4
圖3.1實數(shù)完備性定理的等價性251
圖3.2實數(shù)的定義與完備性總覽圖282
圖6.1Dedekind基本定理的證明截圖372
圖6.2計算機軟件著作權(quán)登記證書373
前言
致謝
符號匯集
第1章引言1
1.1概述1
1.1.1證明輔助工具Coq1
1.1.2形式化數(shù)學2
1.1.3分析基礎(chǔ)3
1.1.4第三代微積分5
1.1.5本書結(jié)構(gòu)安排7
1.2基本Coq指令清單及邏輯預備知識7
1.3集合與映射的一些基本概念13
第2章分析基礎(chǔ)的形式化系統(tǒng)實現(xiàn)19
2.1自然數(shù)19
2.1.1公理19
2.1.2加法22
2.1.3序26
2.1.4乘法36
2.1.5補充材料:有限數(shù)的定義及性質(zhì)40
2.2分數(shù)44
2.2.1定義和等價44
2.2.2序46
2.2.3加法51
2.2.4乘法56
2.2.5有理數(shù)和整數(shù)61
2.3分割83
2.3.1定義83
2.3.2序86
2.3.3加法89
2.3.4乘法97
2.3.5有理分割和整分割106
2.4實數(shù)118
2.4.1定義118
2.4.2序.119
2.4.3加法125
2.4.4乘法139
2.4.5Dedekind基本定理146
2.4.6補充材料:實數(shù)運算的一些性質(zhì)151
2.4.7補充材料:實數(shù)序列的一些性質(zhì)166
2.5復數(shù)175
2.5.1定義175
2.5.2加法177
2.5.3乘法181
2.5.4減法186
2.5.5除法188
2.5.6共軛復數(shù)193
2.5.7絕對值195
2.5.8和與積200
2.5.9冪237
2.5.10將實數(shù)編排在復數(shù)系統(tǒng)中245
第3章實數(shù)完備性等價命題的機器證明251
3.1確界存在定理251
3.1.1用Dedekind基本定理證明確界存在定理251
3.1.2用確界存在定理證明Dedekind基本定理254
3.2單調(diào)有界定理255
3.3閉區(qū)間套定理256
3.4有限覆蓋定理258
3.5聚點原理264
3.6列緊性定理268
3.7Cauchy收斂準則272
3.8用Cauchy收斂準則證明Dedekind基本定理275
第4章閉區(qū)間上連續(xù)函數(shù)性質(zhì)的機器證明283
4.1基本定義283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致連續(xù)性定理300
第5章第三代微積分的形式化實現(xiàn)306
5.1預備知識307
5.1.1基本定義307
5.1.2一些引理308
5.2導數(shù)和定積分的初等定義315
5.3積分與微分的新視角324
5.4微積分系統(tǒng)的基本定理346
第6章總結(jié)與注記370
參考文獻375
附錄Coq指令說明386
A.1Coq專用術(shù)語386
A.2Coq證明指令387
A.3集成策略390
索引393
表索引
表1.1書中涉及常用Coq指令簡表8
表1.2書中涉及常用Coq術(shù)語的基本含義13
表6.1分析基礎(chǔ)形式化系統(tǒng)代碼量統(tǒng)計370
表6.2實數(shù)完備性及其等價命題形式系統(tǒng)化代碼量統(tǒng)計371
表6.3閉區(qū)間上連續(xù)函數(shù)性質(zhì)形式化系統(tǒng)代碼量統(tǒng)計371
表6.4第三代微積分形式化系統(tǒng)代碼量統(tǒng)計371
圖索引
圖1.1Landau《分析基礎(chǔ)》的德文-英文版和中文版封面4
圖3.1實數(shù)完備性定理的等價性251
圖3.2實數(shù)的定義與完備性總覽圖282
圖6.1Dedekind基本定理的證明截圖372
圖6.2計算機軟件著作權(quán)登記證書373
展開全部
分析基礎(chǔ)機器證明系統(tǒng) 節(jié)選
第1章 引言 人工智能研究是當前科技發(fā)展的熱點和前沿方向，夯實人工智能基礎(chǔ)理論尤為重要，數(shù)學定理機器證明是人工智能基礎(chǔ)理論的深刻體現(xiàn)，參見文獻[4-6，9，10，13，16，26，59，67-69，78-80，87，134，139，175，180，184186，189，198，201，220]. 1.1 概述 1.1.1 證明輔助工具Coq 數(shù)學定理的計算機形式化證明，近年來隨著計算機科學的迅猛發(fā)展，特別是證明輔助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]的出現(xiàn)，取得了長足的進展[10，67-69，78-80，87，99，201].Coq是一個交互式定理證明與程序開發(fā)系統(tǒng)平臺，是一個用于描述定理內(nèi)容、驗證定理證明的計算機工具.這些定理可能涉及普通數(shù)學、證明理論或程序驗證等[14，35，105，148]多個方面.在推理和編程方面，Coq都擁有足夠強大的表達能力，從構(gòu)造簡單的項、執(zhí)行簡單的證明，直至建立完整的理論、學習復雜的算法等，對學習者的能力有著不同層次的要求[14，35，105，148]. Coq是一個交互式的編譯環(huán)境[14，35，105，148]，用戶以人機對話的方式一問一答，用戶可以邊設(shè)計、邊修改，使證明中的錯誤及時得到補證.Coq系統(tǒng)的基本原理是歸納構(gòu)造演算[14，35，105，148]，是一個形式化系統(tǒng).Coq支持自動推理程序.Coq通過命令式程序進行邏輯推導，可以利用已證命題進行自動推理.Coq中的歸納類型擴展了傳統(tǒng)程序設(shè)計語言中有關(guān)類型定義的概念，類似于大多數(shù)函數(shù)式程序設(shè)計語言中的遞歸類型定義[14，35，105，148].Coq有一支強大的全職研發(fā)隊伍，支持開源.前，Coq已成為數(shù)學定理證明與計算邏輯領(lǐng)域的一個重要工具[7，9，30，148，180].2005年，國際著名計算機專家Gonthier和Werner成功基于Coq給出了著名的“四色定理”的計算機證明[67]，進而，Gonthier等又經(jīng)過六年努力，于2012年完成對“有限單群分類定理”的機器驗證(該證明過程約有4300個定義和15000條定理，約170000行Coq代碼)[10，68，69]，使得證明輔助工具Coq在學術(shù)界得到廣泛認可.2015年，Hales等又HOLLight和Isabelle/HOL[71，145]上完成了對“Kepler猜想”的機器驗證[87]，Wiedijk在文章[183]中指出，全球各相關(guān)研究團隊已經(jīng)或計劃完成包括G.del**不完備性定理、Jordan曲線定理、素數(shù)定理以及Fermat大定理等在內(nèi)的100個著名數(shù)學定理的計算機形式化證明.這些成果使得證明輔助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]在學術(shù)界的影響日益增強 1.1.2形式化數(shù)學 形式化數(shù)學在20世紀初對于數(shù)學基礎(chǔ)的深入討論中受到重視，對整個20世紀數(shù)學的發(fā)展產(chǎn)生了深遠的影響，參見文[2，18，23，39，46，54-56，73，75-77，85，94，95，97，106，109，111，113，115，117，143，159，166，170，173，179，201，209，213]，雖然有時也飽受過于“形式”的詬病[46，85，111，115，153，167]，但20世紀90年代，特別是進入21世紀以來，隨著計算機形式化工具的出現(xiàn)，尤其是上述一系列著名數(shù)學難題形式化證明的實現(xiàn)，使得形式化數(shù)學與形式化證明輔助工具的結(jié)合在學術(shù)界得到極大重視. 著名數(shù)學家和計算機專家Wiedijk認為當前正在進行的形式化數(shù)學是一次數(shù)學革命，他在文章[183]中指出，“數(shù)學歷史上發(fā)生過三次革命.**次是公元前3世紀，古希臘數(shù)學家Euclid在《幾何原本》引入數(shù)學證明方法;第二次是19世紀Cauchy等引入‘嚴格’數(shù)學方法，以及后來的數(shù)理邏輯和集合論;第三次就是當前正在進行的形式化數(shù)學”[26，183].2002年菲爾茲獎獲得者Gowers[72]和Voevodsky[169]、2010年菲爾茲獎獲得者Villani[168]以及1987年沃爾夫獎和2005年阿貝爾獎獲得者Lax都大力倡導發(fā)展可信數(shù)學[98].Gowers在文章[72]中指出，“21世紀計算機在證明定理的過程中會起到巨大作用，理論數(shù)學研究的模式將會徹底改觀，計算機的作用有可能超出我們現(xiàn)在的想象”，甚至預測[72，129]“2099年之前，計算機或可完成所有重要的數(shù)學.計算機會提出猜想、找到證明.而數(shù)學家的工作，是試著去理解和運用其中的一些結(jié)果”.Lax認為“(高速計算機)對于應(yīng)用數(shù)學和純粹數(shù)學的影響可以與望遠鏡對天文學和顯微鏡對生物學的影響相比擬”[98]. 當今數(shù)學論證變得如此復雜，而計算機軟件能夠檢查卷帙浩繁的數(shù)學證明正確性，人類的大腦無法跟上數(shù)學不斷增長的復雜性，計算機檢驗將是唯一的解決方案[168，169].今后，每一本嚴謹?shù)臄?shù)學專著，甚至每一篇數(shù)學論文，都可由計算機檢驗其細節(jié)的正確性，這正發(fā)展為一種趨勢.英國帝國理工學院的數(shù)學教授Buzzard在劍橋舉辦的一次研討會上表示:證明是一種很高的標準，我們不需要數(shù)學家像機器一樣工作，而是可以要他們?nèi)ナ褂脵C器à！關(guān)于數(shù)學定理的形式化證明，必然涉及國際著名的布爾巴基(Bourbaki)學派[18-21].布爾巴基是一群以法國人為主的數(shù)學家的共同名字，他們的思想對于20世紀中葉以來的數(shù)學發(fā)展具有深刻影響[111，115，173].該學派提出數(shù)學結(jié)構(gòu)的概念，并用此概念統(tǒng)一現(xiàn)代數(shù)學[18，111，115，173].按照布爾巴基學派的觀點，數(shù)學中有三大母結(jié)構(gòu)，即序結(jié)構(gòu)[21]、代數(shù)結(jié)構(gòu)[19]和拓撲結(jié)構(gòu)[20].基于這三種結(jié)構(gòu)相互交融形成了現(xiàn)代數(shù)學的主體內(nèi)容.利用交互式定理證明工具Coq，可以完整構(gòu)建這三大母結(jié)構(gòu)的機器證明系統(tǒng)，在此方面國內(nèi)外都開始進行了一些有益的研究工作[9，11，47，57，78-80，83，84，99，130，160-164，180，188，201，203，207]. 1.1.3分析基礎(chǔ) 數(shù)學史上*使人驚奇的事實之一，是實數(shù)系的邏輯基礎(chǔ)竟遲至19世紀后葉才建立起來的[115].而自然數(shù)理論公理體系的建立更是基于Dedekind總結(jié)出的五條基本性質(zhì)[95，173]，以Peano[113]發(fā)表于1889年的《算術(shù)原理——用一種新方法展現(xiàn)》為標志. 經(jīng)歷無數(shù)失敗和挫折之后，為分析數(shù)學尋找基礎(chǔ)的工作逐漸有了眉目，這個過程就是19世紀分析算術(shù)化的實現(xiàn)，于19世紀末期完成，大體包括三個階段，見文獻[2，54，74-77，85，97，106，111，113，115，173]:**階段——極限論建立，主要以法國數(shù)學家Cauchy與德國數(shù)學家Weierstrass的工作為標志;第二階段——實數(shù)理論建立，主要以德國數(shù)學家Dedekind、Cantor與Weierstrass等的實數(shù)構(gòu)造理論為標志;第三階段——算術(shù)化過程完成，以德國數(shù)學家Dedekind與意大利數(shù)學家、邏輯學家Peano的自然數(shù)理論為標志[173].可以看到，分析算術(shù)化的過程與克服數(shù)學史著名的三次危機，即無理數(shù)的發(fā)現(xiàn)、分析的嚴密化、集合論中悖論的消解[179]，是密切相關(guān)的[115]. 德國著名數(shù)學家Landau發(fā)表于1929年的《分析基礎(chǔ):整數(shù)、有理數(shù)、無理數(shù)和復數(shù)的運算(微積分補充教材)》[117](簡稱《分析基礎(chǔ)》)，從Peano五條公設(shè)[113]出發(fā)，依次構(gòu)造了自然數(shù)、分數(shù)、分割、實數(shù)和復數(shù)，并建立了Dedekind實數(shù)完備性定理，即Dedekind基本定理，從而迅速且自然地給出數(shù)學分析的堅實基礎(chǔ)[117]. Landau的名著在世界范圍內(nèi)影響了幾代數(shù)學家，德文本即出版有四個版次，英文翻譯本也至少出版有三個版次[117].在我國，1958年高等教育出版社曾出版有劉紱堂先生翻譯的中文版[117].圖1.1是Landau《分析基礎(chǔ)》的德文-英文版和中文版封面.老一輩數(shù)學家丁石孫[211]、嚴士健[196]、張恭慶[211]等都深受此書影響，并推薦學生研讀.Landau的名著[117]問世以來，又有多部論述實數(shù)理論的專著，例如[49，142，159，177]，相繼出版. 眾所周知，Dedekind基本定理與實數(shù)完備性的幾個著名命題等價，這些命題包括確界存在定理、單調(diào)有界定理、Cauchy-Cantor閉區(qū)間套定理、Heine-Borel-Lebesgue有限覆蓋定理、Bolzano-Weierstrass聚點原理、Bolzano-Weierstrass列緊性定理及Bolzano-Cauchy收斂準則等，而閉區(qū)間上連續(xù)函數(shù)的重要性質(zhì)——有界性定理、*值定理、介值定理、一致連續(xù)性定理——本質(zhì)上也依賴于實數(shù)完備性理論.實數(shù)完備性各命題間等價性及閉區(qū)間上連續(xù)函數(shù)性質(zhì)的人工證明散見于國內(nèi)外“數(shù)學分析”的標準教材，參見文獻[1，3，24，25，27，28，36，42，43，48，50，51，58，64，66，89，100-103，107，119，120，131，149，150，152，165，178，187，191，194，211，223，225-228].實數(shù)完備性是極限論的基礎(chǔ)，上述內(nèi)容一直是數(shù)學分析的重點和難點.近年來仍有人在各類期刊上討論有關(guān)實數(shù)完備性定理的證明，特別指出，廣州大學袁文俊教授在文獻[204，205]中，從上述八大實數(shù)完備性定理中的任何一個定理出發(fā)，放射性地推出其他七個定理，系統(tǒng)總結(jié)了八大實數(shù)完備性定理的相互等價性. 圖1.1Landau《分析基礎(chǔ)》的德文-英文版和中文版封面 20世紀70年代，vanBenthemJutting[13]基于Automath軟件平臺[22，41，144，182]完成Landau《分析基礎(chǔ)》[117]的全部形式化實現(xiàn).這是數(shù)學理論計算機形式化領(lǐng)域里程碑式的工作，影響深遠. Automath[13，22，41，144，182]是為實現(xiàn)數(shù)學的表示，1970年由荷蘭Eindhoven大學deBrujin教授設(shè)計的基于λ類型[135，136]理論的數(shù)學定理證明器，與基于歸納構(gòu)造演算的現(xiàn)代類型理論[9，14，30，35，105，148，180]存在較大差異.基于Automath[22，41，144，182]完成的Landau《分析基礎(chǔ)》[117]形式化代碼[13]，目前看來，在可讀性方面也不能令人滿意[182]. 2011年，德國Saarland大學著名教授Brown[22]提出，將vanBenthemJutting[13]基于Automath[22，41，144，182]完成的Landau《分析基礎(chǔ)》[117]形式化代碼用計算機忠實“翻譯”成Coq代碼的構(gòu)想，這項“翻譯”主要是針對Landau《分析基礎(chǔ)》中公理、定義和定理的形式化描述而言的，針對定理機器證明代碼的“翻譯”難度較大，尚未見報道，相關(guān)的研究似仍在進行中.2011年，Smolka和Brown指導的學生Hornung[99]還給出了基于Coq的Landau《分析基礎(chǔ)》[117]前四章形式化代碼的一個版本.早期關(guān)于實數(shù)理論形式化的工作還包括:Chirimar和Howe[31]基于Nuprl[33]利用Cauchy序列定義實數(shù)，Harrison[90，91]基于Isabelle/HOL[71，145]對實數(shù)的構(gòu)造，Ciaffaglione和DiGianantonio[32]基于Coq直接用無窮序列表達實數(shù)，以及Geuvers和Niqui[60]基于Coq利用Cauchy完備性構(gòu)造實數(shù)等. 1.1.4第三代微積分 微積分是數(shù)學史上*偉大的成就之一，開啟了近代科技的新紀元，對物理學、天文學等其他學科的發(fā)展也起到了重要的促進作用.微積分的創(chuàng)立距今已有三百多年的歷史[111，115，12
書友推薦
- >
小考拉的故事-套裝共3冊
- >
朝聞道
- >
煙與鏡
- >
【精裝繪本】畫給孩子的中國神話
- >
回憶愛瑪儂
- >
李白與唐代文化
- >
自卑與超越
- >
羅庸西南聯(lián)大授課錄
本類暢銷
