基于MK的实数公理系统相容性和范畴性的Coq形式化
郭达凯
冷姝锟
窦国威
陈思
郁文生
北京邮电大学电子工程学院天地互联与融合北京市重点实验室,北京 100876
摘要：数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程己被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!
关键词：Morse-Kelley公理化集合论实数公理系统相容性范畴性Coq形式化机器证明人工智能
论文发表日期：2024-07-28
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：12( 1274-1285 )
英文信息