您的位置：首页 > 论文页面
基于Coq的两个重要极限的形式化证明
发表时间：2021-06-19 浏览量：871 下载量：182
| 全部作者： | 赵保强，于畅，郁文生 |
| 作者单位： | 北京邮电大学电子工程学院 |
| 摘 要： | 数学机械化主要是利用计算机实现对数学定理的推理，形式化数学是数学机械化的重要内容。本文利用交互式定理证明工具Coq实现两个重要极限的形式化证明，其中主要包括集合、数列、函数、极限等概念的定义以及相关定理的证明。在此基础上建立级数相关理论体系，实现Cauchy准则、正项级数审敛法、绝对收敛的性质等定理的形式化。通过级数给出正弦函数的形式化定义，并实现两个重要极限的形式化证明。本文涉及的所有代码均在Coq中验证通过，充分体现了Coq的高可信性。 |
| 关 键 词： | 人工智能；极限；形式化验证；定理机器证明；级数；Coq |
| Title： | A formal proof of two important limits in Coq |
| Author： | ZHAO Baoqiang, YU Chang, YU Wensheng |
| Organization： | School of Electronic Engineering, Beijing University of Posts and Telecommunications |
| Abstract： | Mathematical mechanization mainly uses computers to realize the reasoning of mathematical theorems, and formal mathematics is an important content of mathematical mechanization. In this paper, the interactive theorem proving tool Coq is used to realize the formal proof of two important limits, which includes the definition of concepts such as set, sequence, function, limit and the proof of related theorems. On this basis, the related theoretical system of series is established to realize the formalization of the theorems such as Cauchy criterion, convergence method of positive series and the nature of absolute convergence. The formal definition of the sine function is given through the series, and the formal proof of two important limits is realized. All codes involved in this paper have been verified in Coq, which fully reflects the high credibility of Coq. |
| Key words： | artificial intelligence; limit; formal verification; mechanical theorem proving; series; Coq |
| 发表期数： | 2021年6月第2期 |
| 引用格式： | 赵保强，于畅，郁文生. 基于Coq的两个重要极限的形式化证明[J]. 中国科技论文在线精品论文，2021，14（2）：177-186. |
4
评论数 0请您登录
暂无评论
下载全文
多维论文