• 
  分析基础机器证明...
  ￥156.42元
• 
  近世计算理论导引
  ￥15.80元
• 
  方程求解与机器证...
  ￥93.22元
• 
  可积系统与计算机...
  ￥25.28元
• 
  消去法及其应用
  ￥37.92元
• 
  实域论
  ￥40.00元
• 
  进程代数——对称...
  ￥19.75元
• 
  数学机械化（中文...
  ￥116.92元
• 
  交互式马尔可夫链...
  ￥22.12元
• 
  多项式系统的实根...
  ￥23.70元
• 
  不等式机器证明与...
  ￥69.52元
• 
  实域论
  ￥47.40元
• 
  复杂非线性波的构...
  ￥101.12元
• 
  数学机械化
  ￥116.92元
• 
  公理化集合论机器...
  ￥101.12元
• 
  自然数的紧化延伸...
  ￥227.52元

本书利用交互式定理证明工具Coq,在朴素集合论的基础上,从Peano五条公设出发,完整实现Landau著名的《分析基础》中实数理论的形式化系统,包括对该专著中全部5个公设、73条定义和301个定理Coq描述,其中依次构造了自然数、分数、分割、实数和复数,并建立了Dedekind实数完备性定理,从而迅速且自然地给出数学分析的坚实基础.在分析基础形式化系统下,给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明,这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等,基于实数的完备性定理,作为应用,进一步给出闭区间上连续函数的重要性质——有界性定理、最值定理、介值定理、一致连续性定理——的机器证明.另外,还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现.在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于数学分析相关理论的形式化构建.

样章试读

• 暂时还没有任何用户评论

总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

全部咨询(共0条问答)

• 暂时还没有任何用户咨询内容

总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

用户名：	匿名用户
E-mail：
咨询内容：

• 目录
  前言
  致谢
  符号汇集
  第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