同类推荐
-
-
拿来即用的AI工具一本通
-
¥49.90
-
-
拿来即用的AI工具一本通
-
¥49.90
-
-
拿来即用的AI工具一本通
-
¥49.90
-
-
腾讯元宝从入门到精通：工作、学习、生活全场景应用指南
-
¥79.00
-
-
无线边缘智能
-
¥79.00
-
-
无线边缘智能
-
¥79.00
-
-
无线边缘智能
-
¥79.00
-
-
AI大模型与智能体企业级实战：DeepSeek+Dif…
-
¥79.00
-
-
联邦学习技术及应用
-
¥79.00
-
-
联邦学习技术及应用
-
¥79.00
|
|
图书信息
|
|
|
|
自然数的紧化延伸机器证明系统
|
| ISBN： | 9787030775450 |
定价： | ￥288.00 |
| 作者： | 郁文生，窦国威著 |
出版社： | 科学出版社 |
| 出版时间： | 2024年05月 |
开本： | 24cm |
| 页数： | 17,573页 |
装祯： | 精装 |
中图法： | TP181 |
相关供货商
|
供货商名称
|
库存量
|
库区
|
更新日期
|
|
北京人天书店有限公司
|
36
|
库区4/库区7/样本4
|
2025-10-22
|
|
其它供货商库存合计
|
184
|
|
2025-10-22
|
图书简介 | | 本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。 |
|