本書對計算機科學方面的數理邏輯進行了綜合介紹，涵蓋命題邏輯、謂詞邏輯、通過模型檢測進行驗證、程序驗證、模態(tài)邏輯與代理、二叉判定圖這些內容。本書主要討論有關軟硬件規(guī)范和驗證這一主題的內容，反映了計算機科學中數理邏輯的新發(fā)展和實際需要。第2版新增了可滿足性算法、Lowenheim-Skolem定理，并介紹了Alloy語言和NuSMV工具等內容。