分析基础机器证明系统

图书标准信息

• 作者 郁文生；付尧顺；郭礼权
• 出版社 科学出版社
• 出版时间 2022-01
• 版次 1
• ISBN 9787030706713
• 定价 198.00元
• 装帧 精装
• 开本 16开
• 纸张 胶版纸
• 页数 396页
• 字数 500.000千字

【内容简介】

《分析基础机器证明系统》利用交互式定理证明工具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