自然数的紧化延伸机器证明系统 人工智能 郁文生,窦国威 新华正版
￥ 195.44 6.8折 ￥ 288 全新
库存9件
河北保定
认证卖家担保交易快速发货售后保障
作者郁文生,窦国威
出版社科学出版社
ISBN9787030775450
出版时间2024-05
版次1
装帧平装
开本16
页数600页
字数756千字
定价288元
货号xhwx_1203303132
上书时间2024-07-02
- 最新上架
商品详情
- 品相描述：全新
- 正版特价新书
- 商品描述
-
目录：
目录
“数学机械化丛书”前言
前言
基本符号
章 引言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<上的一个重要分类317
4.3.2 r上的序321
4.3.3 r上的运算325
4.4 r中的整数和有理数348
4.4.1 非负整数集348
4.4.2 整数集355
4.4.3 有理数集368
4.4.4 archimedes与稠密379
4.5 数列和完备383
4.5.1 ω上的数列及其延伸383
4.5.2 q上的数列及其延伸388
4.5.3 r上的数列402
4.5.4 实数完备411
4.6 无理数的存在418
4.6.1 数列和运算的补充质418
4.6.2 一些具体数列433
4.6.3 算术方根和无理数446
4.7 实数是什么457
第5章 非主算术超滤的存在461
5.1 滤子扩张原则461
5.2 一些引理467
5.3 连续统设蕴含非主算术超滤存在497
第6章 结论与注记509
参文献516
附录一 coq指令说明525
a.1 coq专用术语525
a.2 coq证明指令526
a.3 集成策略529
附录二 公理化集合论与实数公理化的结构呈现532
索引569
表目录
表1.1 书中涉及常用coq指令简表10
表1.2 书中涉及常用coq术语的基本含义13
表4.1 数系扩充符号汇集457
表6.1 公理化集合论形式化系统代码量统计509
表6.2 滤子构造超有理数形式化系统代码量统计510
表6.3 实数形式化系统代码量统计510
表6.4 非主算术超滤存在形式化系统代码量统计510
图目录
图1.1 kelley《一般拓扑学》的英文版和中文版封面4
图1.2 landau《分析基础》的德文-英文版和中文版封面6
图1.3 汪芳庭《数学基础》的两个版本封面8
图3.1 滤子各概念之间的关系示意图138
图3.2 *z=(*n×*n)/r示意图184
图3.3 *q=(*z×(*z～{*z0}))/r示意图226
图4.1 从ω扩充至*q过程示意图458
图4.2 *q结构与r结构之间的关系图459
图6.1 实数完备的证明截图511
图6.2 计算机软件著作权登记512
图6.3 lean验证数学定理输出的命题和概念网络513
图6.4 lean验证多项式freiman-ruzsa猜想输出的blueprint图514
内容简介：
数系的扩充始终贯穿于数学理论的发展之中.本书利用交互式定理证明工具coq 在morekelley 公理化集合论形式化系统下给出学与技术大学汪芳庭教授在其数学基础中采用算术超滤分数构造实数的机器证明系统 包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现 构建了非标准实数模型 自然包含标准实数模型 并且给出滤子扩张原则和连续统设蕴含非主算术超滤存在的形式化验证. 在我们开发的系统中定理无例外地给出coq的机器证明代码 所有形式化过程已被coq验证 并在计算机上运行通过 充分体现了基于coq 的数学定理机器证明具有可读、交互和智能的特点 其证明过程规范、严谨、可靠. 该系统可方便地应用于非标准分析理论的形式化构建.本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或教材 也可供从事人工智能相关科研工作者学参.
— 没有更多了 —
以下为对购买帮助不大的评价