面向計(jì)算機(jī)科學(xué)的數(shù)理邏輯系統(tǒng)建模與推理（原書(shū)第2版）

出版者的話
專家指導(dǎo)委員會(huì)
譯者序
第1版序
第2版前言
第1章 命題邏輯
1．1 判斷語(yǔ)句
1．2 自然演繹
1．2．1 自然演繹規(guī)則
1．2．2 派生規(guī)則
1．2．3 自然演繹總結(jié)
1．2．4 邏輯等價(jià)
1．2．5 側(cè)記：反證法
1．3 作為形式語(yǔ)言的命題邏輯
1．4 命題邏輯的語(yǔ)義
1．4．1 邏輯連接詞的含義
1．4．2 數(shù)學(xué)歸納法
1．4．3 命題邏輯的合理性
1．4．4 命題邏輯的完備性
1．5 范式
1．5．1 語(yǔ)義等價(jià)、滿足性和有效性
1．5．2 合取范式和有效性
1．5．3 霍恩子句和可滿足性
1．6 SAT求解機(jī)
1．6．1 線性求解機(jī)
1．6．2 三次求解機(jī)
1．7 習(xí)題
1．8 文獻(xiàn)注釋
第2章 謂詞邏輯
2．1 我們需要更豐富的語(yǔ)言
2．2 作為形式語(yǔ)言的謂詞邏輯
2．2．1 項(xiàng)
2．2．2 公式
2．2．3 自由變量和約束變量
2．2．4 代換
2．3 謂詞邏輯的證明論
2．3．1 自然演繹規(guī)則
2．3．2 量詞的等價(jià)
2．4 謂詞邏輯的語(yǔ)義
2．4．1 模型
2．4．2 語(yǔ)義推導(dǎo)
2．4．3 相等的語(yǔ)義
2．5 謂詞邏輯的不可判定性
2．6 謂詞邏輯的表達(dá)能力
2．6．1 存在式二階邏輯
2．6．2 全稱式二階邏輯
2．7 軟件的微觀模型
2．7．1 狀態(tài)機(jī)
2．7．2 Alma重觀
2．7．3 軟件的微模型

2．8 習(xí)題
2．9 文獻(xiàn)注釋
第3章 通過(guò)模型檢測(cè)進(jìn)行驗(yàn)證
3．1 驗(yàn)證的動(dòng)機(jī)
3．2 線性時(shí)態(tài)邏輯
3．2．1 LTL的語(yǔ)法
3．2．2 LTL的語(yǔ)義
3．2．3 規(guī)范的實(shí)際模式
3．2．4 LTL公式之間的重要等價(jià)
3．2．5 LTL的適當(dāng)連接詞集
3．3 模型檢測(cè)：系統(tǒng)、工具和性質(zhì)
3．3．1 例：互斥
3．3．2 NuSMV模型檢測(cè)器
3．3．3 運(yùn)行NuSMV
3．3．4 重溫互斥
3．3．5 擺渡者難題
3．3．6 交錯(cuò)位協(xié)議
3．4 分支時(shí)間邏輯
3．4．1 CTL的語(yǔ)法
3．4．2 計(jì)算樹(shù)邏輯的語(yǔ)義
3．4．3 規(guī)范的實(shí)際模式
3．4．4 CTL公式間的重要等價(jià)
3．4．5 CTL連接詞的適當(dāng)集
3．5 CTL*與LTL和CTL的表達(dá)能力
3．5．1 CTL中時(shí)態(tài)公式的布爾組合
3．5．2 LTL中的過(guò)去算子
3．6 模型檢測(cè)算法
3．6．1 CTL模型檢測(cè)算法
3．6．2 具有公平性的CTL模型檢測(cè)
3．6．3 LTL模型檢測(cè)算法
3．7 CTL的不動(dòng)點(diǎn)特征
3．7．1 單調(diào)函數(shù)
3．7．2 SATEG的正確性
3．7．3 SATEU的正確性
3．8 習(xí)題
3．9 文獻(xiàn)注釋
第4章 程序驗(yàn)證
4．1 為什么要規(guī)范和驗(yàn)證編碼
4．2 軟件驗(yàn)證的一種框架
4．2．1 一種核心程序設(shè)計(jì)語(yǔ)言
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 習(xí)題

4．7 文獻(xiàn)注釋
第5章 模態(tài)邏輯與代理
5．1 真值的模式
5．2 基本模態(tài)邏輯
5．2．1 語(yǔ)法
5．2．2 語(yǔ)義
5．3 邏輯工程
5．3．1 有效公式儲(chǔ)備
5．3．2 可達(dá)關(guān)系的重要性質(zhì)
5．3．3 對(duì)應(yīng)理論
5．3．4 一些模態(tài)邏輯
5．4 自然演繹
5．5 多代理系統(tǒng)中的知識(shí)推理
5．5．1 一些例子
5．5．2 模態(tài)邏輯KT45n
5．5．3 KT45n的自然演繹
5．5．4 例子的形式化
5．6 習(xí)題
5．7 文獻(xiàn)注釋
第6章 二叉判定圖
6．1 布爾函數(shù)的表示
6．1．1 命題公式和真值表
6．1．2 二叉判定圖
6．1．3 有序BDD
6．2 簡(jiǎn)約OBDD的算法
6．2．1 算法reduce
6．2．2 算法apply
6．2．3 算法res七rict
6．2．4 算法exis七s
6．2．5 OBDD的評(píng)價(jià)
6．3 符號(hào)模型檢測(cè)
6．3．1 表示狀態(tài)集合的子集
6．3．2 表示遷移關(guān)系
6．3．3 實(shí)現(xiàn)函數(shù)pre3和preν
6．3．4 綜合OBDD
6．4 關(guān)系μ演算
6．4．1 語(yǔ)法和語(yǔ)義
6．4．2 對(duì)CTL模型及規(guī)范說(shuō)明的編碼
6．5 習(xí)題
6．6 文獻(xiàn)注釋
參考文獻(xiàn)