书馨卡帮你省薪 2024个人购书报告 2024中图网年度报告
好书大清仓|每满60减30，减后满百送文创
欢迎光临中图网 请 | 注册
搜索
搜索全部
  • 搜索全部
  • 书名
  • 作者
  • 出版社
  • ISBN
高级搜索
我身体里的人造星星乡间的日常情感勒索神秘的黑猫
  • 合成诗经
  • 新用户注册领10元
中图网
>
自然科学
>
数学
>
数学理论
分析基础机器证明系统
分享

分析基础机器证明系统

作者：郁文生//付尧顺//郭礼权
出版社：科学出版社出版时间：2022-01-01
开本： 16开 页数： 396
本类榜单：自然科学销量榜
中 图 价:¥142.6(7.2折) 定价  ¥198.0 登录后可看到会员价
加入购物车 收藏
运费6元，满39元免运费
?新疆、西藏除外
本类五星书更多>
中图价:¥142.6 加入购物车
洞明世事，从读书开始 淘书团

分析基础机器证明系统 版权信息

  • ISBN：9787030706713
  • 条形码：9787030706713 ; 978-7-03-070671-3
  • 装帧：一般胶版纸
  • 册数：暂无
  • 重量：暂无
  • 所属分类：
    自然科学
    >
    数学
    >
    数学理论

分析基础机器证明系统 内容简介

本书利用交互式定理证明工具Coq，在朴素集合论的基础上，从Peano五条公设出发，完整实现Landau有名的《分析基础》中实数理论的形式化系统，包括对该专著中全部5个公设、73条定义和301个定理的Coq描述，其中依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，从而迅速且自然地给出数学分析的坚实基础。在分析基础形式化系统下，给出Dedekind实数完备性定理与它的几个有名等价命题间等价性的机器证明，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，基于实数的完备性定理，作为应用，进一步给出闭区间上连续函数的重要性质——有界性定理、很值定理、介值定理、一致连续性定理——的机器证明。另外，还给出张景中院士提出的第三代微积分——不用极限的微积分——的形式化系统实现。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于数学分析相关理论的形式化构建。 本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材，也可供从事人工智能相关科研工作者参考。

分析基础机器证明系统 目录

目录
前言
致谢
符号汇集
第1章引言1
1.1概述1
1.1.1证明辅助工具Coq1
1.1.2形式化数学2
1.1.3分析基础3
1.1.4第三代微积分5
1.1.5本书结构安排7
1.2基本Coq指令清单及逻辑预备知识7
1.3集合与映射的一些基本概念13
第2章分析基础的形式化系统实现19
2.1自然数19
2.1.1公理19
2.1.2加法22
2.1.3序26
2.1.4乘法36
2.1.5补充材料:有限数的定义及性质40
2.2分数44
2.2.1定义和等价44
2.2.2序46
2.2.3加法51
2.2.4乘法56
2.2.5有理数和整数61
2.3分割83
2.3.1定义83
2.3.2序86
2.3.3加法89
2.3.4乘法97
2.3.5有理分割和整分割106
2.4实数118
2.4.1定义118
2.4.2序.119
2.4.3加法125
2.4.4乘法139
2.4.5Dedekind基本定理146
2.4.6补充材料:实数运算的一些性质151
2.4.7补充材料:实数序列的一些性质166
2.5复数175
2.5.1定义175
2.5.2加法177
2.5.3乘法181
2.5.4减法186
2.5.5除法188
2.5.6共轭复数193
2.5.7绝对值195
2.5.8和与积200
2.5.9幂237
2.5.10将实数编排在复数系统中245
第3章实数完备性等价命题的机器证明251
3.1确界存在定理251
3.1.1用Dedekind基本定理证明确界存在定理251
3.1.2用确界存在定理证明Dedekind基本定理254
3.2单调有界定理255
3.3闭区间套定理256
3.4有限覆盖定理258
3.5聚点原理264
3.6列紧性定理268
3.7Cauchy收敛准则272
3.8用Cauchy收敛准则证明Dedekind基本定理275
第4章闭区间上连续函数性质的机器证明283
4.1基本定义283
4.2有界性定理290
4.3*值定理293
4.4介值定理295
4.5一致连续性定理300
第5章第三代微积分的形式化实现306
5.1预备知识307
5.1.1基本定义307
5.1.2一些引理308
5.2导数和定积分的初等定义315
5.3积分与微分的新视角324
5.4微积分系统的基本定理346
第6章总结与注记370
参考文献375
附录Coq指令说明386
A.1Coq专用术语386
A.2Coq证明指令387
A.3集成策略390
索引393
表索引
表1.1书中涉及常用Coq指令简表8
表1.2书中涉及常用Coq术语的基本含义13
表6.1分析基础形式化系统代码量统计370
表6.2实数完备性及其等价命题形式系统化代码量统计371
表6.3闭区间上连续函数性质形式化系统代码量统计371
表6.4第三代微积分形式化系统代码量统计371
图索引
图1.1Landau《分析基础》的德文-英文版和中文版封面4
图3.1实数完备性定理的等价性251
图3.2实数的定义与完备性总览图282
图6.1Dedekind基本定理的证明截图372
图6.2计算机软件著作权登记证书373
展开全部

分析基础机器证明系统 节选

第1章　引言 人工智能研究是当前科技发展的热点和前沿方向，夯实人工智能基础理论尤为重要，数学定理机器证明是人工智能基础理论的深刻体现，参见文献[4-6，9，10，13，16，26，59，67-69，78-80，87，134，139，175，180，184186，189，198，201，220]. 1.1　概述 1.1.1　证明辅助工具Coq 数学定理的计算机形式化证明，近年来随着计算机科学的迅猛发展，特别是证明辅助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]的出现，取得了长足的进展[10，67-69，78-80，87，99，201].Coq是一个交互式定理证明与程序开发系统平台，是一个用于描述定理内容、验证定理证明的计算机工具.这些定理可能涉及普通数学、证明理论或程序验证等[14，35，105，148]多个方面.在推理和编程方面，Coq都拥有足够强大的表达能力，从构造简单的项、执行简单的证明，直至建立完整的理论、学习复杂的算法等，对学习者的能力有着不同层次的要求[14，35，105，148]. Coq是一个交互式的编译环境[14，35，105，148]，用户以人机对话的方式一问一答，用户可以边设计、边修改，使证明中的错误及时得到补证.Coq系统的基本原理是归纳构造演算[14，35，105，148]，是一个形式化系统.Coq支持自动推理程序.Coq通过命令式程序进行逻辑推导，可以利用已证命题进行自动推理.Coq中的归纳类型扩展了传统程序设计语言中有关类型定义的概念，类似于大多数函数式程序设计语言中的递归类型定义[14，35，105，148].Coq有一支强大的全职研发队伍，支持开源.前，Coq已成为数学定理证明与计算逻辑领域的一个重要工具[7，9，30，148，180].2005年，国际著名计算机专家Gonthier和Werner成功基于Coq给出了著名的“四色定理”的计算机证明[67]，进而，Gonthier等又经过六年努力，于2012年完成对“有限单群分类定理”的机器验证(该证明过程约有4300个定义和15000条定理，约170000行Coq代码)[10，68，69]，使得证明辅助工具Coq在学术界得到广泛认可.2015年，Hales等又HOLLight和Isabelle/HOL[71，145]上完成了对“Kepler猜想”的机器验证[87]，Wiedijk在文章[183]中指出，全球各相关研究团队已经或计划完成包括G.del**不完备性定理、Jordan曲线定理、素数定理以及Fermat大定理等在内的100个著名数学定理的计算机形式化证明.这些成果使得证明辅助工具Coq、Isabelle及HOL等[14，35，71，86，92，105，145，148，183]在学术界的影响日益增强 1.1.2形式化数学 形式化数学在20世纪初对于数学基础的深入讨论中受到重视，对整个20世纪数学的发展产生了深远的影响，参见文[2，18，23，39，46，54-56，73，75-77，85，94，95，97，106，109，111，113，115，117，143，159，166，170，173，179，201，209，213]，虽然有时也饱受过于“形式”的诟病[46，85，111，115，153，167]，但20世纪90年代，特别是进入21世纪以来，随着计算机形式化工具的出现，尤其是上述一系列著名数学难题形式化证明的实现，使得形式化数学与形式化证明辅助工具的结合在学术界得到极大重视. 著名数学家和计算机专家Wiedijk认为当前正在进行的形式化数学是一次数学革命，他在文章[183]中指出，“数学历史上发生过三次革命.**次是公元前3世纪，古希腊数学家Euclid在《几何原本》引入数学证明方法;第二次是19世纪Cauchy等引入‘严格’数学方法，以及后来的数理逻辑和集合论;第三次就是当前正在进行的形式化数学”[26，183].2002年菲尔兹奖获得者Gowers[72]和Voevodsky[169]、2010年菲尔兹奖获得者Villani[168]以及1987年沃尔夫奖和2005年阿贝尔奖获得者Lax都大力倡导发展可信数学[98].Gowers在文章[72]中指出，“21世纪计算机在证明定理的过程中会起到巨大作用，理论数学研究的模式将会彻底改观，计算机的作用有可能超出我们现在的想象”，甚至预测[72，129]“2099年之前，计算机或可完成所有重要的数学.计算机会提出猜想、找到证明.而数学家的工作，是试着去理解和运用其中的一些结果”.Lax认为“(高速计算机)对于应用数学和纯粹数学的影响可以与望远镜对天文学和显微镜对生物学的影响相比拟”[98]. 当今数学论证变得如此复杂，而计算机软件能够检查卷帙浩繁的数学证明正确性，人类的大脑无法跟上数学不断增长的复杂性，计算机检验将是唯一的解决方案[168，169].今后，每一本严谨的数学专著，甚至每一篇数学论文，都可由计算机检验其细节的正确性，这正发展为一种趋势.英国帝国理工学院的数学教授Buzzard在剑桥举办的一次研讨会上表示:证明是一种很高的标准，我们不需要数学家像机器一样工作，而是可以要他们去使用机器à！关于数学定理的形式化证明，必然涉及国际著名的布尔巴基(Bourbaki)学派[18-21].布尔巴基是一群以法国人为主的数学家的共同名字，他们的思想对于20世纪中叶以来的数学发展具有深刻影响[111，115，173].该学派提出数学结构的概念，并用此概念统一现代数学[18，111，115，173].按照布尔巴基学派的观点，数学中有三大母结构，即序结构[21]、代数结构[19]和拓扑结构[20].基于这三种结构相互交融形成了现代数学的主体内容.利用交互式定理证明工具Coq，可以完整构建这三大母结构的机器证明系统，在此方面国内外都开始进行了一些有益的研究工作[9，11，47，57，78-80，83，84，99，130，160-164，180，188，201，203，207]. 1.1.3分析基础 数学史上*使人惊奇的事实之一，是实数系的逻辑基础竟迟至19世纪后叶才建立起来的[115].而自然数理论公理体系的建立更是基于Dedekind总结出的五条基本性质[95，173]，以Peano[113]发表于1889年的《算术原理——用一种新方法展现》为标志. 经历无数失败和挫折之后，为分析数学寻找基础的工作逐渐有了眉目，这个过程就是19世纪分析算术化的实现，于19世纪末期完成，大体包括三个阶段，见文献[2，54，74-77，85，97，106，111，113，115，173]:**阶段——极限论建立，主要以法国数学家Cauchy与德国数学家Weierstrass的工作为标志;第二阶段——实数理论建立，主要以德国数学家Dedekind、Cantor与Weierstrass等的实数构造理论为标志;第三阶段——算术化过程完成，以德国数学家Dedekind与意大利数学家、逻辑学家Peano的自然数理论为标志[173].可以看到，分析算术化的过程与克服数学史著名的三次危机，即无理数的发现、分析的严密化、集合论中悖论的消解[179]，是密切相关的[115]. 德国著名数学家Landau发表于1929年的《分析基础:整数、有理数、无理数和复数的运算(微积分补充教材)》[117](简称《分析基础》)，从Peano五条公设[113]出发，依次构造了自然数、分数、分割、实数和复数，并建立了Dedekind实数完备性定理，即Dedekind基本定理，从而迅速且自然地给出数学分析的坚实基础[117]. Landau的名著在世界范围内影响了几代数学家，德文本即出版有四个版次，英文翻译本也至少出版有三个版次[117].在我国，1958年高等教育出版社曾出版有刘绂堂先生翻译的中文版[117].图1.1是Landau《分析基础》的德文-英文版和中文版封面.老一辈数学家丁石孙[211]、严士健[196]、张恭庆[211]等都深受此书影响，并推荐学生研读.Landau的名著[117]问世以来，又有多部论述实数理论的专著，例如[49，142，159，177]，相继出版. 众所周知，Dedekind基本定理与实数完备性的几个著名命题等价，这些命题包括确界存在定理、单调有界定理、Cauchy-Cantor闭区间套定理、Heine-Borel-Lebesgue有限覆盖定理、Bolzano-Weierstrass聚点原理、Bolzano-Weierstrass列紧性定理及Bolzano-Cauchy收敛准则等，而闭区间上连续函数的重要性质——有界性定理、*值定理、介值定理、一致连续性定理——本质上也依赖于实数完备性理论.实数完备性各命题间等价性及闭区间上连续函数性质的人工证明散见于国内外“数学分析”的标准教材，参见文献[1，3，24，25，27，28，36，42，43，48，50，51，58，64，66，89，100-103，107，119，120，131，149，150，152，165，178，187，191，194，211，223，225-228].实数完备性是极限论的基础，上述内容一直是数学分析的重点和难点.近年来仍有人在各类期刊上讨论有关实数完备性定理的证明，特别指出，广州大学袁文俊教授在文献[204，205]中，从上述八大实数完备性定理中的任何一个定理出发，放射性地推出其他七个定理，系统总结了八大实数完备性定理的相互等价性. 图1.1Landau《分析基础》的德文-英文版和中文版封面 20世纪70年代，vanBenthemJutting[13]基于Automath软件平台[22，41，144，182]完成Landau《分析基础》[117]的全部形式化实现.这是数学理论计算机形式化领域里程碑式的工作，影响深远. Automath[13，22，41，144，182]是为实现数学的表示，1970年由荷兰Eindhoven大学deBrujin教授设计的基于λ类型[135，136]理论的数学定理证明器，与基于归纳构造演算的现代类型理论[9，14，30，35，105，148，180]存在较大差异.基于Automath[22，41，144，182]完成的Landau《分析基础》[117]形式化代码[13]，目前看来，在可读性方面也不能令人满意[182]. 2011年，德国Saarland大学著名教授Brown[22]提出，将vanBenthemJutting[13]基于Automath[22，41，144，182]完成的Landau《分析基础》[117]形式化代码用计算机忠实“翻译”成Coq代码的构想，这项“翻译”主要是针对Landau《分析基础》中公理、定义和定理的形式化描述而言的，针对定理机器证明代码的“翻译”难度较大，尚未见报道，相关的研究似仍在进行中.2011年，Smolka和Brown指导的学生Hornung[99]还给出了基于Coq的Landau《分析基础》[117]前四章形式化代码的一个版本.早期关于实数理论形式化的工作还包括:Chirimar和Howe[31]基于Nuprl[33]利用Cauchy序列定义实数，Harrison[90，91]基于Isabelle/HOL[71，145]对实数的构造，Ciaffaglione和DiGianantonio[32]基于Coq直接用无穷序列表达实数，以及Geuvers和Niqui[60]基于Coq利用Cauchy完备性构造实数等. 1.1.4第三代微积分 微积分是数学史上*伟大的成就之一，开启了近代科技的新纪元，对物理学、天文学等其他学科的发展也起到了重要的促进作用.微积分的创立距今已有三百多年的历史[111，115，12

商品评论(0条)
写书评 赚书币
暂无评论……
书友推荐
本类畅销
编辑推荐
返回顶部
新手上路
新用户指引
注册用户 更改注册信息
购物常见问题
关于特价书的常见问题
购买问题
订单跟踪
付款方式
账户余额  申请提现
配送方式及费用、范围
集团购买
售后服务
退换货流程
投诉与建议
特色服务
会员等级与书币
中图网书馨卡
邀请好友购买返10元礼包
其他信息
本站简介
联系我们
招聘英才
网站联盟
友情链接
微信公众号
中图网微信
中图网微博
中图网微博
手机中图网
手机中图网
中图网
诚信认证 电子商务诚信单位认证

京ICP备09013606号-3京信市监发[2002]122号海淀公安分局备案编号：1101083394

营业执照出版物经营许可证 京出发京批字第直110071

在线客服