典型文献
基于Coq的杨忠道定理形式化证明
文献摘要：
实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.
文献关键词：
Coq;形式化证明;公理化集合论;一般拓扑;拓扑空间;杨忠道定理
中图分类号：
作者姓名：
严升;郁文生;付尧顺
作者机构：
天地互联与融合北京市重点实验室(北京邮电大学 电子工程学院), 北京 100876
文献出处：
引用格式：
[1]严升;郁文生;付尧顺-.基于Coq的杨忠道定理形式化证明)[J].软件学报,2022(06):2208-2223
A类：
Coq,杨忠道定理,宿愿,一般拓扑,一般拓扑学,公理化集合论
B类：
形式化证明,机器证明,吴文俊,院士,生前,深刻理解,拓扑空间,子集,导集,集为,闭集,当此,单点,点集,定理证明,辅助工具,邻域,凝聚点,形式化描述,基本性质,形式化验证,引理,推论,代码,数学定理,可读性,交互性,智能性,过程规范
AB值：
0.210594
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
