正版图书 可开发票 品质保证图书
-
作者:
郁文生//付尧顺//郭礼权|责编:王丽平|总主编:吴文俊
-
出版社:
科学
-
ISBN:
9787030706713
-
出版时间:
2022-01
-
装帧:
精装
-
开本:
16开
-
作者:
郁文生//付尧顺//郭礼权|责编:王丽平|总主编:吴文俊
-
出版社:
科学
-
ISBN:
9787030706713
-
出版时间:
2022-01
售价
￥
156.42
7.9折
定价
￥198.00
品相
全新
上书时间2026-02-23
卖家超过10天未登录
-
-
商品描述：
-
目录
前言
致谢
符号汇集
第1章 引言
1.1 概述
1.1.1 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 分析基础
1.1.4 第三代微积分
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
1.3 集合与映射的一些基本概念
第2章 分析基础的形式化系统实现
2.1 自然数
2.1.1 公理
2.1.2 加法
2.1.3 序
2.1.4 乘法
2.1.5 补充材料：有限数的定义及性质
2.2 分数
2.2.1 定义和等价
2.2.2 序
2.2.3 加法
2.2.4 乘法
2.2.5 有理数和整数
2.3 分割
2.3.1 定义
2.3.2 序
2.3.3 加法
2.3.4 乘法
2.3.5 有理分割和整分割
2.4 实数
2.4.1 定义
2.4.2 序
2.4.3 加法
2.4.4 乘法
2.4.5 Dedekind基本定理
2.4.6 补充材料：实数运算的一些性质
2.4.7 补充材料：实数序列的一些性质
2.5 复数
2.5.1 定义
2.5.2 加法
2.5.3 乘法
2.5.4 减法
2.5.5 除法
2.5.6 共轭复数
2.5.7 绝对值
2.5.8 和与积
2.5.9 幂
2.5.10 将实数编排在复数系统中
内容摘要
本书利用交互式定理证明工具Coq,在朴素集合论的基础上,从Peano五条公设出发,完整实现Landau著名的《分析基础》中实数理论的形式化系统,包括对该专著中全部5个公设、73条定义和301个定理Coq描述,其中依次构造了自然数、分数、分割、实数和复数,并建立了Dedekind实数完备性定理,从而迅速且自然地给出数学分析的坚实基础.在分析基础形式化系统下,给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明,这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等,基于实数的完备性定理,作为应用,进一步给出闭区间上连续函数的重要性质——有界性定理、最值定理、介值定理、一致连续性定理——的机器证明.另外,还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现.在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于数学分析相关理论的形式化构建.
![]()
孔网啦啦啦啦啦纺织女工火锅店第三课
开播时间：09月02日 10:30
即将开播，去预约
直播中，去观看
占位居中
