|
题名:
|
自然数的紧化延伸机器证明系统 / 郁文生, 窦国威著 , |
|
ISBN:
|
978-7-03-077545-0 价格： CNY288.00 |
|
语种:
|
chi |
|
载体形态:
|
xvii, 573页 彩图 25cm |
|
出版发行:
|
出版地： 北京 出版社： 科学出版社 出版日期： 2024 |
|
内容提要:
|
本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。 |
|
主题词:
|
机器证明 |
|
中图分类法:
|
TP181 版次： 5 |
|
主要责任者:
|
郁文生 著 |
|
主要责任者:
|
窦国威 著 |