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

譯者序
第1版序
第2版前言
致謝
第1章　命題邏輯1
　1.1　判斷語(yǔ)句1
　1.2　自然演繹3
　　1.2.1　自然演繹規(guī)則4
　　1.2.2　派生規(guī)則15
　　1.2.3　自然演繹總結(jié)17
　　1.2.4　邏輯等價(jià)19
　　1.2.5　側(cè)記：反證法19
　1.3　作為形式語(yǔ)言的命題邏輯20
　1.4　命題邏輯的語(yǔ)義23
　　1.4.1　邏輯連接詞的含義23
　　1.4.2　數(shù)學(xué)歸納法25
　　1.4.3　命題邏輯的合理性28
　　1.4.4　命題邏輯的完備性30
　1.5　范式33
　　1.5.1　語(yǔ)義等價(jià)、滿(mǎn)足性和
有效性34
　　1.5.2　合取范式和有效性36
　　1.5.3　霍恩子句和可滿(mǎn)足性41
　1.6　SAT求解機(jī)42
　　1.6.1　線性求解機(jī)43
　　1.6.2　三次求解機(jī)45
　1.7　習(xí)題50
　1.8　文獻(xiàn)注釋61
第2章　謂詞邏輯62
　2.1　我們需要更豐富的語(yǔ)言62
　2.2　作為形式語(yǔ)言的謂詞邏輯65
　　2.2.1　項(xiàng)66
　　2.2.2　公式66
　　2.2.3　自由變量和約束變量68
　　2.2.4　代換69
　2.3　謂詞邏輯的證明論71
　　2.3.1　自然演繹規(guī)則71
　　2.3.2　量詞的等價(jià)77
　2.4　謂詞邏輯的語(yǔ)義80
　　2.4.1　模型81
　　2.4.2　語(yǔ)義推導(dǎo)85
　　2.4.3　相等的語(yǔ)義86
　2.5　謂詞邏輯的不可判定性86
　2.6　謂詞邏輯的表達(dá)能力89
　　2.6.1　存在式二階邏輯91
　　2.6.2　全稱(chēng)式二階邏輯91
　2.7　軟件的微觀模型92
　　2.7.1　狀態(tài)機(jī)93
　　2.7.2　Alma重觀95
　　2.7.3　軟件的微模型97
　2.8　習(xí)題102
　2.9　文獻(xiàn)注釋113
第3章　通過(guò)模型檢測(cè)進(jìn)行驗(yàn)證115
　3.1　驗(yàn)證的動(dòng)機(jī)115
　3.2　線性時(shí)態(tài)邏輯117
　　3.2.1　LTL的語(yǔ)法117
　　3.2.2　LTL的語(yǔ)義118
　　3.2.3　規(guī)范的實(shí)際模式122
　　3.2.4　LTL公式之間的重要等價(jià)123
　　3.2.5　LTL的適當(dāng)連接詞集124
　3.3　模型檢測(cè): 系統(tǒng)、工具和性質(zhì)124
　　3.3.1　例: 互斥124
　　3.3.2　NuSMV模型檢測(cè)器127
　　3.3.3　運(yùn)行NuSMV129
　　3.3.4　重溫互斥129
　　3.3.5　擺渡者難題132
　　3.3.6　交錯(cuò)位協(xié)議134
　3.4　分支時(shí)間邏輯138
　　3.4.1　CTL的語(yǔ)法138
　　3.4.2　計(jì)算樹(shù)邏輯的語(yǔ)義139
　　3.4.3　規(guī)范的實(shí)際模式142
　　3.4.4　CTL公式間的重要等價(jià)142
　　3.4.5　CTL連接詞的適當(dāng)集143
　3.5　CTL^*與LTL和CTL的
表達(dá)能力144
　　3.5.1　CTL中時(shí)態(tài)公式的布爾
組合145
　　3.5.2　LTL中的過(guò)去算子146
　3.6　模型檢測(cè)算法146
　　3.6.1　CTL模型檢測(cè)算法146
　　3.6.2　具有公平性的CTL模型
檢測(cè)151
　　3.6.3　LTL模型檢測(cè)算法153
　3.7　CTL的不動(dòng)點(diǎn)特征157
　　3.7.1　單調(diào)函數(shù)158
　　3.7.2　SAT_EG的正確性159
　　3.7.3　SAT_EU的正確性160
　3.8　習(xí)題161
　3.9　文獻(xiàn)注釋168
第4章　程序驗(yàn)證170
　4.1　為什么要規(guī)范和驗(yàn)證編碼170
　4.2　軟件驗(yàn)證的一種框架171
　　4.2.1　一種核心程序設(shè)計(jì)語(yǔ)言172
　　4.2.2　霍爾三元組173
　　4.2.3　部分正確性和完全
正確性175
　　4.2.4　程序變量和邏輯變量176
　4.3　部分正確性的證明演算177
　　4.3.1　證明規(guī)則177
　　4.3.2　證明布景180
　　4.3.3　案例研究：最小和截段189
　4.4　完全正確性的證明演算192
　4.5　合同編程194
　4.6　習(xí)題196
　4.7　文獻(xiàn)注釋200
第5章　模態(tài)邏輯與代理202
　5.1　真值的模式202
　5.2　基本模態(tài)邏輯202
　　5.2.1　語(yǔ)法202
　　5.2.2　語(yǔ)義204
　5.3　邏輯工程208
　　5.3.1　有效公式儲(chǔ)備209
　　5.3.2　可達(dá)關(guān)系的重要性質(zhì)210
　　5.3.3　對(duì)應(yīng)理論212
　　5.3.4　一些模態(tài)邏輯214
　5.4　自然演繹216
　5.5　多代理系統(tǒng)中的知識(shí)推理218
　　5.5.1　一些例子218
　　5.5.2　模態(tài)邏輯KT45^n220
　　5.5.3　KT45^n的自然演繹223
　　5.5.4　例子的形式化224
　5.6　習(xí)題230
　5.7　文獻(xiàn)注釋236
第6章　二叉判定圖237
　6.1　布爾函數(shù)的表示237
　　6.1.1　命題公式和真值表237
　　6.1.2　二叉判定圖239
　　6.1.3　有序BDD242
　6.2　簡(jiǎn)約OBDD的算法246
　　6.2.1　算法reduce246
　　6.2.2　算法apply247
　　6.2.3　算法restrict249
　　6.2.4　算法exists249
　　6.2.5　OBDD的評(píng)價(jià)251
　6.3　符號(hào)模型檢測(cè)252
　　6.3.1　表示狀態(tài)集合的子集253
　　6.3.2　表示遷移關(guān)系255
　　6.3.3　實(shí)現(xiàn)函數(shù)pre_?和pre_?255
　　6.3.4　綜合OBDD 256
　6.4　關(guān)系μ演算257
　　6.4.