MARC状态：审校 文献类型：中文图书 浏览次数：12
- 题名/责任者:
- 分析基础机器证明系统/郁文生, 付尧顺, 郭礼权著
- 出版发行项:
- 北京:科学出版社,2022
- ISBN及定价:
- 978-7-03-070671-3 精装/CNY198.00
- 载体形态项:
- xv, 396页:彩图;25cm
- 丛编项:
- 数学机械化丛书;14
- 个人责任者:
- 郁文生 著
- 个人责任者:
- 付尧顺 著
- 个人责任者:
- 郭礼权 著
- 学科主题:
- 数学分析-基础-机器证明
- 中图法分类号:
- O171
- 书目附注:
- 有书目 (第375-385页) 和索引
- 提要文摘附注:
- 本书利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau著名的《分析基础》中实数理论的形式化系统，包括对《分析基础机器证明系统》中全部5个公设、73条定义和301个定理Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速且自然地给出数学分析的坚实基础。在分析基础形式化系统下，给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质—有界性定理、最值定理、介值定理、一致连续性定理—的机器证明。
- 随书光盘:
全部MARC细节信息>>
总馆