北京邮电大学学报 ›› 2019, Vol. 42 ›› Issue (5): 1-7.doi: 10.13190/j.jbupt.2019-001
• 论文 • 下一篇
选择公理与Tukey引理等价性的机器证明
孙天宇, 郁文生
- 北京邮电大学 天地互联与融合北京市重点实验室, 北京 100876
-
收稿日期:
2019-01-19出版日期:
2019-10-28发布日期:
2019-11-25 -
作者简介:
孙天宇(1993-),男,博士生,E-mail:stycyj@bupt.edu.cn;郁文生(1967-),男,教授,博士生导师. -
基金资助:
国家自然科学基金项目(61571064,61936008)
A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma
SUN Tian-yu, YU Wen-sheng
- Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China
-
Received:
2019-01-19Online:
2019-10-28Published:
2019-11-25
摘要: 基于计算机证明辅助工具Coq,提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上,给出选择公理与Tukey引理的形式化描述,这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码,并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠,在集合论、拓扑学和代数学的形式化构建中具有重要应用.
中图分类号:
引用本文
孙天宇, 郁文生. 选择公理与Tukey引理等价性的机器证明[J]. 北京邮电大学学报, 2019, 42(5): 1-7.
SUN Tian-yu, YU Wen-sheng. A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma[J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2019, 42(5): 1-7.
[1] Jech T. The axiom of choice[M]. Amsterdam:North Holland Publishing Company, 1973:1-56. [2] Bernays P, Fraenkel A A. Axiomatic set theory[M]. Amsterdam:North Holland Publishing Company, 1958:1-73. [3] Bertot Y, Castéran P. Interactive theorem proving and program development, Coq'art:the calculus of inductive constructions[M]. Heidelberg:Springer, 2004:1-11. [4] Gonthier G. Formal proof-the four color theorem[J]. Notices of the American Mathematical Society, 2008, 55(11):1382-1393. [5] Gonthier G, Asperti A, Avigad J, et al. Machine-checked proof of the odd order theorem[C]//ITP 2013. Heidelberg:Springer, 2013:163-179. [6] Wiedijk F. Formal proof-getting started[J]. Notices of the American Mathematical Society, 2008, 55(11):1408-1414. [7] Wang Hao. On Zermelo's and Von Neumann's axioms for set theory[J]. Proc Natl Acad Sci USA, 1949, 35(3):150-155. [8] Kelley J L. General topology[M]. New York:Springer-Verlag, 1955:250-281. [9] Sun Tianyu. Axiomatic set theory[EB/OL]. (2018-10-20)[2018-12-10]. https://github.com/styzystyzy/Axiomatic_Set_Theory/. [10] Werner B. Sets in types, types in sets[C]//Proceedings of TACS' 97. Heidelberg:Springer, 1997:530-546. [11] Barras B. Sets in Coq, Coq in sets[J]. Journal of Formalized Reasoning, 2010, 3(1):29-48. [12] Kirst D, Smolka G. Categoricity results for second-order ZF in dependent type theory[C]//ITP 2017. Heidelberg:Springer, 2017:304-318. [13] Paulson L C. The relative consistency of the axiom of choice mechanized using Isabelle/ZF[J]. LMS Journal of Computation and Mathematics, 2003(6):98-248. [14] Sun Tianyu, Yu Wensheng. Machine proving system for mathematical theorems based on Coq-machine proving of Hausdorff maximal principle and Zermelo postulate[C]//Proceedings of the 36th Chinese Control Conference. New York:IEEE, 2017:9871-9878. [15] 熊金城. 点集拓扑讲义[M]. 北京:高等教育出版社, 2011:36-40. [16] Sun Tianyu. Tukey's lemma and AC[EB/OL]. (2018-11-30)[2018-12-10]. https://github.com/BKLSIC/Tukey_AC/. |
[1] | 章晨宇 温向明 陈亚文. 蜂窝移动网络低成本高精度授时[J]. 北京邮电大学学报, 2023, 46(1): 103-108. |
[2] | 郭令奇 褚智贤 廖建新 王敬宇 陆璐. 意图驱动的自智网络资源按需服务[J]. 北京邮电大学学报, 2022, 45(6): 85-91. |
[3] | 初星河, 路兆铭, 王鲁晗, 武穆清, 温向明. 多径信号辅助的网联车辆无线协作定位[J]. 北京邮电大学学报, 2021, 44(2): 116-123. |
[4] | 张天魁, 王筱斐, 杨立伟, 杨鼎成. 移动网络SFC部署与计算资源分配联合算法[J]. 北京邮电大学学报, 2021, 44(1): 7-13. |
[5] | 吕廷杰, 宋罗娜, 滕颖蕾, 丰业媛. 面向生态可持续的下一代通信网络架构与评价体系[J]. 北京邮电大学学报, 2020, 43(6): 18-26,35. |
[6] | 何建华, 赵辉, 徐晓斌, 闫蕾, 王尚广. 基于改进双层LT码的天基物联网数据收集方法[J]. 北京邮电大学学报, 2020, 43(6): 118-125. |
[7] | 马璐, 刘铭, 李超, 路兆铭, 马欢. 面向6G边缘网络的云边协同计算任务调度算法[J]. 北京邮电大学学报, 2020, 43(6): 66-73. |
[8] | 管婉青, 张海君, 路兆铭. 基于DRL的6G多租户网络切片智能资源分配算法[J]. 北京邮电大学学报, 2020, 43(6): 132-139. |
[9] | 罗轶, 王雨婷, 施荣华, 严梦纯, 曾豪. 能量采集衬底式认知协作中继网络安全中断概率分析[J]. 北京邮电大学学报, 2020, 43(3): 105-111,124. |
[10] | 李君瑶, 常永宇, 曾天一. 大规模3D MIMO中基于信道相关的LOS/NLOS识别算法[J]. 北京邮电大学学报, 2020, 43(1): 1-7. |
[11] | 蒋芳, 张南飞, 胡艳军, 王翊. 基于BP神经网络的CSI无源目标分类方法[J]. 北京邮电大学学报, 2020, 43(1): 40-45. |
[12] | 任佳智, 田辉, 聂高峰. 基于本地内容流行度预测的主动缓存策略[J]. 北京邮电大学学报, 2020, 43(1): 80-91. |
[13] | 徐九韵, 孙忠顺, 张如如. 基于链路预测的手机节能方法[J]. 北京邮电大学学报, 2020, 43(1): 8-13,27. |
[14] | 李晓辉, 杜洋帆, 石潇竹, 杨胥. 基于信道模糊关联识别的NLOS测距误差补偿算法[J]. 北京邮电大学学报, 2020, 43(1): 21-27. |
[15] | 李鹏, 王德勇, 师文喜, 姜志国. 大数据环境下基于深度学习的行人再识别[J]. 北京邮电大学学报, 2019, 42(6): 29-34. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||