計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)
定 價(jià):99 元
叢書(shū)名:計(jì)算機(jī)科學(xué)叢書(shū)
- 作者:[美] 雷克斯·佩奇(Rex Page) 著,汪榮貴,陳朗,汪雄飛 譯
- 出版時(shí)間:2021/6/1
- ISBN:9787111682226
- 出 版 社:機(jī)械工業(yè)出版社
- 中圖法分類:TP302.2
- 頁(yè)碼:222
- 紙張:膠版紙
- 版次:1
- 開(kāi)本:16開(kāi)
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》以實(shí)際問(wèn)題的求解為導(dǎo)向,對(duì)計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)知識(shí)進(jìn)行了介紹、討論和歸納,實(shí)現(xiàn)了邏輯與計(jì)算機(jī)之間的知識(shí)貫通。
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》主要內(nèi)容包括邏輯與等式、計(jì)算機(jī)算術(shù)、算法、計(jì)算實(shí)踐四個(gè)部分,采用三種形式化表示法,即傳統(tǒng)的邏輯代數(shù)公式表示法、數(shù)字電路圖表示法以及ACL2表示法實(shí)現(xiàn)邏輯推理。
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》不僅可以作為高等學(xué)校計(jì)算機(jī)、人工智能、大數(shù)據(jù)及相關(guān)專業(yè)的邏輯課程教材,也可供廣大計(jì)算機(jī)愛(ài)好者、計(jì)算機(jī)及相關(guān)領(lǐng)域的科研人員和工程技術(shù)人員自學(xué)參考。
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》以實(shí)際問(wèn)題的求解為導(dǎo)向,對(duì)計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)知識(shí)進(jìn)行了介紹、討論和歸納,完美地實(shí)現(xiàn)了邏輯與計(jì)算機(jī)之間的知識(shí)貫通。
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》主要內(nèi)容包括邏輯與等式、計(jì)算機(jī)算術(shù)、算法、計(jì)算實(shí)踐四個(gè)部分,采用三種形式化表示法,即傳統(tǒng)的邏輯代數(shù)公式表示法、數(shù)字電路圖表示法以及ACL2表示法實(shí)現(xiàn)邏輯推理。
《計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)》特色:
知識(shí)體系的組織結(jié)構(gòu)突破了傳統(tǒng)的數(shù)學(xué)框架,直接面向與計(jì)算機(jī)科學(xué)相關(guān)的邏輯主題,將邏輯用于解決計(jì)算機(jī)科學(xué)領(lǐng)域的重要問(wèn)題。
結(jié)合生動(dòng)有趣的具體應(yīng)用實(shí)例介紹邏輯知識(shí)和證明方法,能夠有效地激發(fā)讀者的學(xué)習(xí)興趣,特別有助于培養(yǎng)讀者的邏輯思維和數(shù)學(xué)思維。
采用三種形式化表示方法實(shí)現(xiàn)邏輯推理并將ACL2作為邏輯證明引擎,通過(guò)實(shí)際應(yīng)用效果生動(dòng)地驗(yàn)證了軟件和硬件工程師均可以從邏輯(包括機(jī)械化邏輯)的學(xué)習(xí)中獲益。
作為思維的基本形式和基本規(guī)則,邏輯構(gòu)成了人類思維和機(jī)器思維的共同基礎(chǔ),也是計(jì)算機(jī)科學(xué)與信息科學(xué)的理論基礎(chǔ)。事實(shí)上,無(wú)論是計(jì)算機(jī)硬件還是計(jì)算機(jī)軟件,它們都是一組邏輯組件的某種特定表現(xiàn)形式。具備嚴(yán)謹(jǐn)?shù)倪壿嬎季S能力對(duì)于計(jì)算機(jī)系統(tǒng)研發(fā)人員的重要性是毋庸置疑的。然而,邏輯思維能力的培養(yǎng)并不是一件很容易的事情,通常需要經(jīng)歷一定的理論學(xué)習(xí)和實(shí)際訓(xùn)練。目前,計(jì)算機(jī)專業(yè)的學(xué)生主要是通過(guò)離散數(shù)學(xué)等數(shù)學(xué)課程進(jìn)行形式邏輯方面的學(xué)習(xí),而不是直接面向計(jì)算機(jī)專業(yè)內(nèi)容討論計(jì)算機(jī)科學(xué)的基本邏輯,這使得學(xué)生接觸到的邏輯知識(shí)與計(jì)算機(jī)科學(xué)的關(guān)系較為松散,不利于邏輯與計(jì)算機(jī)之間的知識(shí)貫通。本書(shū)可以很好地彌補(bǔ)這方面的不足。它以實(shí)際問(wèn)題的求解為導(dǎo)向,對(duì)計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)知識(shí)進(jìn)行了比較系統(tǒng)的介紹、討論和歸納,較好地實(shí)現(xiàn)了邏輯與計(jì)算機(jī)之間的知識(shí)貫通,可以有效地培育和提升讀者的邏輯思維能力,使其能夠在計(jì)算機(jī)邏輯方面獲得比較系統(tǒng)的專業(yè)訓(xùn)練,從而能夠更加高效地從事計(jì)算機(jī)軟硬件產(chǎn)品的研發(fā)工作。本書(shū)的基本特點(diǎn)主要表現(xiàn)在如下三個(gè)方面:
第一,知識(shí)體系的組織結(jié)構(gòu)突破了傳統(tǒng)的數(shù)學(xué)框架,內(nèi)容主要包括邏輯與等式、計(jì)算機(jī)算術(shù)、算法、計(jì)算實(shí)踐四個(gè)部分,直接關(guān)注與計(jì)算機(jī)科學(xué)相關(guān)的邏輯主題,將邏輯用于解決計(jì)算機(jī)科學(xué)領(lǐng)域的問(wèn)題,包括硬件組件、軟件組件、測(cè)試和驗(yàn)證以及算法分析,邏輯知識(shí)與計(jì)算機(jī)知識(shí)的聯(lián)系更加緊密,實(shí)現(xiàn)了兩者的深度融合,特別適合用來(lái)對(duì)計(jì)算機(jī)專業(yè)人員進(jìn)行系統(tǒng)性的邏輯訓(xùn)練。
第二,在可讀性方面做了很好的設(shè)計(jì),主要通過(guò)一些生動(dòng)有趣的具體應(yīng)用實(shí)例介紹邏輯知識(shí)和證明方法,能夠有效地激發(fā)讀者的學(xué)習(xí)興趣,培養(yǎng)讀者的邏輯思維和數(shù)學(xué)思維能力。例如,通過(guò)石頭、剪刀、布這個(gè)簡(jiǎn)單的游戲深入淺出地闡述程序的基本結(jié)構(gòu)和基于等式的程序模型,生動(dòng)地解釋了在基于等式的模型中,程序?yàn)楹瓮耆苫诓僮鲾?shù)的數(shù)學(xué)函數(shù)組成,為何可以使用經(jīng)典邏輯和傳統(tǒng)代數(shù)公式來(lái)理解基于等式的程序。通過(guò)介紹深藍(lán)計(jì)算機(jī)系統(tǒng)的基本工作原理來(lái)介紹歸納定義,使得讀者能夠清楚地認(rèn)識(shí)到,對(duì)于計(jì)算機(jī)系統(tǒng)和邏輯系統(tǒng)而言,再?gòu)?fù)雜的行為通常也是從最初簡(jiǎn)單的行為演變而來(lái),再?gòu)?fù)雜的理論通常也是建立在一些簡(jiǎn)單的基本原則基礎(chǔ)之上。
第三,采用三種形式化表示法,即傳統(tǒng)的邏輯代數(shù)公式表示法、數(shù)字電路圖表示法以及ACL2表示法,使得學(xué)生可以借助軟件工具比較容易地學(xué)習(xí)機(jī)械化邏輯的相關(guān)知識(shí)。本書(shū)使用ACL2作為邏輯證明引擎,ACL2提供了比任何其他工具更容易理解的機(jī)械化邏輯證明形式,通過(guò)事實(shí)生動(dòng)地說(shuō)明軟件和硬件工程師可以如何從邏輯(包括機(jī)械化邏輯)中受益。當(dāng)讀者在檢查證據(jù)和處理證明細(xì)節(jié)的很多方面得到ACL2軟件工具的有效支持時(shí),會(huì)非常開(kāi)心并且更有學(xué)習(xí)動(dòng)力。
雷克斯·佩奇(Rex Page),美國(guó)俄克拉荷馬大學(xué)計(jì)算機(jī)科學(xué)學(xué)院榮休教授,專注于設(shè)計(jì)和開(kāi)發(fā)可靠的數(shù)字電路和軟件的方法,在學(xué)術(shù)界和工業(yè)界從事可靠軟件領(lǐng)域的研發(fā)工作已有40年。他于斯坦福大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位,加州大學(xué)圣地亞哥分校獲得數(shù)學(xué)博士學(xué)位。在加入俄克拉荷馬大學(xué)之前,曾先后在科羅拉多州立大學(xué)和美國(guó)石油公司從事教學(xué)和研究工作。他的早期工作為大規(guī)模并行計(jì)算系統(tǒng)開(kāi)發(fā)了有效的軟件工程方法,在教學(xué)生涯中提倡在計(jì)算機(jī)科學(xué)和軟件工程的學(xué)士學(xué)位課程中加強(qiáng)應(yīng)用邏輯的教育。
魯本·岡博亞(Ruben Gamboa),懷俄明大學(xué)工程與應(yīng)用科學(xué)學(xué)院計(jì)算機(jī)科學(xué)系教授,主要研究基于半自動(dòng)化證明引擎ACL2的自動(dòng)定理證明。除此之外,他的研究興趣還包括NoSQL數(shù)據(jù)庫(kù)、近似算法、云計(jì)算的應(yīng)用、計(jì)算機(jī)圖形學(xué)等。他于得克薩斯農(nóng)工大學(xué)獲得碩士學(xué)位,得克薩斯大學(xué)奧斯汀分校獲得博士學(xué)位。他多次在ACL2Workshop中發(fā)表研究論文,并曾連續(xù)兩年任職于ACL2指導(dǎo)委員會(huì)。
出版者的話
譯者序
前言
第一部分 邏輯與等式
第1章 計(jì)算機(jī)系統(tǒng):原理簡(jiǎn)單,行為復(fù)雜
1.1 硬件與軟件
1.2 程序的結(jié)構(gòu)
1.3 深藍(lán)與歸納定義
習(xí)題
第2章 布爾公式和等式
2.1 利用等式推理
習(xí)題
2.2 布爾等式
習(xí)題
2.3 布爾公式
習(xí)題
2.4 數(shù)字電路
習(xí)題
2.5 演繹推理
習(xí)題
2.6 謂詞和量詞
習(xí)題
2.7 量化謂詞的推理
習(xí)題
2.8 布爾模型
習(xí)題
2.9 謂詞和量詞的一般模型
第3章 軟件測(cè)試和前綴法
習(xí)題
第4章 數(shù)學(xué)歸納
4.1 數(shù)學(xué)對(duì)象列表
習(xí)題
4.2 數(shù)學(xué)歸納法
習(xí)題
4.3 Defun:ACL2中運(yùn)算符的定義
4.4 連接、前綴和后綴
習(xí)題
第5章 機(jī)械化邏輯
5.1 ACL2定理與證明
5.2 使用已證的定理庫(kù)
習(xí)題
5.3 約束定理
習(xí)題
5.4 輔助機(jī)械化邏輯工作
習(xí)題
5.5 自動(dòng)化證明及其做不到的事
習(xí)題
第二部分 計(jì)算機(jī)算術(shù)
第6章 二進(jìn)制數(shù)字
6.1 數(shù)和數(shù)字
習(xí)題
6.2 從數(shù)字到數(shù)
習(xí)題
6.3 二進(jìn)制數(shù)字
習(xí)題
第7章 加法器
7.1 數(shù)字相加
習(xí)題
7.2 一位二進(jìn)制數(shù)字加法電路
7.3 兩位二進(jìn)制數(shù)字加法電路
習(xí)題
7.4 w位二進(jìn)制數(shù)字加法
習(xí)題
7.5 負(fù)數(shù)的數(shù)字
習(xí)題
第8章 乘法器和大數(shù)算法
8.1 大數(shù)加法器
習(xí)題
8.2 移位相加乘法器
習(xí)題
第三部分 算法
第9章 多路復(fù)用器和解復(fù)用器
9.1 多路復(fù)用器
習(xí)題
9.2 解復(fù)用器
習(xí)題
第10章 排序
10.1 插入排序
習(xí)題
10.2 保序合并
習(xí)題
10.3 歸并排序
習(xí)題
10.4 排序算法分析
10.4.1 計(jì)算步驟的計(jì)數(shù)
習(xí)題
10.4.2 計(jì)算解復(fù)用的步數(shù)
習(xí)題
10.4.3 計(jì)算歸并的步數(shù)
習(xí)題
10.4.4 計(jì)算歸并排序的步數(shù)
習(xí)題
10.4.5 計(jì)算插入排序的步數(shù)
習(xí)題
第11章 搜索樹(shù)
11.1 查找事物
11.2 平衡二叉樹(shù)
11.3 搜索樹(shù)的表示
11.4 有序搜索樹(shù)
習(xí)題
11.5 平衡搜索樹(shù)
習(xí)題
11.6 搜索樹(shù)中插入新項(xiàng)目
習(xí)題
11.7 順序插入
習(xí)題
11.8 雙旋轉(zhuǎn)
習(xí)題
11.9 快速插入
習(xí)題
第12章 哈希表
12.1 列表和數(shù)組
12.2 哈希運(yùn)算符
習(xí)題
12.3 一些應(yīng)用
……
第四部分 計(jì)算實(shí)踐
索引