基于Coq的选择公理及其等价命题的机器实现
利用交互式定理证明工具Coq,在公理化集合论体系下,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey引理、Hausdorff最大原则、最大原则、Zorn引理、良序原则等.本文从选择公理出发依次证明上述定理,最后又通过良序原则证明了选择公理,从而循环证明了选择公理与这些命题间的等价性.本文体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.
公理化集合论 公理选择 等价命题 机器证明
孙天宇 郁文生
北京邮电大学,电子工程学院,北京100876
国内会议
厦门
中文
326-334
2017-11-17（万方平台首次上网日期，不代表论文的发表时间）