- 题名/责任者:
- 公理化集合论机器证明系统/郁文生, 孙天宇, 付尧顺著
- 出版发行项:
- 北京:科学出版社,2020
- ISBN及定价:
- 978-7-03-064039-0 精装/CNY128.00
- 载体形态项:
- xiii, 293页, [1] 页图版:图;25cm
- 丛编项:
- 数学机械化丛书;13
- 个人责任者:
- 郁文生 著
- 个人责任者:
- 孙天宇 著
- 个人责任者:
- 付尧顺 著
- 学科主题:
- 集论公理系统-机器证明
- 中图法分类号:
- O144-39
- 书目附注:
- 有书目 (第284-289页) 和索引
- 提要文摘附注:
- 本书利用交互式定理证明工具 Coq, 实现 Morse-Kelley 公理化集合论形式化系统, 包括对该体系中 8 个公理 (含选择公理)和 1 个公理图示以及全部 181 条定义或定理的Coq 描述, 其中构造了序数和基数, 定义了非负整数, 把Peano公设当作定理, 可以迅速而自然地给出一个数学基础, 摆脱了明显的悖论. 这是 Morse-Kelley公理化集合论系统的首次形式化实现. 在Morse-Kelley公理化集合论形式化系统下, 作为应用, 我们给出选择公理与它的几个著名等价命题间等价性的机器证明。
- 随书光盘:
全部MARC细节信息>>
| 索书号 | 条码号 | 年卷期 | 馆藏地 | 书刊状态 |
| O144-39/1 | 01488876 |  西区3层
|
可借 | |
| O144-39/1 | 01488877 | 总馆
|
可借 |
显示全部馆藏信息