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

论文摘要

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

论文目录

文章来源

类型: 期刊论文

作者: 孙天宇,郁文生

关键词: 机器证明,形式化数学,选择公理,引理

来源: 北京邮电大学学报 2019年05期

年度: 2019

分类: 信息科技,基础科学

专业: 数学,自动化技术

单位: 北京邮电大学天地互联与融合北京市重点实验室

基金: 国家自然科学基金项目(61571064,61936008)

分类号: TP18;O144

DOI: 10.13190/j.jbupt.2019-001

页码: 1-7

总页数: 7

文件大小: 141K

下载量: 59

相关论文文献

• [1].单目视觉Tukey权因子模型室内位置测量[J]. 遥感学报 2020(01)
• [2].单因素分析-Tukey法比较鬼针草挥发油β-环糊精3种包合工艺[J]. 中国医院药学杂志 2015(20)
• [3].基于Tukey法改进时间序列平稳性检验的分段检验法[J]. 统计与决策 2018(16)
• [4].基于Tukey怀疑度模型旅游线路M估计协同推荐[J]. 湖南工业大学学报 2018(04)

本文来源: https://www.lunwen66.cn/article/e9be9fe3802b7a8c370f2160.html