-
分析基础机器证明系统
¥142.6(7.2折)定价:¥198.0本书利用交互式定理证明工具Coq,在朴素集合论的基础上,从Peano五条公设出发,完整实现Landau有名的《分析基础》中实数理论的形式化系统,包括对该专著中全部5个公设、73条定义和301个定理的Coq描述,其中依次构造了自然数、分数、分割、实数和复数,并建立了Dedekind实数完备性定理,从而迅速且自然地给出数学分析的坚实基础。在分析基础形式化系统下,给出Dedekind实数完备性定理与它的几个有名等价命题间等价性的机器证明,这