內容簡介
面向計算機科學的數理邏輯系統建模與推理
本書對計算機科學方面的數理邏輯進行了綜合介紹，涵蓋命題邏輯、謂詞邏輯、模態邏輯與代理、二叉判定圖、模型檢測和程式驗證等內容。本書主要討論有關軟硬體規範和驗證這一主題，反映了計算機科學中數理邏輯的新發展和實際需要。第2版新增了可滿足性算法、L6wenheim—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．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 SATEG的正確性
3．7．3 SATEU的正確性
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 模態邏輯KT45n
5．5．3 KT45n的自然演繹
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 算法res七rict
6．2．4 算法exis七s
6．2．5 OBDD的評價
6．3 符號模型檢測
6．3．1 表示狀態集合的子集
6．3．2 表示遷移關係
6．3．3 實現函式pre3和preν
6．3．4 綜合OBDD
6．4 關係μ演算
6．4．1 語法和語義
6．4．2 對CTL模型及規範說明的編碼
6．5 習題
6．6 文獻注釋
參考文獻
