MARC状态：审校 文献类型：中文图书 浏览次数：14
- 题名/责任者:
- 自然数的紧化延伸机器证明系统/郁文生, 窦国威著
- 出版发行项:
- 北京:科学出版社,2024
- ISBN及定价:
- 978-7-03-077545-0 精装/CNY288.00
- 载体形态项:
- xvii, 573页:彩图;25cm
- 丛编项:
- 数学机械化丛书;15
- 个人责任者:
- 郁文生 著
- 个人责任者:
- 窦国威 著
- 学科主题:
- 机器证明
- 中图法分类号:
- TP181
- 书目附注:
- 有书目 (第516-524页) 和索引
- 提要文摘附注:
- 本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。
全部MARC细节信息>>
| 索书号 | 条码号 | 年卷期 | 馆藏地 | 书刊状态 | 还书位置 |
| TP181/527 | 2404065 |  自然科学书库-四楼西北（410）
|
可借 | 自然科学书库-四楼西北（410） |
显示全部馆藏信息