机读格式显示(MARC)

• 000 01449oam2 2200277 450

• 001 0000792163

• 005 20250725212300.0

• 010 __ |a 978-7-03-077545-0 |b 精装 |d CNY288.00

• 100 __ |a 20240711d2024 em y0chiy50 ea

• 101 0_ |a chi

• 102 __ |a CN |b 110000

• 105 __ |a ak a 001yy

• 106 __ |a r

• 200 1_ |a 自然数的紧化延伸机器证明系统 |A zi ran shu de jin hua yan shen ji qi zheng ming xi tong |f 郁文生, 窦国威著

• 210 __ |a 北京 |c 科学出版社 |d 2024

• 215 __ |a xvii, 573页 |c 彩图 |d 25cm

• 225 2_ |a 数学机械化丛书 |A shu xue ji xie hua cong shu |v 15

• 320 __ |a 有书目 (第516-524页) 和索引

• 330 __ |a 本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。

• 410 _0 |1 2001 |a 数学机械化丛书 |v 15

• 606 0_ |a 机器证明 |A ji qi zheng ming

• 690 __ |a TP181 |v 5

• 701 _0 |a 郁文生 |A yu wen sheng |4 著

• 701 _0 |a 窦国威 |A dou guo wei |4 著

• 801 _0 |a CN |b WFKJXY |c 20250725

• 905 __ |a WFKJXY |d TP181/527