选择公理与Tukey引理等价性的机器证明

• 作者: 孙天宇 郁文生
• 来源期刊: 北京邮电大学学报
• 学科: 工学
• 关键词: 机器证明 形式化数学 选择公理 Tukey引理
• 年，卷（期）: 2019,（5）
• 所属期刊栏目: 论文
• 页码范围: 1-7
• 页数: 7页
• 分类号: TN929.53
• 语种: 中文
• DOI: 10.13190/j.jbupt.2019-001

摘要

基于计算机证明辅助工具Coq,提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上,给出选择公理与Tukey引理的形式化描述,这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码,并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性与交互性特点,其证明过程规范、严谨、可靠,在集合论、拓扑学和代数学的形式化构建中具有重要应用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙天宇	北京邮电大学天地互联与融合北京市重点实验室	1	0	0.0	0.0
2	郁文生	北京邮电大学天地互联与融合北京市重点实验室	4	7	2.0	2.0