图书信息: 丛 书 名:数学机械化丛书 |
|
作者简介: 郁文生,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 的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建。 目录: |
控制理论专业委员会 ©2011-2020 版权所有 | |