杭州电子科技大学图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

自然数的紧化延伸机器证明系统/郁文生，窦国威著

出版发行项:

北京:科学出版社,2024.05

ISBN及定价:

978-7-03-077545-0/CNY288.00

载体形态项:

602页;24cm

丛编项:

数学机械化丛书

个人责任者:

郁文生 著

个人责任者:

窦国威 著

学科主题:

机器证明

中图法分类号:

TP181

提要文摘附注:

本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。

使用对象附注:

本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材，也可供从事人工智能相关科研工作者学习参考

豆瓣简介：