机读格式显示(MARC)
- 010 __ |a 978-7-03-070671-3 |b 精装 |d CNY198.00
- 099 __ |a CAL 012022009716
- 100 __ |a 20220222d2022 em y0chiy50 ea
- 200 1_ |a 分析基础机器证明系统 |A fen xi ji chu ji qi zheng ming xi tong |d = Machine proof system of foundations of analvsis |f 郁文生, 付尧顺, 郭礼权著 |z eng
- 210 __ |a 北京 |c 科学出版社 |d 2022
- 215 __ |a xv, 396页 |c 彩图 |d 25cm
- 225 2_ |a 数学机械化丛书 |A shu xue ji xie hua cong shu |v 14
- 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 |1 2001 |a 数学机械化丛书 |v 14
- 510 1_ |a Machine proof system of foundations of analvsis |z eng
- 606 0_ |a 数学分析 |A shu xue fen xi |x 基础 |x 机器证明
- 701 _0 |a 郁文生 |A yu wen sheng |4 著
- 701 _0 |a 付尧顺 |A fu yao shun |4 著
- 701 _0 |a 郭礼权 |A guo li quan |4 著
- 801 _0 |a CN |b CAU |c 20221005