MARC状态：订购 文献类型：中文图书 浏览次数：6
- 题名/责任者:
- 分析基础机器证明系统/郁文生，付尧顺，郭礼权著
- 出版发行项:
- 北京:科学出版社,2022.01
- ISBN及定价:
- 978-7-03-070671-3 精装/CNY198.00
- 载体形态项:
- 15,396页;25cm
- 中图法分类号:
- O171
- 提要文摘附注:
- 本书利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau著名的《分析基础》中实数理论的形式化系统，包括对该专著中全部5个公设、73条定义和301个定理的Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速而自然地给出数学分析的坚实基础。在分析基础形式化系统下，进而给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理。
- 使用对象附注:
- 数学机械研究人员
全部MARC细节信息>>