分析基础机器证明系统
正版保障 假一赔十 可开发票
￥ 121.97 6.2折 ￥ 198 全新
仅1件
广东广州
认证卖家担保交易快速发货售后保障
作者郁文生,付尧顺,郭礼权
出版社中国科技出版传媒股份有限公司
ISBN9787030706713
出版时间2021-11
装帧精装
开本16开
定价198元
货号11371410
上书时间2024-09-08
商品详情
- 品相描述：全新
- 商品描述
-
目录
目录前言致谢符号汇集第1章引言11.1概述11.1.1证明辅助工具Coq11.1.2形式化数学21.1.3分析基础31.1.4第三代微积分51.1.5本书结构安排71.2基本Coq指令清单及逻辑预备知识71.3集合与映射的一些基本概念13第2章分析基础的形式化系统实现192.1自然数192.1.1公理192.1.2加法222.1.3序262.1.4乘法362.1.5补充材料:有限数的定义及性质402.2分数442.2.1定义和等价442.2.2序462.2.3加法512.2.4乘法562.2.5有理数和整数612.3分割832.3.1定义832.3.2序862.3.3加法892.3.4乘法972.3.5有理分割和整分割1062.4实数1182.4.1定义1182.4.2序.1192.4.3加法1252.4.4乘法1392.4.5Dedekind基本定理1462.4.6补充材料:实数运算的一些性质1512.4.7补充材料:实数序列的一些性质1662.5复数1752.5.1定义1752.5.2加法1772.5.3乘法1812.5.4减法1862.5.5除法1882.5.6共轭复数1932.5.7绝对值1952.5.8和与积2002.5.9幂2372.5.10将实数编排在复数系统中245第3章实数完备性等价命题的机器证明2513.1确界存在定理2513.1.1用Dedekind基本定理证明确界存在定理2513.1.2用确界存在定理证明Dedekind基本定理2543.2单调有界定理2553.3闭区间套定理2563.4有限覆盖定理2583.5聚点原理2643.6列紧性定理2683.7Cauchy收敛准则2723.8用Cauchy收敛准则证明Dedekind基本定理275第4章闭区间上连续函数性质的机器证明2834.1基本定义2834.2有界性定理2904.3最值定理2934.4介值定理2954.5一致连续性定理300第5章第三代微积分的形式化实现3065.1预备知识3075.1.1基本定义3075.1.2一些引理3085.2导数和定积分的初等定义3155.3积分与微分的新视角3245.4微积分系统的基本定理346第6章总结与注记370参考文献375附录Coq指令说明386A.1Coq专用术语386A.2Coq证明指令387A.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
精彩内容
本书利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau著名的《分析基础》中实数理论的形式化系统，包括对该专著中全部5个公设、73条定义和301个定理的Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速而自然地给出数学分析的坚实基础.在分析基础形式化系统下，进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界原理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质--有界性定理、最值定理、介值定理、一致连续性定理--的机器证明.另外，还给出张景中院士提出的第三代微积分--即不用极限的微积分--的形式化系统实现.
相关推荐
— 没有更多了 —
以下为对购买帮助不大的评价