《分析基础机器证明系统》利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau著名的《分析基础》中实数理论的形式化系统，包括对《分析基础机器证明系统》中全部5个公设、73条定义和301个定理Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速且自然地给出数学分析的坚实基础.在分析基础形式化系统下，给出Dedekind实数完备性定理与它的几个著名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质——有界性定理、*值定理、介值定理、一致连续性定理——的机器证明.另外，还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现.在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠.该系统可方便地应用于数学分析相关理论的形式化构建.
鄂公网安备 42010302001612号 