計算機科學的邏輯基礎 Essential Logic for Computer Science

本書以實際問題的求解為導向，對計算機科學的邏輯基礎知識進行了介紹、
討論和歸納，實現了邏輯與計算機之間的知識貫通。
本書主要內容包括邏輯與等式、計算機算術、算法、計算實踐四個部分，採用三種形式化表示法，
即傳統的邏輯代數公式表示法、數字電路圖表示法以及ACL2表示法實現邏輯推理。
本書不僅可以作為高等學校計算機、人工智能、大數據及相關專業的邏輯課程教材，
也可供廣大計算機愛好者、計算機及相關領域的科研人員和工程技術人員自學參考。

雷克斯·佩奇（Rex Page），美國俄克拉荷馬大學計算機科學學院榮休教授，專注於設計和開發可靠的數字電路和軟件的方法，在學術界和工業界從事可靠軟件領域的研發工作已有40年。
他於斯坦福大學獲得數學學士學位，加州大學聖地亞哥分校獲得數學博士學位。
在加入俄克拉荷馬大學之前，曾先後在科羅拉多州立大學和美國石油公司從事教學和研究工作。
他的早期工作為大規模並行計算系統開發了有效的軟件工程方法，在教學生涯中提倡在計算機科學和軟件工程的學士學位課程中加強應用邏輯的教育。
　　

魯本·岡博亞（Ruben Gamboa），懷俄明大學工程與應用科學學院計算機科學系教授，主要研究基於半自動化證明引擎ACL2的自動定理證明。
除此之外，他的研究興趣還包括NoSQL數據庫、近似算法、雲計算的應用、計算機圖形學等。他於得克薩斯農工大學獲得碩士學位，得克薩斯大學奧斯汀分校獲得博士學位。
他多次在ACL2Workshop中發表研究論文，並曾連續兩年任職於ACL2指導委員會。

出版者的話
譯者序
前言
第一部分 邏輯與等式
第1章 計算機系統：原理簡單，行為複雜 2
1.1 硬件與軟件 2
1.2 程序的結構 4
1.3 深藍與歸納定義 7
習題 10

第2章 布爾公式和等式 11
2.1 利用等式推理 11
習題 13
2.2 布爾等式 13
習題 19
2.3 布爾公式 19
習題 22
2.4 數字電路 23
習題 26
2.5 演繹推理 27
習題 36
2.6 謂詞和量詞 37
習題 40
2.7 量化謂詞的推理 40
習題 47
2.8 布爾模型 47
習題 52
2.9 謂詞和量詞的一般模型 52

第3章 軟件測試和前綴法 55
習題 59

第4章 數學歸納 61
4.1 數學對象列表 61
習題 65
4.2 數學歸納法 65
習題 71
4.3 Defun：ACL2中運算符的定義 71
4.4 連接、前綴和後綴 72
習題 77

第5章 機械化邏輯 78
5.1 ACL2定理與證明 78
5.2 使用已證的定理庫 80
習題 80
5.3 約束定理 81
習題 83
5.4 輔助機械化邏輯工作 83
習題 86
5.5 自動化證明及其做不到的事 86
習題 92

第二部分 計算機算術
第6章 二進制數字 94
6.1 數和數字 94
習題 98
6.2 從數字到數 99
習題 102
6.3 二進制數字 103
習題 104

第7章 加法器 106
7.1 數字相加 106
習題 106
7.2 一位二進制數字加法電路 106
7.3 兩位二進制數字加法電路 109
習題 110
7.4 w位二進制數字加法 110
習題 113
7.5 負數的數字 114
習題 116

第8章 乘法器和大數算法 118
8.1 大數加法器 118
習題 121
8.2 移位相加乘法器 121
習題 124

第三部分 算法
第9章 多路復用器和解復用器 126
9.1 多路復用器 126
習題 129
9.2 解復用器 129
習題 131

第10章 排序 132
10.1 插入排序 132
習題 135
10.2 保序合併 135
習題 137
10.3 歸併排序 137
習題 139
10.4 排序算法分析 139
10.4.1 計算步驟的計數 139
習題 141
10.4.2 計算解復用的步數 141
習題 142
10.4.3 計算歸併的步數 143
習題 144
10.4.4 計算歸併排序的步數 144
習題 147
10.4.5 計算插入排序的步數 147
習題 149

第11章 搜索樹 150
11.1 查找事物 150
11.2 平衡二叉樹 152
11.3 搜索樹的表示 154
11.4 有序搜索樹 155
習題 156
11.5 平衡搜索樹 156
習題 157
11.6 搜索樹中插入新項目 157
習題 159
11.7 順序插入 159
習題 163
11.8 雙旋轉 164
習題 167
11.9 快速插入 167
習題 169
第12章 哈希表 170
12.1 列表和數組 170
12.2 哈希運算符 172
習題 177
12.3 一些應用 178

第四部分 計算實踐
第13章 Facebook分片技術 182
13.1 技術挑戰 182
13.2 權宜之計 183
13.2.1 緩存 183
13.2.2 分片 184
13.3 Cassandra的解決方案 185
13.4 小結 186

第14章 MapReduce的並行計算 187
14.1 水平擴展和垂直擴展 187
14.2 MapReduce的策略 188
14.3 基於MapReduce的數據挖掘 191
14.4 小結 195

第15章 計算機藝術創作 196
15.1 在計算機中表示圖像 196
15.2 隨機生成圖像 198
15.3 生成目標圖像 201
索引 203