-
出版时间:
2024-05
-
装帧:
精装
-
开本:
16开
-
ISBN:
9787030775450
-
出版时间:
2024-05
售价
￥
982.00
定价
￥288.00
品相
全新
上书时间2024-10-31
卖家超过10天未登录
-
-
商品描述：
-
导语摘要
数系的扩充始终贯穿于数学理论的发展之中.本书利用交互式定理证明工具Coq, 在Morse-Kelley 公理化集合论形式化系统下,给出中国科学与技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统, 包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现, 构建了非标准实数模型, 自然包含标准实数模型, 并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证. 在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过, 充分体现了基于Coq 的数学定理机器证明具有可读性、交互性和智能性的特点, 其证明过程规范、严谨、可靠. 该系统可方便地应用于非标准分析理论的形式化构建.本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材, 也可供从事人工智能相关科研工作者学习参考.
作者简介
第三届杨嘉墀科技奖（2013），吴文俊人工智能科学技术奖自然科学奖（2017）。
目录
目录
“数学机械化丛书”前言
前言
基本符号
第1章 引言1
1.1 概述1
1.1.1 证明辅助工具Coq1
1.1.2 形式化数学2
1.1.3 Morse-Kelley公理化集合论系统3
1.1.4 关于数系的扩充5
1.1.5 本书结构安排8
1.2 基本Coq指令清单及逻辑预备知识9
第2章 Morse-Kelley公理化集合论的形式化系统实现15
2.1 分类公理图式15
2.2 分类公理图式(续).16
2.3 类的初等代数17
2.4 集的存在性23
2.5 序偶:关系27
2.6 函数33
2.7 良序39
2.8 序47
2.9 非负整数56
2.10 选择公理60
2.11 基数63
第3章 滤子构造超有理数的形式化系统实现88
3.1 Peano算术的适当展开88
3.1.1 加法和乘法89
3.1.2 代数运算性质95
3.1.3 偶数和奇数103
3.2 滤子与超滤109
3.3 超滤变换125
3.4 算术超滤及其算术模型134
3.4.1 算术超滤134
3.4.2 *N上的序138
3.4.3 *N上的运算143
3.4.4 ω嵌入*N165
3.5 *N扩张到*Z177
3.5.1 等价关系与分类177
3.5.2 *N×*N的一个重要分类179
3.5.3 *Z上的序184
3.5.4 *Z上的运算188
3.5.5 *N嵌入*Z208
3.6 *Z扩张到*Q221
3.6.1 *Z×(*Z～{*Z0})的一个重要分类221
3.6.2 *Q上的序226
3.6.3 *Q上的运算230
3.6.4 *N和*Z嵌入*Q255
第4章 什么是实数266
4.1 *Q中的整数和有理数266
4.1.1 非负整数集266
4.1.2 整数集274
4.1.3 有理数集283
4.2 *Q中的无穷289
4.2.1 Archimedes子集与无穷大289
4.2.2 无穷小309
4.3 实数集R317
4.3.1 Q
![]()
孔网啦啦啦啦啦纺织女工火锅店第三课
开播时间：09月02日 10:30
即将开播，去预约
直播中，去观看
占位居中
