掃一掃
關(guān)注中圖網(wǎng)
官方微博
包郵 自然數(shù)的緊化延伸機(jī)器證明系統(tǒng)
作者：郁文生
開(kāi)本：
B5
頁(yè)數(shù)：
602
本類(lèi)榜單：計(jì)算機(jī)/網(wǎng)絡(luò)銷(xiāo)量榜
本類(lèi)五星書(shū)更多>
-
>
全國(guó)計(jì)算機(jī)等級(jí)考試最新真考題庫(kù)模擬考場(chǎng)及詳解·二級(jí)MSOffice高級(jí)應(yīng)用
-
>
決戰(zhàn)行測(cè)5000題(言語(yǔ)理解與表達(dá))
-
>
軟件性能測(cè)試.分析與調(diào)優(yōu)實(shí)踐之路
-
>
第一行代碼Android
-
>
JAVA持續(xù)交付
-
>
EXCEL最強(qiáng)教科書(shū)(完全版)(全彩印刷)
-
>
深度學(xué)習(xí)
中圖價(jià):¥207.4
加入購(gòu)物車(chē)
自然數(shù)的緊化延伸機(jī)器證明系統(tǒng) 版權(quán)信息
- ISBN：9787030775450
- 條形碼：9787030775450 ; 978-7-03-077545-0
- 裝幀：精裝
- 冊(cè)數(shù)：暫無(wú)
- 重量：暫無(wú)
- 所屬分類(lèi)：>
自然數(shù)的緊化延伸機(jī)器證明系統(tǒng) 內(nèi)容簡(jiǎn)介
數(shù)系的擴(kuò)充始終貫穿于數(shù)學(xué)理論的發(fā)展之中.本書(shū)利用交互式定理證明工具Coq, 在Morse-Kelley 公理化集合論形式化系統(tǒng)下,給出中國(guó)科學(xué)與技術(shù)大學(xué)汪芳庭教授在其《數(shù)學(xué)基礎(chǔ)》中采用算術(shù)超濾分?jǐn)?shù)構(gòu)造實(shí)數(shù)的機(jī)器證明系統(tǒng), 包括超濾空間與算術(shù)超濾的基本概念、超濾變換以及用算術(shù)超濾構(gòu)造算術(shù)模型的形式化實(shí)現(xiàn), 構(gòu)建了非標(biāo)準(zhǔn)實(shí)數(shù)模型, 自然包含標(biāo)準(zhǔn)實(shí)數(shù)模型, 并且給出濾子擴(kuò)張?jiān)瓌t和連續(xù)統(tǒng)假設(shè)蘊(yùn)含非主算術(shù)超濾存在的形式化驗(yàn)證. 在我們開(kāi)發(fā)的系統(tǒng)中,全部定理無(wú)例外地給出Coq的機(jī)器證明代碼, 所有形式化過(guò)程已被Coq驗(yàn)證, 并在計(jì)算機(jī)上運(yùn)行通過(guò), 充分體現(xiàn)了基于Coq 的數(shù)學(xué)定理機(jī)器證明具有可讀性、交互性和智能性的特點(diǎn), 其證明過(guò)程規(guī)范、嚴(yán)謹(jǐn)、可靠. 該系統(tǒng)可方便地應(yīng)用于非標(biāo)準(zhǔn)分析理論的形式化構(gòu)建.本書(shū)可作為數(shù)學(xué)與計(jì)算機(jī)科學(xué)、信息科學(xué)相關(guān)專業(yè)的高年級(jí)本科生或研究生教材, 也可供從事人工智能相關(guān)科研工作者學(xué)習(xí)參考.
自然數(shù)的緊化延伸機(jī)器證明系統(tǒng) 目錄
“數(shù)學(xué)機(jī)械化叢書(shū)”前言
前言
基本符號(hào)
第1章 引言
1.1 概述
1.1.1 證明輔助工具Coq
1.1.2 形式化數(shù)學(xué)
1.1.3 Morse-Kelley公理化集合論系統(tǒng)
1.1.4 關(guān)于數(shù)系的擴(kuò)充
1.1.5 本書(shū)結(jié)構(gòu)安排
1.2 基本Coq指令清單及邏輯預(yù)備知識(shí)
第2章 Morse-Kelley公理化集合論的形式化系統(tǒng)實(shí)現(xiàn)
2.1 分類(lèi)公理圖式
2.2 分類(lèi)公理圖式（續(xù)）
2.3 類(lèi)的初等代數(shù)
2.4 集的存在性
2.5 序偶：關(guān)系
2.6 函數(shù)
2.7 良序
2.8 序
2.9 非負(fù)整數(shù)
2.10 選擇公理
2.11 基數(shù)
第3章 濾子構(gòu)造超有理數(shù)的形式化系統(tǒng)實(shí)現(xiàn)
3.1 Peano算術(shù)的適當(dāng)展開(kāi)
3.1.1 加法和乘法
3.1.2 代數(shù)運(yùn)算性質(zhì)
3.1.3 偶數(shù)和奇數(shù)
3.2 濾子與超濾
3.3 超濾變換
3.4 算術(shù)超濾及其算術(shù)模型
3.4.1 算術(shù)超濾
3.4.2 *N上的序
3.4.3 *N上的運(yùn)算
3.4.4 ω嵌入*N
3.5 *N擴(kuò)張到*Z
3.5.1 等價(jià)關(guān)系與分類(lèi)
3.5.2 *N×*N的一個(gè)重要分類(lèi)
3.5.3 *Z上的序
3.5.4 *Z上的運(yùn)算
3.5.5 *N嵌入*Z
3.6 *Z擴(kuò)張到*Q
3.6.1 *Z×（*Z～{*Z0
展開(kāi)全部
自然數(shù)的緊化延伸機(jī)器證明系統(tǒng) 作者簡(jiǎn)介
第三屆楊嘉墀科技獎(jiǎng)（2013），吳文俊人工智能科學(xué)技術(shù)獎(jiǎng)自然科學(xué)獎(jiǎng)（2017）。
書(shū)友推薦
- >
莉莉和章魚(yú)
- >
上帝之肋:男人的真實(shí)旅程
- >
回憶愛(ài)瑪儂
- >
史學(xué)評(píng)論
- >
苦雨齋序跋文-周作人自編集
- >
企鵝口袋書(shū)系列·偉大的思想20:論自然選擇(英漢雙語(yǔ))
- >
月亮虎
- >
中國(guó)人在烏蘇里邊疆區(qū):歷史與人類(lèi)學(xué)概述
本類(lèi)暢銷(xiāo)
