123,123

內(nèi)容簡(jiǎn)介

　　本書對(duì)計(jì)算機(jī)科學(xué)方面的數(shù)理邏輯進(jìn)行了綜合介紹，涵蓋命題邏輯、謂詞邏輯、模態(tài)邏輯與代理、二叉判定圖、模型檢測(cè)和程序驗(yàn)證等內(nèi)容。

作者簡(jiǎn)介

　　邁克爾·休斯（Michael Huth）現(xiàn)任紐倫堡科技大學(xué)（UTN）創(chuàng)始校長(zhǎng)。在加入U(xiǎn)TN之前，休斯教授曾在倫敦帝國(guó)理工學(xué)院工作，歷任計(jì)算機(jī)科學(xué)教授、計(jì)算機(jī)系主任，并將繼續(xù)擔(dān)任客座教授。在研究和教學(xué)方面，他目前的研究重點(diǎn)是人工智能和網(wǎng)絡(luò)安全領(lǐng)域的前瞻性課題。馬克·萊恩（Mark Ryan）伯明翰大學(xué)計(jì)算機(jī)科學(xué)學(xué)院計(jì)算機(jī)安全教授，也是伯明翰大學(xué)安全與隱私中心的負(fù)責(zé)人。他的主要研究方向包括機(jī)器學(xué)習(xí)的安全性、應(yīng)用密碼學(xué)和安全協(xié)議、安全系統(tǒng)分析、隱私計(jì)算等。

圖書目錄

譯者序
第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à)、滿足性和
有效性34
　　1.5.2　合取范式和有效性36
　　1.5.3　霍恩子句和可滿足性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　全稱式二階邏輯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ì)算樹邏輯的語(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.