科研之友
微信
新浪微博
Facebook
分享链接
摘要
数学机械化主要是利用计算机实现对数学定理的推理，形式化数学是数学机械化的重要内容。本文利用交互式定理证明工具Coq实现两个重要极限的形式化证明，其中主要包括集合、数列、函数、极限等概念的定义以及相关定理的证明。在此基础上建立级数相关理论体系，实现Cauchy准则、正项级数审敛法、绝对收敛的性质等定理的形式化。通过级数给出正弦函数的形式化定义，并实现两个重要极限的形式化证明。本文涉及的所有代码均在Coq中验证通过，充分体现了Coq的高可信性。
-
单位北京邮电大学; 电子工程学院
