论文摘要
基于计算机证明辅助工具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)