分析基礎機器證明系統

內容簡介

本書利用互動式定理證明工具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

分析基礎機器證明系統

基本介紹

內容簡介

作者簡介

圖書目錄

相關詞條

熱門詞條