計算機科學中的數理邏輯
宋麗華、王兆麗、韓敬利、夏青、王元元
- 出版商: 清華大學
- 出版日期: 2026-05-01
- 售價: $414
- 語言: 簡體中文
- ISBN: 7302713316
- ISBN-13: 9787302713319
-
相關分類:
Computer-Science
下單後立即進貨 (約4週~6週)
商品描述
目錄大綱
目錄
第0 章緒論........................................................................ 1
0.1 思維、感知的概念化和理性化.................................................... 1
0.2 數理邏輯求助數學——符號化.................................................... 2
0.3 數理邏輯追隨數學——公理化.................................................... 3
0.4 數理邏輯改造數學——形式化.................................................... 4
0.5 數理邏輯與計算機科學.............................................................. 6
0.6 本章小結.................................................................................. 7
0.7 習題................................................................................ 8
第1 章集合論基礎：概念與運算........................................................... 9
1.1 集合的概念............................................................................. 9
1.2 集合運算............................................................................... 10
1.3 關系..................................................................................... 12
1.3.1 關系的基本概念.......................................................... 13
1.3.2 關系的基本運算.......................................................... 14
1.3.3 關系的特性................................................................. 16
1.3.4 等價關系.................................................................... 18
1.3.5 序關系....................................................................... 19
1.4 函數..................................................................................... 22
1.4.1 函數的基本概念及合成運算......................................... 22
1.4.2 單射、滿射和雙射....................................................... 24
1.4.3 函數的逆.................................................................... 25
1.5 本章小結................................................................................ 27
1.6 習題................................................................................. 27
第2 章集合論基礎：歸納................................................................... 29
2.1 集合的歸納定義..................................................................... 29
2.2 歸納法................................................................................... 32
2.2.1 結構歸納法................................................................. 32
2.2.2 歸納定義及歸納法在計算機科學中的應用....................................... 33
2.2.3 數學歸納法............................................................................. 37
2.3 本章小結.............................................................................. 39
2.4 習題................................................................................. 39
第3 章命題演算.............................................................................. 41
3.1 命題演算基本概念........................................................... 41
3.1.1 命題與聯結詞............................................................ 41
3.1.2 命題公式及其真值.......................................................... 43
3.1.3 範式...................................................................... 46
3.1.4 聯結詞的擴充與規約............................................................... 48
3.2 命題演算形式系統PC ......................................................... 51
3.2.1 PC 系統的組成...................................................... 51
3.2.2 PC 中的推理.............................................................. 51
3.2.3 PC 的語義.................................................................... 54
3.2.4 關於PC 的重要元定理................................................................... 54
3.3 命題演算形式系統ND .............................................................. 58
3.4 本章小結................................................................................. 64
3.5 習題..................................................................................... 64
第4 章一階謂詞演算......................................................................... 66
4.1 一階謂詞演算基本概念........................................................... 66
4.1.1 個體、謂詞和函詞......................................................66
4.1.2 變元和常元..................................................................... 68
4.1.3 量詞...................................................................... 69
4.1.4 謂詞公式.................................................................... 69
4.1.5 公式的真值............................................................... 71
4.2 一階謂詞演算形式系統FC ..................................................... 75
4.2.1 一階語言................................................................. 75
4.2.2 一階邏輯.................................................................... 77
4.3 FC 的語義............................................................................... 82
4.4 關於FC 的重要元定理................................................................ 84
4.4.1 FC 的合理性及其他......................................................... 84
4.4.2 FC 的完備性及其他....................................................... 85
4.4.3 FC 的半可判定性............................................................ 89
4.5 一階謂詞演算自然推理系統FND ........................................... 90
4.6 本章小結................................................................................. 94
4.7 習題............................................................................ 94
第5 章帶等詞的一階謂詞演算............................................................. 97
5.1 等詞公理.............................................................................. 97
5.2 帶等詞一階系統的語義........................................................ 99
5.3 群論......................................................................... 103
5.4 公理化集合論.................................................................... 107
5.5 一階算術理論................................................................... 111
5.5.1 一階算術系統組成....................................................... 111
5.5.2 一階算術系統的模型.......................................................... 112
5.5.3 皮亞諾公設.................................................................. 113
5.6 帶等詞的自然推理系統....................................................... 114
5.7 本章小結........................................................................... 115
5.8 習題................................................................................. 115
第6 章消解原理........................................................................... 117
6.1 命題演算的消解原理........................................................... 117
6.1.1 文字、子句和子句集.............................................................. 117
6.1.2 消解證明.............................................................. 118
6.2 Skolem 化............................................................... 122
6.2.1 前束範式............................................................. 123
6.2.2 Skolem 標準形......................................................... 125
6.2.3 子句集................................................................... 127
6.3 合一.................................................................................. 128
6.3.1 代換....................................................................... 128
6.3.2 合一基本概念........................................................ 130
6.3.3 合一算法................................................................ 132
6.4 一階謂詞演算的消解原理................................................... 135
6.5 消解原理的完備性............................................................ 138
6.5.1 Herbrand 結構............................................................. 138
6.5.2 Herbrand 定理................................................................ 142
6.5.3 完備性定理的證明.......................................................... 144
6.6 本章小結.................................................................. 147
6.7 習題.................................................................................. 147
第7 章程序邏輯.............................................................................. 150
7.1 程序邏輯簡介..................................................................... 150
7.2 程序規約.......................................................................... 151
7.2.1 命令式編程語言WHILE ............................................. 152
7.2.2 斷言與規約.............................................................. 153
7.2.3 程序的部分正確性與完全正確性.................................................... 155
7.3 Hoare 邏輯系統................................................................... 156
7.3.1 系統組成................................................................. 156
7.3.2 完全正確性的證明.......................................................... 163
7.4 Hoare 邏輯語義及性質............................................................. 165
7.4.1 WHILE 語言語義......................................................... 166
7.4.2 Hoare 三元組語義....................................................... 168
7.4.3 關於Hoare 邏輯的重要元定理....................................................... 168
7.5 Hoare 邏輯的擴展................................................................ 178
7.5.1 對for 循環的擴展.......................................................... 178
7.5.2 對數組的擴展.............................................................. 180
7.6 分離邏輯............................................................................. 181
7.6.1 共享可變數據結構.......................................................... 182
7.6.2 小堆模型、分離邏輯聯結詞、斷言................................................ 183
7.6.3 堆操作命令及語義............................................................ 186
7.6.4 公理與推理規則.............................................................. 188
7.6.5 鏈表反轉程序的證明.................................................................... 190
7.7 自動程序驗證......................................................................... 192
7.8 Dafny .................................................................. 194
7.8.1 程序與規約：一個例子................................................................. 194
7.8.2 謂詞、假設和定理............................................................ 197
7.8.3 可終止性證明............................................................ 202
7.9 本章小結.......................................................................... 205
7.10 習題................................................................................. 205
第8 章模型檢測................................................................... 207
8.1 遷移系統......................................................................... 208
8.2 線性時序邏輯LTL ............................................................ 216
8.2.1 LTL 語法................................................................... 216
8.2.2 LTL 語義............................................................... 217
8.2.3 重要的LTL 等價式...................................................... 219
8.3 分支時序邏輯CTL .................................................................. 222
8.3.1 CTL 語法................................................................. 222
8.3.2 CTL 語義................................................................ 224
8.3.3 重要的CTL 等價式...................................................................... 227
8.3.4 CTL 與LTL 表達能力比較............................................................ 230
8.4 安全性、活性及公平性.......................................................... 230
8.5 模型檢測算法..................................................................... 234
8.5.1 LTL 模型檢測............................................................... 235
8.5.2 CTL 模型檢測............................................................ 253
8.6 Spin .............................................................................. 261
8.6.1 Promela .............................................................. 262
8.6.2 互斥訪問算法驗證................................................. 265
8.7 本章小結............................................................ 274
8.8 習題........................................................................... 274
參考文獻.................................................................... 276
