中圖網小程序
一鍵登錄
更方便
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
面向計算機科學的數理邏輯:系統建模與推理:原書第2版 版權信息
- ISBN：9787111770688
- 條形碼：9787111770688 ; 978-7-111-77068-8
- 裝幀：平裝-膠訂
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
面向計算機科學的數理邏輯:系統建模與推理:原書第2版 本書特色
作為計算機及其相關專業的數理邏輯課程教材，本書自出版以來受到了廣泛的好評，世界許多著名大學（比如美國普林斯頓大學、卡內基·梅隆大學、英國劍橋大學、德國漢堡大學、加拿大多倫多大學、荷蘭Vrije大學、印度理工學院）都采用本書作為教材。全書涵蓋了命題邏輯、謂詞邏輯、模態邏輯與代理、二叉判定圖、模型檢測和程序驗證等內容。主要特色就是緊緊圍繞軟硬件規約和驗證這一主題，反映計算機科學中數理邏輯的發展和實際需要。第2版新增了可滿足性（SAT）算法、緊致性理論和l?wenheim-Skolem定理，并介紹了Alloyy語言和NuSMV工具。本書適合作為高等院校計算機及相關專業的數理邏輯/形式化方法課程的教材，也可供相關研究人員和專業人士參考。
面向計算機科學的數理邏輯:系統建模與推理:原書第2版 內容簡介
本書對計算機科學方面的數理邏輯進行了綜合介紹，涵蓋命題邏輯、謂詞邏輯、模態邏輯與代理、二叉判定圖、模型檢測和程序驗證等內容。
面向計算機科學的數理邏輯:系統建模與推理:原書第2版面向計算機科學的數理邏輯:系統建模與推理:原書第2版 前言
第2版前言Logic in Computer Science：Modelling and Reasoning about Systems,Second Edition
本書的（重新）寫作動機
本書第1版的寫作主旨之一來自于以下觀察：在計算機系統的設計、規范描述和驗證中使用的大多數邏輯基本上都是處理一個滿足關系 M ╞ φ
其中M是某種場景或系統的模型，而 φ 是一個規范，該邏輯的一個公式用來描述在場景M中什么應該是真的。這種結構的核心在于：我們可以經常規范并實現計算 ╞ 的算法。我們為命題邏輯、一階邏輯、時態邏輯、模態邏輯和程序邏輯發展了這個主題。基于我們所收到的來自五大洲讀者的鼓勵性反饋，我們很高興出版本書的第2版，本版遵循了第1版的原始主旨并有所改進。
面向計算機科學的數理邏輯:系統建模與推理:原書第2版 目錄
譯者序
第1版序
第2版前言
致謝
第1章 命題邏輯1
1.1 判斷語句1
1.2 自然演繹3
1.2.1 自然演繹規則4
1.2.2 派生規則15
1.2.3 自然演繹總結17
1.2.4 邏輯等價19
1.2.5 側記：反證法19
1.3 作為形式語言的命題邏輯20
1.4 命題邏輯的語義23
1.4.1 邏輯連接詞的含義23
1.4.2 數學歸納法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 自然演繹規則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 狀態機93
2.7.2 Alma重觀95
2.7.3 軟件的微模型97
2.8 習題102
2.9 文獻注釋113
第3章 通過模型檢測進行驗證115
3.1 驗證的動機115
3.2 線性時態邏輯117
3.2.1 LTL的語法117
3.2.2 LTL的語義118
3.2.3 規范的實際模式122
3.2.4 LTL公式之間的重要等價123
3.2.5 LTL的適當連接詞集124
3.3 模型檢測: 系統、工具和性質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 交錯位協議134
3.4 分支時間邏輯138
3.4.1 CTL的語法138
3.4.2 計算樹邏輯的語義139
3.4.3 規范的實際模式142
3.4.4 CTL公式間的重要等價142
3.4.5 CTL連接詞的適當集143
3.5 CTL^*與LTL和CTL的
表達能力144
3.5.1 CTL中時態公式的布爾
組合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 單調函數158
3.7.2 SAT_EG的正確性159
3.7.3 SAT_EU的正確性160
3.8 習題161
3.9 文獻注釋168
第4章 程序驗證170
4.1 為什么要規范和驗證編碼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 證明規則177
4.3.2 證明布景180
4.3.3 案例研究：*小和截段189
4.4 完全正確性的證明演算192
4.5 合同編程194
4.6 習題196
4.7 文獻注釋200
第5章 模態邏輯與代理202
5.1 真值的模式202
5.2 基本模態邏輯202
5.2.1 語法202
5.2.2 語義204
5.3 邏輯工程208
5.3.1 有效公式儲備209
5.3.2 可達關系的重要性質210
5.3.3 對應理論212
5.3.4 一些模態邏輯214
5.4 自然演繹216
5.5 多代理系統中的知識推理218
5.5.1 一些例子218
5.5.2 模態邏輯KT45^n220
5.5.3 KT45^n的自然演繹223
5.5.4 例子的形式化224
5.6 習題230
5.7 文獻注釋236
第6章 二叉判定圖237
6.1 布爾函數的表示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 表示狀態集合的子集253
6.3.2 表示遷移關系255
6.3.3 實現函數pre_?和pre_?255
6.3.4 綜合OBDD 256
6.4 關系μ演算257
6.4.
第1版序
第2版前言
致謝
第1章 命題邏輯1
1.1 判斷語句1
1.2 自然演繹3
1.2.1 自然演繹規則4
1.2.2 派生規則15
1.2.3 自然演繹總結17
1.2.4 邏輯等價19
1.2.5 側記：反證法19
1.3 作為形式語言的命題邏輯20
1.4 命題邏輯的語義23
1.4.1 邏輯連接詞的含義23
1.4.2 數學歸納法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 自然演繹規則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 狀態機93
2.7.2 Alma重觀95
2.7.3 軟件的微模型97
2.8 習題102
2.9 文獻注釋113
第3章 通過模型檢測進行驗證115
3.1 驗證的動機115
3.2 線性時態邏輯117
3.2.1 LTL的語法117
3.2.2 LTL的語義118
3.2.3 規范的實際模式122
3.2.4 LTL公式之間的重要等價123
3.2.5 LTL的適當連接詞集124
3.3 模型檢測: 系統、工具和性質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 交錯位協議134
3.4 分支時間邏輯138
3.4.1 CTL的語法138
3.4.2 計算樹邏輯的語義139
3.4.3 規范的實際模式142
3.4.4 CTL公式間的重要等價142
3.4.5 CTL連接詞的適當集143
3.5 CTL^*與LTL和CTL的
表達能力144
3.5.1 CTL中時態公式的布爾
組合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 單調函數158
3.7.2 SAT_EG的正確性159
3.7.3 SAT_EU的正確性160
3.8 習題161
3.9 文獻注釋168
第4章 程序驗證170
4.1 為什么要規范和驗證編碼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 證明規則177
4.3.2 證明布景180
4.3.3 案例研究：*小和截段189
4.4 完全正確性的證明演算192
4.5 合同編程194
4.6 習題196
4.7 文獻注釋200
第5章 模態邏輯與代理202
5.1 真值的模式202
5.2 基本模態邏輯202
5.2.1 語法202
5.2.2 語義204
5.3 邏輯工程208
5.3.1 有效公式儲備209
5.3.2 可達關系的重要性質210
5.3.3 對應理論212
5.3.4 一些模態邏輯214
5.4 自然演繹216
5.5 多代理系統中的知識推理218
5.5.1 一些例子218
5.5.2 模態邏輯KT45^n220
5.5.3 KT45^n的自然演繹223
5.5.4 例子的形式化224
5.6 習題230
5.7 文獻注釋236
第6章 二叉判定圖237
6.1 布爾函數的表示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 表示狀態集合的子集253
6.3.2 表示遷移關系255
6.3.3 實現函數pre_?和pre_?255
6.3.4 綜合OBDD 256
6.4 關系μ演算257
6.4.
展開全部
面向計算機科學的數理邏輯:系統建模與推理:原書第2版 作者簡介
邁克爾·休斯（Michael Huth）現任紐倫堡科技大學（UTN）創始校長。在加入UTN之前，休斯教授曾在倫敦帝國理工學院工作，歷任計算機科學教授、計算機系主任，并將繼續擔任客座教授。在研究和教學方面，他目前的研究重點是人工智能和網絡安全領域的前瞻性課題。
馬克·萊恩（Mark Ryan）伯明翰大學計算機科學學院計算機安全教授，也是伯明翰大學安全與隱私中心的負責人。他的主要研究方向包括機器學習的安全性、應用密碼學和安全協議、安全系統分析、隱私計算等。
書友推薦
- >
上帝之肋:男人的真實旅程
- >
姑媽的寶刀
- >
莉莉和章魚
- >
龍榆生：詞曲概論/大家小書
- >
推拿
- >
山海經
- >
大紅狗在馬戲團-大紅狗克里弗-助人
- >
人文閱讀與收藏·良友文學叢書:一天的工作
本類暢銷
