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