分析基礎(chǔ)機(jī)器證明系統(tǒng)

定　價：￥198.00

作　者：	郁文生，付堯順，郭禮權(quán) 著
出版社：	科學(xué)出版社
叢編項：	數(shù)學(xué)機(jī)械化叢書
標(biāo)　簽：	暫缺

購買這本書可以去

ISBN：	9787030706713	出版時間：	2022-01-01	包裝：	精裝
開本：	16開	頁數(shù)：	396	字?jǐn)?shù)：

內(nèi)容簡介

　　《分析基礎(chǔ)機(jī)器證明系統(tǒng)》利用交互式定理證明工具Coq，在樸素集合論的基礎(chǔ)上，從Peano五條公設(shè)出發(fā)，完整實現(xiàn)Landau著名的《分析基礎(chǔ)》中實數(shù)理論的形式化系統(tǒng)，包括對《分析基礎(chǔ)機(jī)器證明系統(tǒng)》中全部5個公設(shè)、73條定義和301個定理Coq描述，其中依次構(gòu)造了自然數(shù)、分?jǐn)?shù)、分割、實數(shù)和復(fù)數(shù)，并建立了Dedekind實數(shù)完備性定理，從而迅速且自然地給出數(shù)學(xué)分析的堅實基礎(chǔ).在分析基礎(chǔ)形式化系統(tǒng)下，給出Dedekind實數(shù)完備性定理與它的幾個著名等價命題間等價性的機(jī)器證明，這些命題包括確界存在定理、單調(diào)有界定理、Cauchy-Cantor閉區(qū)間套定理、Heine-Borel-Lebesgue有限覆蓋定理、Bolzano-Weierstrass聚點原理、Bolzano-Weierstrass列緊性定理及Bolzano-Cauchy收斂準(zhǔn)則等，基于實數(shù)的完備性定理，作為應(yīng)用，進(jìn)一步給出閉區(qū)間上連續(xù)函數(shù)的重要性質(zhì)——有界性定理、*值定理、介值定理、一致連續(xù)性定理——的機(jī)器證明.另外，還給出張景中院士提出的第三代微積分——不用極限的微積分——的形式化系統(tǒng)實現(xiàn).在我們開發(fā)的系統(tǒng)中，全部定理無例外地給出Coq的機(jī)器證明代碼，所有形式化過程已被Coq驗證，并在計算機(jī)上運(yùn)行通過，體現(xiàn)了基于Coq的數(shù)學(xué)定理機(jī)器證明具有可讀性和交互性的特點，其證明過程規(guī)范、嚴(yán)謹(jǐn)、可靠.該系統(tǒng)可方便地應(yīng)用于數(shù)學(xué)分析相關(guān)理論的形式化構(gòu)建.

作者簡介

暫缺《分析基礎(chǔ)機(jī)器證明系統(tǒng)》作者簡介

圖書目錄

目錄
前言
致謝
符號匯集
第1章引言1
1.1概述1
1.1.1證明輔助工具Coq1
1.1.2形式化數(shù)學(xué)2
1.1.3分析基礎(chǔ)3
1.1.4第三代微積分5
1.1.5本書結(jié)構(gòu)安排7
1.2基本Coq指令清單及邏輯預(yù)備知識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補(bǔ)充材料:有限數(shù)的定義及性質(zhì)40
2.2分?jǐn)?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補(bǔ)充材料:實數(shù)運(yùn)算的一些性質(zhì)151
2.4.7補(bǔ)充材料:實數(shù)序列的一些性質(zhì)166
2.5復(fù)數(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共軛復(fù)數(shù)193
2.5.7絕對值195
2.5.8和與積200
2.5.9冪237
2.5.10將實數(shù)編排在復(fù)數(shù)系統(tǒng)中245
第3章實數(shù)完備性等價命題的機(jī)器證明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收斂準(zhǔn)則272
3.8用Cauchy收斂準(zhǔn)則證明Dedekind基本定理275
第4章閉區(qū)間上連續(xù)函數(shù)性質(zhì)的機(jī)器證明283
4.1基本定義283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致連續(xù)性定理300
第5章第三代微積分的形式化實現(xiàn)306
5.1預(yù)備知識307
5.1.1基本定義307
5.1.2一些引理308
5.2導(dǎo)數(shù)和定積分的初等定義315
5.3積分與微分的新視角324
5.4微積分系統(tǒng)的基本定理346
第6章總結(jié)與注記370
參考文獻(xiàn)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計算機(jī)軟件著作權(quán)登記證書373