新書推薦：
《
从康德到黑格尔的发展：兼论宗教哲学（英国观念论名著译丛）
》
售價：HK$
60.5
《
突破不可能：用特工思维提升领导力
》
售價：HK$
77.3
《
王阳明大传：知行合一的心学智慧（精装典藏版）
》
售價：HK$
221.8
《
失衡与重塑——百年变局下的中国与世界经济
》
售價：HK$
132.2
《
不被定义的年龄：积极年龄观让我们更快乐、健康、长寿
》
售價：HK$
77.3
《
南方谈话：邓小平在1992
》
售價：HK$
80.6
《
纷纭万端 ： 近代中国的思想与社会
》
售價：HK$
109.8
《
中国古代文体形态研究（第四版）（中华当代学术著作辑要）
》
售價：HK$
168.0
|
| 內容簡介： |
|
《分析基础机器证明系统》利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau著名的《分析基础》中实数理论的形式化系统，包括对《分析基础机器证明系统》中全部5个公设、73条定义和301个定理Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速且自然地给出数学分析的坚实基础.在分析基础形式化系统下，给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质——有界性定理、值定理、介值定理、一致连续性定理——的机器证明.另外，还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现.在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠.该系统可方便地应用于数学分析相关理论的形式化构建.
|
| 目錄：
|
|
目录前言致谢符号汇集第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
|
|
購物車/收銀台(0) | 在線留言板
| 付款方式
| 運費計算
| 聯絡我們
| 幫助中心 |
加入書簽
HOME
新書上架
