基于Coq的有标集族相关定理的机器证明

• 作者: 付尧顺 刘佳 吕红伟 郁文生
• 来源期刊: 伊犁师范学院学报（自然科学版）
• 学科: 数学
• 关键词: Coq 机器证明 公理化集合论 有标集族
• 年，卷（期）: 2020,（2）
• 所属期刊栏目: 数学与应用数学
• 页码范围: 13-22
• 页数: 10页
• 分类号: O212.1
• 语种: 中文

摘要

基于计算机证明辅助工具Coq,参考"公理化集合论"形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了Coq的规范、严谨、可靠.为构建完整的点集拓扑理论打下基础,在此系统下,有望实现拓扑空间相关性质的形式化系统.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘佳		7	15	3.0	3.0
2	郁文生		4	7	2.0	2.0
3	吕红伟		1	0	0.0	0.0
4	付尧顺		1	0	0.0	0.0