面向電腦科學的數理邏輯(系統建模與推理原書第2版)/電腦科學叢書
內容大鋼
數理邏輯是電腦科學的基礎之一，在模型與系統的規範與驗證等方面有著廣泛的應用。隨著當今軟硬體產品（電路、程序和通信協議等）日趨複雜，數理邏輯已經成為設計開發人員的日常工具。
作為電腦及其相關專業的數理邏輯課程教材，本書自出版以來受到了廣泛的好評，世界許多著名大學（比如美國普林斯頓大學、卡內基?梅隆大學、英國劍橋大學、德國漢堡大學、加拿大多倫多大學、荷蘭Vrije大學、印度理工學院）都採用本書作為教材。
全書涵蓋了命題邏輯、謂詞邏輯、模態邏輯與代理、二叉判定圖、模型檢測和程序驗證等內容。主要特色就是緊緊圍繞軟硬體規約和驗證這一主題，反映電腦科學中數理邏輯的發展和實際需要。第2版新增了可滿足性（SAT）演算法、緊致性理論和L?wenheim-Skolem定理，並介紹了Alloy語言和NuSMV工具。
本書適合作為高等院校電腦及相關專業的數理邏輯/形式化方法課程的教材，也可供相關研究人員和專業人士參考。
作者介紹
(德)邁克爾·休斯//(英)馬克·萊恩|責編:姚蕾|譯者:何偉//樊磊
目錄
譯者序
第1版序
第2版前言
致謝
第1章 命題邏輯
1.1 判斷語句
1.2 自然演繹
1.2.1 自然演繹規則
1.2.2 派生規則
1.2.3 自然演繹總結
1.2.4 邏輯等價
1.2.5 側記：反證法
1.3 作為形式語言的命題邏輯
1.4.1 邏輯連接詞的含義
1.4.2 數學歸納法
1.4.3 命題邏輯的合理性
1.4.4 命題邏輯的完備性
1.5 範式
1.5.1 語義等價、滿足性和有效性
1.5.2 合取範式和有效性
1.5.3 霍恩子句和可滿足性
1.6 SAT求解機
1.6.1 線性求解機
1.6.2 三次求解機
1.7 習題
1.8 文獻註釋
第2章 謂詞邏輯
2.1 我們需要更豐富的語言
2.2 作為形式語言的謂詞邏輯
2.2.1 項
2.2.2 公式
2.2.3 自由變數和約束變數
2.2.4 代換
2.3 謂詞邏輯的證明論
2.3.1 自然演繹規則
2.3.2 量詞的等價
2.4 謂詞邏輯的語義
2.4.1 模型
2.4.2 語義推導
2.4.3 相等的語義
2.5 謂詞邏輯的不可判定性
2.6 謂詞邏輯的表達能力
2.6.1 存在式二階邏輯
2.6.2 全稱式二階邏輯
2.7 軟體的微觀模型
2.7.1 狀態機
2.7.2 Alma重現
2.7.3 軟體的微模型
2.8 習題
2.9 文獻註釋
第3章 通過模型檢測進行驗證
3.1 驗證的動機
3.2 線性時態邏輯
3.2.1 LTL的語法
3.2.2 LTL的語義
3.2.3 規範的實際模式
3.2.4 LTL公式之間的重要等價
3.2.5 LTL的適當連接詞集
3.3 模型檢測：系統、工具和性質
3.3.1 例：互斥
3.3.2 NuSMV模型檢測器
3.3.3 運行NuSMV
3.3.4 重濕互斥
3.3.5 擺渡者難題
3.3.6 交錯位協議
3.4 分支時間邏輯
3.4.1 CTL的語法
3.4.2 計算樹邏輯的語義
3.4.3 規範的實際模式
3.4.4 CTL公式間的重要等價
3.4.5 CTL連接詞的適當集
3.5 CTL與LTL和CTL的表達能力
3.5.1 CTL中時態公式的布爾組合
3.5.2 LTL中的過去運算元
3.6 模型檢測演算法
3.6.1 CTL模型檢測演算法
3.6.2 具有公平性的CTL模型檢測
3.6.3 LTL模型檢測演算法
3.7 CTL的不動點特徵
3.7.1 單調函數
3.7.2 SAT的正確性
3.7.3 SAT的正確性
3.8 習題
3.9 文獻註釋
第4章 程序驗證
4.1 為什麼要規範和驗證編程
4.2 軟體驗證的一種框架
4.2.1 一種核心程序設計語言
4.2.2 霍爾三元組
4.2.3 部分正確性和完全正確性
4.2.4 程序變數和邏輯變數
4.3 部分正確性的證明演算
4.3.1 證明規則
4.3.2 證明布景
4.3.3 案例研究：最小和截段
4.4 完全正確性的證明演算
4.5 合同編程
4.6 習題
4.7 文獻註釋
第5章 模態邏輯與代理
5.1 真值的模式
5.2 基本模態邏輯
5.2.1 語法
5.2.2 語義
5.3 邏輯工程
5.3.1 有效公式儲備
5.3.2 可達關係的重要性質
5.3.3 對應理論
5.3.4 一些模態邏輯
5.4 自然演繹
5.5 多代理系統中的知識推理
5.5.1 一些例子
5.5.2 模態邏輯KT45
5.5.3 KT45的自然演繹
5.5.4 例子的形式化
5.6 習題
5.7 文獻註釋
第6章 二叉判定圖
6.1 布爾函數的表示
6.1.1 命題公式和真值表
6.1.2 二叉判定圖
6.1.3 有序BDD
6.2 簡約OBDD的演算法
6.2.1 演算法reduce
6.2.2 演算法apply
6.2.3 演算法restrict
6.2.4 演算法exists
6.2.5 OBDD的評價
6.3 符號模型檢測
6.3.1 表示狀態集合的子集
6.3.2 表示遷移關係
6.3.3 實現函數preE和preA
6.3.4 綜合OBDD
6.4 關係μ演算
6.4.1 語法和語義
6.4.2 對CTL模型及規範�
[