作者：郁文生
页数：602
出版社：科学出版社
出版日期：2024
ISBN：9787030775450
高清校对版pdf（带目录）
前往页尾底部查看PDF电子书
内容简介
数系的扩充始终贯穿于数学理论的发展之中.本书利用交互式定理证明工具Coq, 在Morse-Kelley 公理化集合论形式化系统下,给出中国科学与技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统, 包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现, 构建了非标准实数模型, 自然包含标准实数模型, 并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证. 在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过, 充分体现了基于Coq 的数学定理机器证明具有可读性、交互性和智能性的特点, 其证明过程规范、严谨、可靠. 该系统可方便地应用于非标准分析理论的形式化构建.本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材, 也可供从事人工智能相关科研工作者学习参考.
作者简介
第三届杨嘉墀科技奖（2013），吴文俊人工智能科学技术奖自然科学奖（2017）。
目录
“数学机械化丛书”前言
前言
基本符号
第1章 引言
1.1 概述
1.1.1 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 Morse-Kelley公理化集合论系统
1.1.4 关于数系的扩充
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
第2章 Morse-Kelley公理化集合论的形式化系统实现
2.1 分类公理图式
2.2 分类公理图式（续）
2.3 类的初等代数
2.4 集的存在性
2.5 序偶：关系
2.6 函数
2.7 良序
2.8 序
2.9 非负整数
2.10 选择公理
2.11 基数
第3章 滤子构造超有理数的形式化系统实现
3.1 Peano算术的适当展开
3.1.1 加法和乘法
3.1.2 代数运算性质
3.1.3 偶数和奇数
3.2 滤子与超滤
3.3 超滤变换
3.4 算术超滤及其算术模型
3.4.1 算术超滤
3.4.2 最N上的序
3.4.3 最N上的运算
3.4.4 ω嵌入最N
3.5 最N扩张到最Z
3.5.1 等价关系与分类
3.5.2 最N×最N的一个重要分类
3.5.3 最Z上的序
3.5.4 最Z上的运算
3.5.5 最N嵌入最Z
3.6 最Z扩张到最Q
3.6.1 最Z×（最Z～{最Z0
前言
基本符号
第1章 引言
1.1 概述
1.1.1 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 Morse-Kelley公理化集合论系统
1.1.4 关于数系的扩充
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
第2章 Morse-Kelley公理化集合论的形式化系统实现
2.1 分类公理图式
2.2 分类公理图式（续）
2.3 类的初等代数
2.4 集的存在性
2.5 序偶：关系
2.6 函数
2.7 良序
2.8 序
2.9 非负整数
2.10 选择公理
2.11 基数
第3章 滤子构造超有理数的形式化系统实现
3.1 Peano算术的适当展开
3.1.1 加法和乘法
3.1.2 代数运算性质
3.1.3 偶数和奇数
3.2 滤子与超滤
3.3 超滤变换
3.4 算术超滤及其算术模型
3.4.1 算术超滤
3.4.2 最N上的序
3.4.3 最N上的运算
3.4.4 ω嵌入最N
3.5 最N扩张到最Z
3.5.1 等价关系与分类
3.5.2 最N×最N的一个重要分类
3.5.3 最Z上的序
3.5.4 最Z上的运算
3.5.5 最N嵌入最Z
3.6 最Z扩张到最Q
3.6.1 最Z×（最Z～{最Z0
PDF更新中
- THE END -
非特殊说明，本博所有文章均为博主原创。
如若转载，请注明出处：https://www.xiazainiu.com/Wd1qk_5_20513.html
