商品簡介
《計算機科學的邏輯基礎》以實際問題的求解為導向，對計算機科學的邏輯基礎知識進行了介紹、討論和歸納，實現了邏輯與計算機之間的知識貫通。
《計算機科學的邏輯基礎》主要內容包括邏輯與等式、計算機算術、算法、計算實踐四個部分，采用三種形式化表示法，即傳統的邏輯代數公式表示法、數字電路圖表示法以及ACL2表示法實現邏輯推理。
《計算機科學的邏輯基礎》不僅可以作為高等學校計算機、人工智能、大數據及相關專業的邏輯課程教材，也可供廣大計算機愛好者、計算機及相關領域的科研人員和工程技術人員自學參考。
《計算機科學的邏輯基礎》以實際問題的求解為導向，對計算機科學的邏輯基礎知識進行了介紹、討論和歸納，完美地實現了邏輯與計算機之間的知識貫通。
《計算機科學的邏輯基礎》主要內容包括邏輯與等式、計算機算術、算法、計算實踐四個部分，采用三種形式化表示法，即傳統的邏輯代數公式表示法、數字電路圖表示法以及ACL2表示法實現邏輯推理。
《計算機科學的邏輯基礎》特色：
知識體系的組織結構突破了傳統的數學框架，直接面向與計算機科學相關的邏輯主題，將邏輯用於解決計算機科學領域的重要問題。
結合生動有趣的具體應用實例介紹邏輯知識和證明方法，能夠有效地激發讀者的學習興趣，特別有助於培養讀者的邏輯思維和數學思維。
采用三種形式化表示方法實現邏輯推理並將ACL2作為邏輯證明引擎，通過實際應用效果生動地驗證了軟件和硬件工程師均可以從邏輯（包括機械化邏輯）的學習中獲益。
作者簡介
雷克斯·佩奇（Rex Page），美國俄克拉荷馬大學計算機科學學院榮休教授，專注於設計和開發可靠的數字電路和軟件的方法，在學術界和工業界從事可靠軟件領域的研發工作已有40年。他於斯坦福大學獲得數學學士學位，加州大學聖地亞哥分校獲得數學博士學位。在加入俄克拉荷馬大學之前，曾先後在科羅拉多州立大學和美國石油公司從事教學和研究工作。他的早期工作為大規模並行計算系統開發了有效的軟件工程方法，在教學生涯中提倡在計算機科學和軟件工程的學士學位課程中加強應用邏輯的教育。
魯本·岡博亞（Ruben Gamboa），懷俄明大學工程與應用科學學院計算機科學系教授，主要研究基於半自動化證明引擎ACL2的自動定理證明。除此之外，他的研究興趣還包括NoSQL數據庫、近似算法、云計算的應用、計算機圖形學等。他於得克薩斯農工大學獲得碩士學位，得克薩斯大學奧斯汀分校獲得博士學位。他多次在ACL2Workshop中發表研究論文，並曾連續兩年任職於ACL2指導委員會。
名人/編輯推薦
完美實現邏輯與計算機的知識貫通，培養計算機學生數理邏輯思維
序
第一，知識體系的組織結構突破了傳統的數學框架，內容主要包括邏輯與等式、計算機算術、算法、計算實踐四個部分，直接關注與計算機科學相關的邏輯主題，將邏輯用於解決計算機科學領域的問題，包括硬件組件、軟件組件、測試和驗證以及算法分析，邏輯知識與計算機知識的聯系更加緊密，實現了兩者的深度融合，特別適合用來對計算機專業人員進行系統性的邏輯訓練。
第二，在可讀性方面做了很好的設計，主要通過一些生動有趣的具體應用實例介紹邏輯知識和證明方法，能夠有效地激發讀者的學習興趣，培養讀者的邏輯思維和數學思維能力。例如，通過石頭、剪刀、布這個簡單的遊戲深入淺出地闡述程序的基本結構和基於等式的程序模型，生動地解釋了在基於等式的模型中，程序為何完全由基於操作數的數學函數組成，為何可以使用經典邏輯和傳統代數公式來理解基於等式的程序。通過介紹深藍計算機系統的基本工作原理來介紹歸納定義，使得讀者能夠清楚地認識到，對於計算機系統和邏輯系統而言，再復雜的行為通常也是從最初簡單的行為演變而來，再復雜的理論通常也是建立在一些簡單的基本原則基礎之上。
第三，采用三種形式化表示法，即傳統的邏輯代數公式表示法、數字電路圖表示法以及ACL2表示法，使得學生可以借助軟件工具比較容易地學習機械化邏輯的相關知識。本書使用ACL2作為邏輯證明引擎，ACL2提供了比任何其他工具更容易理解的機械化邏輯證明形式，通過事實生動地說明軟件和硬件工程師可以如何從邏輯（包括機械化邏輯）中受益。當讀者在檢查證據和處理證明細節的很多方面得到ACL2軟件工具的有效支持時，會非常開心並且更有學習動力。
目次
譯者序
前言
第一部分 邏輯與等式
第1章 計算機系統：原理簡單，行為復雜
1．1 硬件與軟件
1．2 程序的結構
1．3 深藍與歸納定義
習題
第2章 布爾公式和等式
2．1 利用等式推理
習題
2．2 布爾等式
習題
2．3 布爾公式
習題
2．4 數字電路
習題
2．5 演繹推理
習題
2．6 謂詞和量詞
習題
2．7 量化謂詞的推理
習題
2．8 布爾模型
習題
2．9 謂詞和量詞的一般模型
第3章 軟件測試和前綴法
習題
第4章 數學歸納
4．1 數學物件列表
習題
4．2 數學歸納法
習題
4．3 Defun：ACL2中運算符的定義
4．4 連接、前綴和後綴
習題
第5章 機械化邏輯
5．1 ACL2定理與證明
5．2 使用已證的定理庫
習題
5．3 約束定理
習題
5．4 輔助機械化邏輯工作
習題
5．5 自動化證明及其做不到的事
習題
第二部分 計算機算術
第6章 二進制數字
6．1 數和數字
習題
6．2 從數字到數
習題
6．3 二進制數字
習題
第7章 加法器
7．1 數字相加
習題
7．2 一位二進制數字加法電路
7．3 兩位二進制數字加法電路
習題
7．4 w位二進制數字加法
習題
7．5 負數的數字
習題
第8章 乘法器和大數算法
8．1 大數加法器
習題
8．2 移位相加乘法器
習題
第三部分 算法
第9章 多路復用器和解復用器
9．1 多路復用器
習題
9．2 解復用器
習題
第10章 排序
10．1 插入排序
習題
10．2 保序合並
習題
10．3 歸並排序
習題
10．4 排序算法分析
10．4．1 計算步驟的計數
習題
10．4．2 計算解復用的步數
習題
10．4．3 計算歸並的步數
習題
10．4．4 計算歸並排序的步數
習題
10．4．5 計算插入排序的步數
習題
第11章 搜索樹
11．1 查找事物
11．2 平衡二叉樹
11．3 搜索樹的表示
11．4 有序搜索樹
習題
11．5 平衡搜索樹
習題
11．6 搜索樹中插入新項目
習題
11．7 順序插入
習題
11．8 雙旋轉
習題
11．9 快速插入
習題
第12章 哈希表
12．1 列表和數組
12．2 哈希運算符
習題
12．3 一些應用
……
第四部分 計算實踐
索引
您曾經瀏覽過的商品
購物須知
大陸出版品因裝訂品質及貨運條件與台灣出版品落差甚大，除封面破損、內頁脫落等較嚴重的狀態，其餘商品將正常出貨。
特別提醒：部分書籍附贈之內容(如音頻mp3或影片dvd等)已無實體光碟提供，需以QR CODE 連結至當地網站註冊“並通過驗證程序”，方可下載使用。
無現貨庫存之簡體書，將向海外調貨：
海外有庫存之書籍，等候約45個工作天;
海外無庫存之書籍，平均作業時間約60個工作天，然不保證確定可調到貨，尚請見諒。
為了保護您的權益，「三民網路書店」提供會員七日商品鑑賞期(收到商品為起始日)。
若要辦理退貨，請在商品鑑賞期內寄回，且商品必須是全新狀態與完整包裝(商品、附件、發票、隨貨贈品等)否則恕不接受退貨。