目录
第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
