面向計算機科學的數理邏輯(系統建模與推理原書第2版)

邁克爾·休斯（Michael Huth）現任紐倫堡科技大學（UTN）創始校長。在加入UTN之前，休斯教授曾在倫敦帝國理工學院工作，歷任電腦科學教授、電腦系主任，並將繼續擔任客座教授。在研究和教學方面，他目前的研究重點是人工智能和網絡安全領域的前瞻性課題。

譯者序
第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模型及規範說明的編碼
6.5 習題
6.6 文獻註釋
參考文獻