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

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