%0 Journal Article
%A 孙天宇
%A 郁文生
%T 选择公理与Tukey引理等价性的机器证明
%D 2019
%R 10.13190/j.jbupt.2019-001
%J 北京邮电大学学报
%P 1-7
%V 42
%N 5
%X 基于计算机证明辅助工具Coq，提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上，给出选择公理与Tukey引理的形式化描述，这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码，并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠，在集合论、拓扑学和代数学的形式化构建中具有重要应用.
%U https://journal.bupt.edu.cn/CN/10.13190/j.jbupt.2019-001