译者序
第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.
鄂公网安备 42010302001612号 