中圖網小程序
一鍵登錄
更方便
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
自然數的緊化延伸機器證明系統 版權信息
- 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）。
書友推薦
- >
推拿
- >
李白與唐代文化
- >
姑媽的寶刀
- >
【精裝繪本】畫給孩子的中國神話
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語)
- >
上帝之肋:男人的真實旅程
- >
莉莉和章魚
- >
中國歷史的瞬間
本類暢銷
