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