isbn9787030706713

分析基础机器证明系统

《分析基础机器证明系统》,作者:郁文生,付尧顺,郭礼权 著 出版社:科学出版社 ISBN:9787030706713。本书利用交互式定理证明工具Coq,在朴素集合论的基础上,从Peano五条公设出发,完整实现Landau著名的《分析基础》中实数理论的形式化系统,包括对该专著中全部5个公设、73条定义和301个定理Coq描述,其中依次构造了自然数、分数、分割、实数和复数,并建立了Dedekind实数