文献类型：期刊文章

作　　者：郭达凯[1] 冷姝锟[1] 窦国威[1] 陈思[1] 郁文生[1]

GUO Da-kai;LENG Shu-kun;DOU Guo-wei;CHEN Si;YU Wen-sheng(Beijing Key Laboratory of Space-Ground Interconnection and Convergence,School of Electronic Engineering,Beijing University of Posts and Telecommunications,Beijing 100876,China)

机构地区：[1]北京邮电大学电子工程学院天地互联与融合北京市重点实验室,北京100876

出　　处：《控制理论与应用》

基　　金：国家自然科学基金项目(61936008)资助。

年　　份：2024

卷　　号：41

期　　号：7

起止页码：1274-1285

语　　种：中文

收录情况：AJ、BDHX、BDHX2023、CAS、CSCD、CSCD2023_2024、EI、INSPEC、JST、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!

关 键 词：Morse-Kelley公理化集合论  实数公理系统  相容性 范畴性 COQ 形式化 机器证明  人工智能  

分 类 号：TP18]