ISBN/价格: | 978-7-03-070671-3:CNY198.00 |
---|---|
作品语种: | chi |
出版国别: | CN 110000 |
题名责任者项: | 分析基础机器证明系统/.郁文生, 付尧顺, 郭礼权著 |
出版发行项: | 北京:,科学出版社:,2022.01 |
载体形态项: | 15, 396页:;+25cm |
丛编项: | 数学机械化丛书 |
提要文摘: | 本书利用交互式定理证明工具Coq, 在朴素集合论的基础上, 从Peano五条公设出发, 完整实现Landau著名的《分析基础》中实数理论的形式化系统, 包括对该专著中全部5个公设、73条定义和301个定理的Coq描述, 其中依次构造了自然数、分数、分割、实数和复数, 并建立了Dedekind实数完备性定理, 从而迅速而自然地给出数学分析的坚实基础。在分析基础形式化系统下, 进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明, 这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等, 基于实数的完备性定理。 |
并列题名: | Machine proof system of foundations of analysis eng |
题名主题: | 数学分析 基础 机器证明 |
中图分类: | O171 |
个人名称等同: | 郁文生 著 |
个人名称等同: | 付尧顺 著 |
个人名称等同: | 郭礼权 著 |
记录来源: | CN 人天书店 20220514 |