| 基于Coq的第三代微积分机器证明系统 |
| |
| 引用本文： | 郭礼权,付尧顺,郁文生.基于Coq的第三代微积分机器证明系统[J].中国科学:数学,2021(1). |
| |
| 作者姓名： | 郭礼权 付尧顺 郁文生 |
| |
| 作者单位： | 北京邮电大学天地互联与融合北京市重点实验室 |
| |
| 基金项目： | 国家自然科学基金(批准号:61936008和61571064)资助项目。 |
| |
| 摘 要： | 本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分|没有极限的微积分|理论构架的形式化验证,包括对张景中等发表的题为\微积分基础的新视角"论文中全部定义和定理的Coq描述.进而,对定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.本文是实践研究人员利用计算机学习、理解、构建乃至教育现代数学理论的一个尝试.
|
| 关 键 词： | 证明辅助工具Coq 第三代微积分 形式化 机器证明 |
A mechanized proof system of the third generation calculus in Coq |
| |
| Liquan Guo,Yaoshun Fu,Wensheng Yu.A mechanized proof system of the third generation calculus in Coq[J].Scientia Sinica Mathemation,2021(1). |
| |
| Authors: | Liquan Guo Yaoshun Fu Wensheng Yu |
| |
| Abstract: | |
| |
| Keywords: | proof assistant Coq the third generation calculus formalization mechanized proof |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
