作為思維的基本形式和基本規(guī)則，邏輯構(gòu)成了人類思維和機(jī)器思維的共同基礎(chǔ)，也是計(jì)算機(jī)科學(xué)與信息科學(xué)的理論基礎(chǔ)。事實(shí)上，無論是計(jì)算機(jī)硬件還是計(jì)算機(jī)軟件，它們都是一組邏輯組件的某種特定表現(xiàn)形式。具備嚴(yán)謹(jǐn)?shù)倪壿嬎季S能力對于計(jì)算機(jī)系統(tǒng)研發(fā)人員的重要性是毋庸置疑的。然而，邏輯思維能力的培養(yǎng)并不是一件很容易的事情，通常需要經(jīng)歷一定的理論學(xué)習(xí)和實(shí)際訓(xùn)練。目前，計(jì)算機(jī)專業(yè)的學(xué)生主要是通過離散數(shù)學(xué)等數(shù)學(xué)課程進(jìn)行形式邏輯方面的學(xué)習(xí)，而不是直接面向計(jì)算機(jī)專業(yè)內(nèi)容討論計(jì)算機(jī)科學(xué)的基本邏輯，這使得學(xué)生接觸到的邏輯知識與計(jì)算機(jī)科學(xué)的關(guān)系較為松散，不利于邏輯與計(jì)算機(jī)之間的知識貫通。本書可以很好地彌補(bǔ)這方面的不足。它以實(shí)際問題的求解為導(dǎo)向，對計(jì)算機(jī)科學(xué)的邏輯基礎(chǔ)知識進(jìn)行了比較系統(tǒng)的介紹、討論和歸納，較好地實(shí)現(xiàn)了邏輯與計(jì)算機(jī)之間的知識貫通，可以有效地培育和提升讀者的邏輯思維能力，使其能夠在計(jì)算機(jī)邏輯方面獲得比較系統(tǒng)的專業(yè)訓(xùn)練，從而能夠更加高效地從事計(jì)算機(jī)軟硬件產(chǎn)品的研發(fā)工作。本書的基本特點(diǎn)主要表現(xiàn)在如下三個(gè)方面：
　　第一，知識體系的組織結(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)域的問題，包括硬件組件、軟件組件、測試和驗(yàn)證以及算法分析，邏輯知識與計(jì)算機(jī)知識的聯(lián)系更加緊密，實(shí)現(xiàn)了兩者的深度融合，特別適合用來對計(jì)算機(jī)專業(yè)人員進(jìn)行系統(tǒng)性的邏輯訓(xùn)練。
　　第二，在可讀性方面做了很好的設(shè)計(jì)，主要通過一些生動有趣的具體應(yīng)用實(shí)例介紹邏輯知識和證明方法，能夠有效地激發(fā)讀者的學(xué)習(xí)興趣，培養(yǎng)讀者的邏輯思維和數(shù)學(xué)思維能力。例如，通過石頭、剪刀、布這個(gè)簡單的游戲深入淺出地闡述程序的基本結(jié)構(gòu)和基于等式的程序模型，生動地解釋了在基于等式的模型中，程序?yàn)楹瓮耆�由基于操作�?shù)的數(shù)學(xué)函數(shù)組成，為何可以使用經(jīng)典邏輯和傳統(tǒng)代數(shù)公式來理解基于等式的程序。通過介紹深藍(lán)計(jì)算機(jī)系統(tǒng)的基本工作原理來介紹歸納定義，使得讀者能夠清楚地認(rèn)識到，對于計(jì)算機(jī)系統(tǒng)和邏輯系統(tǒng)而言，再復(fù)雜的行為通常也是從最初簡單的行為演變而來，再復(fù)雜的理論通常也是建立在一些簡單的基本原則基礎(chǔ)之上。
　　第三，采用三種形式化表示法，即傳統(tǒng)的邏輯代數(shù)公式表示法、數(shù)字電路圖表示法以及ACL2表示法，使得學(xué)生可以借助軟件工具比較容易地學(xué)習(xí)機(jī)械化邏輯的相關(guān)知識。本書使用ACL2作為邏輯證明引擎，ACL2提供了比任何其他工具更容易理解的機(jī)械化邏輯證明形式，通過事實(shí)生動地說明軟件和硬件工程師可以如何從邏輯（包括機(jī)械化邏輯）中受益。當(dāng)讀者在檢查證據(jù)和處理證明細(xì)節(jié)的很多方面得到ACL2軟件工具的有效支持時(shí)，會非常開心并且更有學(xué)習(xí)動力。