扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
深度学习
-
>
Unreal Engine 4蓝图完全学习教程
-
>
深入理解计算机系统-原书第3版
-
>
Word/Excel PPT 2013办公应用从入门到精通-(附赠1DVD.含语音视频教学+办公模板+PDF电子书)
自然数的紧化延伸机器证明系统 版权信息
- ISBN：9787030775450
- 条形码：9787030775450 ; 978-7-03-077545-0
- 装帧：精装
- 册数：暂无
- 重量：暂无
- 所属分类：>
自然数的紧化延伸机器证明系统 内容简介
数系的扩充始终贯穿于数学理论的发展之中.本书利用交互式定理证明工具Coq, 在Morse-Kelley 公理化集合论形式化系统下,给出中国科学与技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统, 包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现, 构建了非标准实数模型, 自然包含标准实数模型, 并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证. 在我们开发的系统中,全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过, 充分体现了基于Coq 的数学定理机器证明具有可读性、交互性和智能性的特点, 其证明过程规范、严谨、可靠. 该系统可方便地应用于非标准分析理论的形式化构建.本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教材, 也可供从事人工智能相关科研工作者学习参考.
自然数的紧化延伸机器证明系统 目录
“数学机械化丛书”前言
前言
基本符号
第1章 引言
1.1 概述
1.1.1 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 Morse-Kelley公理化集合论系统
1.1.4 关于数系的扩充
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
第2章 Morse-Kelley公理化集合论的形式化系统实现
2.1 分类公理图式
2.2 分类公理图式（续）
2.3 类的初等代数
2.4 集的存在性
2.5 序偶：关系
2.6 函数
2.7 良序
2.8 序
2.9 非负整数
2.10 选择公理
2.11 基数
第3章 滤子构造超有理数的形式化系统实现
3.1 Peano算术的适当展开
3.1.1 加法和乘法
3.1.2 代数运算性质
3.1.3 偶数和奇数
3.2 滤子与超滤
3.3 超滤变换
3.4 算术超滤及其算术模型
3.4.1 算术超滤
3.4.2 *N上的序
3.4.3 *N上的运算
3.4.4 ω嵌入*N
3.5 *N扩张到*Z
3.5.1 等价关系与分类
3.5.2 *N×*N的一个重要分类
3.5.3 *Z上的序
3.5.4 *Z上的运算
3.5.5 *N嵌入*Z
3.6 *Z扩张到*Q
3.6.1 *Z×（*Z～{*Z0
展开全部
自然数的紧化延伸机器证明系统 作者简介
第三届杨嘉墀科技奖（2013），吴文俊人工智能科学技术奖自然科学奖（2017）。
书友推荐
- >
【精装绘本】画给孩子的中国神话
【精装绘本】画给孩子的中国神话
¥17.6¥55.0 - >
小考拉的故事-套装共3册
小考拉的故事-套装共3册
¥36.7¥68.0 - >
巴金－再思录
巴金－再思录
¥14.7¥46.0 - >
唐代进士录
唐代进士录
¥15.1¥39.8 - >
随园食单
随园食单
¥15.4¥48.0 - >
月亮虎
月亮虎
¥14.4¥48.0 - >
李白与唐代文化
李白与唐代文化
¥8.9¥29.8 - >
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
¥6.3¥14.0
本类畅销
-
”互联网+“时代计算机算法的应用及其实践研究
¥19.9¥59 -
微服务设计
¥52.8¥69 -
图说深度学习:用可视化方法理解复杂概念
¥109¥188 -
计算机基础
¥17.2¥31 -
改变未来的九大算法
¥50¥68 -
生成式AI入门与AWS实战
¥77.8¥99.8
