0去购物车结算
购物车中还没有商品，赶紧选购吧！
当前位置: > 机器证明：公理集论及分析基础的形式化

相同语种的商品

销售排行榜

机器证明：公理集论及分析基础的形式化


联系编辑
 
标题：
 
内容：
 
联系方式：
 
  
机器证明：公理集论及分析基础的形式化
  • 书号：9787030832443
    作者：郁文生等
  • 外文书名：
  • 装帧：平装
    开本：B5
  • 页数：394
    字数：522000
    语种：zh-Hans
  • 出版社：科学出版社
    出版时间：2025-09-01
  • 所属分类：
  • 定价： ￥198.00元
    售价： ￥156.42元
  • 图书介质:
    纸质书

  • 购买数量： 件  可供
  • 商品总价：

相同系列
全选

内容介绍

样章试读

用户评论

全部咨询

布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础。利用计算机证明辅助工具，可以完整构建这三大母结构的形式化系统。本书利用交互式定理证明工具Coq，实现Morse-Kelley公理化集合论形式化系统，可以迅速而自然地给出一个数学基础，摆脱了明显的悖论。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建。为方便应用，在Morse-Kelley公理化集合论形式化系统下，分别给出Landau的经典著作《分析基础》的形式化系统以及Zorich的著名著作《数学分析》中实数公理化的形式系统实现，从而迅速且自然地给出数学分析的坚实基础。
样章试读
  • 暂时还没有任何用户评论
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

全部咨询(共0条问答)

  • 暂时还没有任何用户咨询内容
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页
用户名： 匿名用户
E-mail：
咨询内容：

目录

  • 目录
    前言
    基本符号
    第1章 引言 1
    1.1 概述 1
    1.1.1 证明辅助工具 Coq 1
    1.1.2 形式化数学 2
    1.1.3 Morse-Kelley公理化集合论系统 3
    1.1.4 分析基础 5
    1.1.5 本书结构安排 7
    1.2 基本Coq指令清单及逻辑预备知识 8
    第2章 Morse-Kelley公理化集合论的形式化系统实现 14
    2.1 分类公理图式 14
    2.2 分类公理图式 (续) 15
    2.3 类的初等代数 16
    2.4 集的存在性 21
    2.5 序偶：关系 25
    2.6 函数 29
    2.7 良序 36
    2.8 序 43
    2.9 非负整数 51
    2.10 选择公理 54
    2.11 基数 57
    第3章 分析基础的形式化系统实现 80
    3.1 自然数 80
    3.1.1 公理 80
    3.1.2 加法 85
    3.1.3 序 90
    3.1.4 乘法 95
    3.2 分数 98
    3.2.1 定义和等价 98
    3.2.2 序 100
    3.2.3 加法 104
    3.2.4 乘法 109
    3.2.5 有理数和整数 113
    3.3 分割.133
    3.3.1 定义 133
    3.3.2 序 136
    3.3.3 加法 138
    3.3.4 乘法 145
    3.3.5 有理分割和整分割 153
    3.4 实数 165
    3.4.1 定义 165
    3.4.2 序 170
    3.4.3 加法 176
    3.4.4 乘法 196
    3.4.5 Dedekind基本定理 212
    3.5 复数.217
    3.5.1 定义 217
    3.5.2 加法 218
    3.5.3 乘法 220
    3.5.4 减法 222
    3.5.5 除法 223
    3.5.6 共轭复数 226
    3.5.7 绝对值 227
    3.5.8 和与积 229
    3.5.9 幂 241
    3.5.10 将实数编排在复数系统中 243
    第4章 实数集的公理系统形式化 247
    4.1 实数集的公理系统及其一般性质 247
    4.1.1 实数集的定义 247
    4.1.2 实数的某些一般的代数性质 250
    4.1.3 完备性公理与数集的确界存在性 259
    4.2 几个重要的实数子集262
    4.2.1 自然数与数学归纳法原理 262
    4.2.2 有理数与无理数 267
    4.2.3 Archimedes原理 280
    4.3 实数的几何解释 286
    4.4 实数模型的唯一性 291
    第5章 结论与注记.321
    附录一 Coq指令说明 327
    A.1 Coq专用术语327
    A.2 Coq证明指令328
    A.3 集成策略 331
    附录二 公理集论与实数公理化的结构性呈现 343
    参考文献 376
    索引 387
    后记 393
    表格目录
    表1.1 书中涉及的常用 Coq 指令简表9
    表1.2 书中涉及的常用 Coq 术语的基本含义 12
    表5.1 公理化集合论形式化系统代码量统计 321
    表5.2 分析基础形式化系统代码量统计 322
    表5.3 实数公理化形式系统代码量统计 322
    插图目录
    图1.1 Kelley的《一般拓扑学》英文版和中文版封面 4
    图1.2 Landau的《分析基础》德文、英文版和中文版封面 5
    图1.3 Zorich的《数学分析》俄文版、英文版、中文版封面 7
    图5.1 实数模型同构唯一性的证明截图323
    图5.2 计算机软件著作权登记证书 323
    图5.3 Lean 验证数学定理输出的命题和概念网络 325
帮助中心
公司简介
联系我们
常见问题
新手上路
发票制度
积分说明
购物指南
配送方式
配送时间及费用
配送查询说明
配送范围
快递查询
售后服务
退换货说明
退换货流程
投诉或建议
版权声明
经营资质
营业执照
出版社经营许可证

中国科技出版传媒股份有限公司　版权所有

本平台为互联网非涉密平台，严禁处理、传输国家秘密。

　

京ICP备14028887号-5　 京ICP证150976号 京公网安备 11010102004214号

北京东黄城根北街16号 邮编：100717 Email:webmaster@mail.sciencep.com