控制理论与应用

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

单位：北京邮电大学电子工程学院,北京邮电大学电子工程学院,北京邮电大学电子工程学院,北京邮电大学电子工程学院,北京邮电大学电子工程学院

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

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

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

来源：2024年第7期

《控制理论与应用》期刊编辑部

查看控制理论与应用杂志2024年第7期