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

出版者的話
專家指導委員會
譯者序
第1版序
第2版前言
第1章 命題邏輯
1．1 判斷語句
1．2 自然演繹
1．2．1 自然演繹規(guī)則
1．2．2 派生規(guī)則
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 自然演繹規(guī)則
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 狀態(tài)機
2．7．2 Alma重觀
2．7．3 軟件的微模型

2．8 習題
2．9 文獻注釋
第3章 通過模型檢測進行驗證
3．1 驗證的動機
3．2 線性時態(tài)邏輯
3．2．1 LTL的語法
3．2．2 LTL的語義
3．2．3 規(guī)范的實際模式
3．2．4 LTL公式之間的重要等價
3．2．5 LTL的適當連接詞集
3．3 模型檢測：系統(tǒng)、工具和性質
3．3．1 例：互斥
3．3．2 NuSMV模型檢測器
3．3．3 運行NuSMV
3．3．4 重溫互斥
3．3．5 擺渡者難題
3．3．6 交錯位協(xié)議
3．4 分支時間邏輯
3．4．1 CTL的語法
3．4．2 計算樹邏輯的語義
3．4．3 規(guī)范的實際模式
3．4．4 CTL公式間的重要等價
3．4．5 CTL連接詞的適當集
3．5 CTL*與LTL和CTL的表達能力
3．5．1 CTL中時態(tài)公式的布爾組合
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 為什么要規(guī)范和驗證編碼
4．2 軟件驗證的一種框架
4．2．1 一種核心程序設計語言
4．2．2 霍爾三元組
4．2．3 部分正確性和完全正確性
4．2．4 程序變量和邏輯變量
4．3 部分正確性的證明演算
4．3．1 證明規(guī)則
4．3．2 證明布景
4．3．3 案例研究：最小和截段
4．4 完全正確性的證明演算
4．5 合同編程
4．6 習題

4．7 文獻注釋
第5章 模態(tài)邏輯與代理
5．1 真值的模式
5．2 基本模態(tài)邏輯
5．2．1 語法
5．2．2 語義
5．3 邏輯工程
5．3．1 有效公式儲備
5．3．2 可達關系的重要性質
5．3．3 對應理論
5．3．4 一些模態(tài)邏輯
5．4 自然演繹
5．5 多代理系統(tǒng)中的知識推理
5．5．1 一些例子
5．5．2 模態(tài)邏輯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 表示狀態(tài)集合的子集
6．3．2 表示遷移關系
6．3．3 實現函數pre3和preν
6．3．4 綜合OBDD
6．4 關系μ演算
6．4．1 語法和語義
6．4．2 對CTL模型及規(guī)范說明的編碼
6．5 習題
6．6 文獻注釋
參考文獻