书目信息 |
| 题名： |
分析基础机器证明系统
|
|
| 作者： | 郁文生 ， 付尧顺 ， 郭礼权 著 | |
| 分册： | ||
| 出版信息： | 北京 科学出版社 2022.01 |
|
| 页数： | 15, 396页 | |
| 开本： | 25cm | |
| 丛书名： | 数学机械化丛书 | |
| 单 册： | ||
| 中图分类： | O171 | |
| 科图分类： | ||
| 主题词： | 数学分析--shu xue fen xi--基础--机器证明 | |
| 电子资源： | ||
| ISBN： | 978-7-03-070671-3 | |
| 000 | 01605nam 2200289 450 | |
| 001 | 2260401742 | |
| 010 | @a978-7-03-070671-3@b精装@dCNY198.00 | |
| 100 | @a20220222d2022 em y0chiy50 ea | |
| 101 | 0 | @achi |
| 102 | @aCN@b110000 | |
| 105 | @ay a 001yy | |
| 106 | @ar | |
| 200 | 1 | @a分析基础机器证明系统@Afen xi ji chu ji qi zheng ming xi tong@d= Machine proof system of foundations of analysis@f郁文生, 付尧顺, 郭礼权著@zeng |
| 210 | @a北京@c科学出版社@d2022.01 | |
| 215 | @a15, 396页@d25cm | |
| 225 | 2 | @a数学机械化丛书@Ashu xue ji xie hua cong shu@v14 |
| 320 | @a有书目 (第375-385页) 和索引 | |
| 330 | @a本书利用交互式定理证明工具Coq, 在朴素集合论的基础上, 从Peano五条公设出发, 完整实现Landau著名的《分析基础》中实数理论的形式化系统, 包括对该专著中全部5个公设、73条定义和301个定理的Coq描述, 其中依次构造了自然数、分数、分割、实数和复数, 并建立了Dedekind实数完备性定理, 从而迅速而自然地给出数学分析的坚实基础。在分析基础形式化系统下, 进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明, 这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等, 基于实数的完备性定理。 | |
| 410 | 0 | @12001 @a数学机械化丛书@v14 |
| 510 | 1 | @aMachine proof system of foundations of analysis@zeng |
| 606 | 0 | @a数学分析@Ashu xue fen xi@x基础@x机器证明 |
| 690 | @aO171@v5 | |
| 701 | 0 | @a郁文生@Ayu wen sheng@4著 |
| 701 | 0 | @a付尧顺@Afu yao shun@4著 |
| 701 | 0 | @a郭礼权@Aguo li quan@4著 |
| 801 | 0 | @aCN@c20220906 |
| 905 | @a河南城建学院图书馆@dO171@eY849 | |
| 分析基础机器证明系统= Machine proof system of foundations of analysis/郁文生, 付尧顺, 郭礼权著.-北京：科学出版社，2022.01 |
| 15, 396页；25cm.-(数学机械化丛书；14) |
| ISBN 978-7-03-070671-3(精装)：CNY198.00 |
| 本书利用交互式定理证明工具Coq, 在朴素集合论的基础上, 从Peano五条公设出发, 完整实现Landau著名的《分析基础》中实数理论的形式化系统, 包括对该专著中全部5个公设、73条定义和301个定理的Coq描述, 其中依次构造了自然数、分数、分割、实数和复数, 并建立了Dedekind实数完备性定理, 从而迅速而自然地给出数学分析的坚实基础。在分析基础形式化系统下, 进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明, 这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等, 基于实数的完备性定理。 |
| ● |
| 相关链接 |
|
|
|
正题名：分析基础机器证明系统
索取号：O171/Y849
预约/预借
| 序号 | 登录号 | 条形码 | 馆藏地/架位号 | 状态 | 备注 |
| 1 | 1572823 | 215728238 | 自科库401/401自科库 43排7列1层/ [索取号:O171/Y849] | 在馆 |