数系的扩充始终贯穿于数学理论的发展之中. 本书利用交互式定理证明工具Coq, 在Morse-Kelley 公理化集合论形式化系统下, 给出中国科学与技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统, 包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现, 构建了非标准实数模型, 自然包含标准实数模型, 并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证. 在我们开发的系统中, 全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过, 充分体现了基于Coq 的数学定理机器证明具有可读性、交互性和智能性的特点, 其证明过程规范、严谨、可靠. 该系统可方便地应用于非标准分析理论的形式化构建. 本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材, 也可供从事人工智能相关科研工作者学习参考.

更多科学出版社服务，请扫码获取。

第三届杨嘉墀科技奖（2013），吴文俊人工智能科学技术奖自然科学奖（2017）。