图书信息:

丛 书 名:数学机械化丛书
中文书名:公理化集合论机器证明系统
英文书名:Machine Proof System of Axiomatic Set Theory 
作  者:郁文生,孙天宇,付尧顺 著
出 版 社:科学出版社
出版日期:2020年3月
定  价:128.00元
语  种:中文
I S B N:9787030640390
页  数:293页

作者简介:   

  郁文生,1998年毕业于北京大学,获理学博士学位。现为北京邮电大学教授,博士生导师,天地互联与融合北京市重点实验室副主任,中国仿真学会智能物联系统建模与仿真专业委员会副主任委员、中国自动化学会控制理论专业委员会委员等。曾任中国科学院自动化所研究员、博士生导师,华东师范大学教授,博士生导师。2013年获杨嘉墀科技奖。2017年获吴文俊人工智能自然科学奖。现主持国家自然科学基金重点项目“基于Coq的布尔巴基数学机器证明系统及其应用”。在系统鲁棒控制理论、时滞系统稳定性分析、线性系统同时镇定及数学定理机器证明等方面做出一系列创新性成果,论文发表于《中国科学》、《科学通报》、《IEEE Trans.》系列等国内外重要学术刊物。曾应邀赴澳大利亚墨尔本大学作高级访问学者。曾多次赴美国、英国、澳大利亚、西班牙、日本及中国香港等国家和地区参加国际性学术会议。研究兴趣为数学定理机器证明与人工智能等。

内容简介:   

  布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础。利用计算机证明辅助工具,可以完整构建这三大母结构的形式化系统。本书利用交互式定理证明工具Coq,实现Morse-Kelley 公理化集合论形式化系统,包括对该体系中8个公理(含选择公理)和1个公理图示以及全部181条定义或定理的Coq 描述,其中构造了序数和基数,定义了非负整数,把Peano公设当作定理,可以迅速而自然地给出一个数学基础,摆脱了明显的悖论。这是Morse-Kelley公理化集合论系统的首次形式化实现。在Morse-Kelley公理化集合论形式化系统下,作为应用,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey 引理、Hausdorff 极大原则、极大原则、Zorn 引理、良序定理及Zermelo 假定等。在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq 的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建。
  本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材,也可供从事人工智能相关科研工作者学习参考。

目录:

第1章 引言
第2章 基本Coq指令清单和预备知识
第3章 Morse-Kelley公理化集合论的形式化系统实现
3.1 分类公理图式
3.2 分类公理图式(续)
3.3 类的初等代数
3.4 集的存在性
3.5 序偶:关系
3.6 函数
3.7 良序
3.8 序数
3.9 非负整数
3.10 选择公理
3.11 基数
第4章 选择公理及其等价命题的机器证明
4.1 基本定义
4.2 Tukey 引理
4.3 Hausdorff 极大原则
4.4 极大原则
4.5 Zermelo 假定
4.6 Zorn 引理
4.7 良序定理
4.8 良序定理证明选择公理
4.9 Zermelo假定证明选择公理
4.10 Tukey引理证明选择公理
第5章 结论与注记
参考文献
索引


  控制理论专业委员会 ©2011-2020 版权所有

中国自动化学会 控制理论专业委员会
电话:86-10-82541403;Email:tcct@iss.ac.cn