首页> 中文会议>2017中国智能物联系统会议 >基于Coq的选择公理及其等价命题的机器实现

基于Coq的选择公理及其等价命题的机器实现

页面导航

摘要
著录项
相似文献
相关主题

摘要

利用交互式定理证明工具Coq,在公理化集合论体系下,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey引理、Hausdorff最大原则、最大原则、Zorn引理、良序原则等.本文从选择公理出发依次证明上述定理,最后又通过良序原则证明了选择公理,从而循环证明了选择公理与这些命题间的等价性.本文体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.

著录项

来源
《2017中国智能物联系统会议》|2017年|326-334|共9页
会议地点厦门
作者
Tianyu Sun; 孙天宇; Wensheng Yu; 郁文生;
展开▼
作者单位

中国仿真学会;

展开▼
会议组织
正文语种
原文格式 PDF
中图分类 TP391.75;
关键词
公理化集合论; 公理选择; 等价命题; 机器证明;

相似文献

中文文献
外文文献
专利

1. 浅谈选择公理及其等价命题 [J] . 高迎 ,石夫磊 . 移动信息 . 2016,第003期
2. 选择公理及其等价命题 [J] . 杨旭 . 吉林师范大学学报（自然科学版） . 2003,第001期
3. 三角范畴定义中八面体公理的等价命题及其应用 [J] . 胡彩霞 ,陈娟 . 厦门大学学报（自然科学版） . 2008,第002期
4. 三角范畴中八面体公理的几个等价命题 [J] . 王济荣 . 四川大学学报（自然科学版） . 2006,第003期
5. 与罗氏平行公理V＊等价的命题补充 [J] . 史明欧 ,朱维宗 . 云南师范大学学报：自然科学版 . 1997,第001期
6. 基于滤子收敛的分离公理的等价刻画 [C] . SHEN Chong ,沈冲 ,YAO Wei . 中国系统工程学会模糊数学与模糊系统专业委员会第十六届学术会议 . 2012
7. 三角范畴定义中八面体公理的等价命题及其应用 [A] . 胡彩霞 . 2007

基于Coq的选择公理及其等价命题的机器实现

摘要

著录项

相似文献

相关主题

期刊订阅