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

183 0

2024-12-10 12:50 | 查看全部阅读模式

文档名：基于Coq的选择公理及其等价命题的机器实现
利用交互式定理证明工具Coq,在公理化集合论体系下,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey引理、Hausdorff最大原则、最大原则、Zorn引理、良序原则等.本文从选择公理出发依次证明上述定理,最后又通过良序原则证明了选择公理,从而循环证明了选择公理与这些命题间的等价性.本文体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.
作者：孙天宇郁文生
作者单位：北京邮电大学,电子工程学院,北京100876
母体文献：2017中国智能物联系统会议论文集
会议名称：2017中国智能物联系统会议
会议时间：2017年11月17日
会议地点：厦门
主办单位：中国仿真学会
语种：chi
分类号：O15O14
关键词：公理化集合论公理选择等价命题机器证明
在线出版日期：2020年6月23日
基金项目：
相似文献
相关博文

2024-12-10 12:50 上传

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

文件大小:: 1.35 MB

下载次数:: 60

高速下载

基于, Coq, 选择, 公理, 及其

【温馨提示】您好！以下是下载说明，请您仔细阅读：
1、推荐使用360安全浏览器访问本站，选择您所需的PDF文档，点击页面下方“下载”按钮。
2、耐心等待两秒钟，系统将自动开始下载，本站文件均为高速下载。
3、下载完成后，请查看您浏览器的下载文件夹，找到对应的PDF文件。
4、使用PDF阅读器打开文档，开始阅读学习。
5、使用过程中遇到问题，请联系QQ客服。

本站提供的所有PDF文档、软件、资料等均为网友上传或网络收集，仅供学习和研究使用，不得用于任何商业用途。
本站尊重知识产权，若本站内容侵犯了您的权益，请及时通知我们，我们将尽快予以删除。

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

相关文档