内容简介
本书对计算机科学方面的数理逻辑进行了综合介绍，涵盖命题逻辑、谓词逻辑、模态逻辑与代理、二叉判定图、模型检测和程序验证等内容。
目录
译者序
第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
前言/序言
第2版前言Logic in Computer Science：Modelling and Reasoning about Systems,Second Edition
本书的（重新）写作动机
本书第1版的写作主旨之一来自于以下观察：在计算机系统的设计、规范描述和验证中使用的大多数逻辑基本上都是处理一个满足关系 M ╞ φ
其中M是某种场景或系统的模型，而 φ 是一个规范，该逻辑的一个公式用来描述在场景M中什么应该是真的。这种结构的核心在于：我们可以经常规范并实现计算 ╞ 的算法。我们为命题逻辑、一阶逻辑、时态逻辑、模态逻辑和程序逻辑发展了这个主题。基于我们所收到的来自五大洲读者的鼓励性反馈，我们很高兴出版本书的第2版，本版遵循了第1版的原始主旨并有所改进。
新增的内容和删除的内容
第1章讨论关于完全命题逻辑的SAT求解器(与St?lmarck方法［SS90］类似的一种标记算法)的设计、正确性和复杂性。
第2章包含了模型论的基本结论(紧致性定理和L?wenheim-Skolem定理)，关于传递闭包和存在式及全称式二阶逻辑表达能力的一节，以及关于对象建模语言Alloy及其分析器(用于说明及探索未规范化的一阶逻辑模型的性质,这种性质是用带有传递闭包的一阶逻辑语言书写的)使用的一节。Alloy语言编写的程序是可执行的，使得这个说明及探索过程成为交互的和形式化的。
第3章已经完全重新组织了。这章的开始讨论线性时态逻辑，彻底概述了开放源码程序NuSMV模型检测工具的特性，并且包括规划问题的讨论，增加了关于时态逻辑表达能力的材料，以及新的建模实例。
第4章包含更多关于完全正确性证明的材料，以及关于验证程序正确性的合同编程范例的一节。
第5章和第6章也进行了修订，做了很多小的改动和订正。
各章之间的依赖关系和预备知识
本书要求学生了解初等数学的基础知识和朴素集合论概念和记号。第1章的核心材料(除1.4.3节到1.6.2节以外的所有内容)是其后的所有章节的基础。除此之外，只有第6章依赖于对第3章以及对第2章中静态范围规则的基本理解，尽管如此，即使完全不看第3章，也可以容易地读懂6.1节和6.2节的内容。各章的大致依赖关系如下图所示：
WWW支持
本书的Web支持站点包含：勘误表、所有程序代码的文本文件、辅助技术资料和链接、所有图形、基于多项选择题的交互式指导以及教师获得书中带有*号练习题答案的详细办法。本书支持站点的URL是www.cs.bham.ac.uk/research/lics/，也可以访问www.cambridge.org/052154310x。
