作为计算机及其相关专业的数理逻辑方面的教材，本书自出版以来受到了广泛的好评，世界许多著名大学（比如美国普林斯顿大学、卡内基-梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰Vrije大学、印度理工学院）都采用本书作为教材。
　　全书涵盖了命题逻辑、谓词逻辑、模态逻辑与代理、二叉判定图、模型检测和程序验证等内容。主要特色就是紧紧围绕软硬件规约和验证这一主题，反映计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性（SAT）算法、紧致性理论和lwenheim-Skolem定理，并介绍了Alloyy语言和NuSMV工具。
　　数理逻辑是计算机科学的基础之一，在模型与系统的规范与验证等方面有着广泛的应用。随着当今软硬件产品（电路、程序和通信协议等）日趋复杂，数理逻辑已经成为设计开发人员的日常工具。本书适合作为高等院校计算机及相关专业的数理逻辑/形式化方法课程的教材，也可供相关研究人员和专业人士参考。

无

本书的（重新）写作动机本书第1版的写作主旨之一来自于以下观察：在计算机系统的设计、规范描述和验证中使用的大多数逻辑基本上都是处理一个满足关系Euclid Math OneMApEuclid Math OneQBp其中Euclid Math OneMAp是某种场景或系统的模型，而是一个规范，该逻辑的一个公式，用来描述在场景Euclid Math OneMAp中什么应该是真的。这种结构的核心在于：我们可以经常规范并实现计算Euclid Math OneQBp的算法。我们为命题逻辑、一阶逻辑、时态逻辑、模态逻辑和程序逻辑发展了这个主题。基于我们所收到的来自五大洲读者的鼓励性反馈，我们很高兴出版本书的第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。

形式化方法的时代终于来临了! 规范描述语言、定理证明器以及模型检测器开始在工业中平常地使用。数理逻辑是所有这些技术的基础。直到现在，写给计算机科学家的逻辑教材还没有跟上硬件和软件规范与验证工具开发的脚步。例如，尽管模型检测在时序电路设计和通信协议验证方面获得了成功，但至今为止，我还没有看到任何一本适合本科生和低年级研究生的教材来尝试解释这种方法是如何工作的。因而，这些材料很少被教授给计算机科学家和电子工程师们，而在不久的将来，作为其工作的一部分他们会需要这些知识。相反，在一些形式化方法有可能真正获益的场合，工程师们却在尽量避免使用，或者抱怨形式化工具使用的概念和记号过于复杂而且不自然。这是很遗憾的，因为形式化方法背后的数学是相当简单的，肯定不比每个上微积分课的学生们必须要学习的那些数学分析概念更困难。
　　由MHuth和MRyan写的本书是一部很特别的著作。我第一次仔细阅读这本书时感到很惊讶。除了命题逻辑和谓词逻辑外，本书还对时态逻辑和模型检测进行透彻的讲解。事实上，本书突出的优点是包含如此之多的材料：线性与分支时态逻辑、显式状态模型检测、公平性、计算树逻辑(CTL)的基本不动点定理甚至还有二叉判定图和符号模型检测。此外，这些材料是以一种适合本科生和低年级研究生的程度来讲解的。书中提供了大量的问题和例子，以帮助学生掌握所讲授的材料。由于Huth和Ryan都是程序逻辑和程序验证方面非常活跃的研究者，他们的作品具有相当的权威。
　　总之，本书的材料是最新的、实用的，而且讲解精彩，是现代计算机科学逻辑教材的一个很好范例。我以最大的热情向读者推荐本书，并预期本书将获得巨大成功。

　　Edmund MClarke
　　卡内基梅隆大学
　　计算机科学FORE Systems教授

Michael Huth;Mark Ryan：Michael Huth: 伦敦帝国学院计算机系高级讲师，研究方向包括模型检测与抽象、程序分析和模型检测中有序结构的应用等。
Mark Ryan: 伯明翰大学计算机科学学院高级讲师，主要研究方向包括模型检测、时序及模态逻辑和非单调推理等。

何伟 樊磊：暂无简介

逻辑在计算机科学中的重要作用不言而喻,但传统的逻辑课本主要面向数学方面的读者。即使对应用有所涉及,也多仅谈及早期历史或某个专门方向的例子。正如为本书作序的Clarke所说,在近年出版的众多逻辑课本中,本书是一个例外。本书不但概要介绍了经典逻辑,而且介绍近年来非经典逻辑(程序逻辑、时态逻辑和模态逻辑等)在软件工程形式化方法特别是在模型检测与验证、知识工程、高效算法及实现等方面的现代应用,给人耳目一新的感觉。本书的选材和作为教材的特点在序言和前言中已有详述,被世界各国多所名校采纳为教材也充分说明了其价值,此处不需再叙。然而,由于国情及教学体系差别等方面的因素,本书中译本的使用范围可能会有所不同,可能更广泛、更灵活一些。我就自己在学习和翻译过程中的粗浅体会,谈谈本书的一些特点。
　　本书代表了欧美近年来十分流行的一种教科书写作风格,行文模仿教师的讲解与学生的对话,对理论背后的直觉、主要思想及方法做了极其详尽的(有时甚至是不厌其烦的)描述,辅之以丰富的实例和工业规模的系统实现来阐述理论结果和算法。从教学方面看,这种写作风格类似我国在20世纪50~60年代翻译出版的某些前苏联教材。这种风格一方面方便了各种程度的读者自学,但另一方面的确也有不符合国内教学现状的情况。举例来讲,本书前两章处理经典命题逻辑和谓词逻辑,篇幅约占全书三分之一以上。虽然起点很低(几乎从零开始),但实质内容偏少(相当我国大学本科离散数学课程所含的逻辑内容)。很多基本结果没有给出证明,直观背景的叙述略显冗长。此外，还有部分材料不太适合国内的教学需要，如本书(包括练习)讲解数学归纳法,却不加解释地使用了诸如等价关系、可计算性或复杂性等概念(尽管是非形式地使用)。虽然前面提到了本书的一些不足，但瑕不掩瑜，本书的优点还是非常突出的。全书的观点、体系、内容甚至习题都是相当现代化的,许多主题都是首次出现在本科生的逻辑教材中。此外,本书还详细介绍了几种较成熟的软件实现,为读者实践书中讲解的内容,了解现代形式化方法的应用情况都极有帮助。本书后面四章基本上是独立的,每章分别介绍一个主题,内容相对比较丰富,但不太系统,多是入门性的介绍和实例,少有形式化的理论和证明。综上所述,译者认为本书比较适合作为本科高年级选修课、毕业论文或其他小型研究项目的参考书或教材,若用于研究生课程则需补充相关的文献。
　　本书的叙述风格以及涉猎广泛的西方科学、技术和文化背景等给翻译工作带来了巨大困难，我们虽努力保持原书的语言风格,但由于文化背景上的差异以及译者水平的限制，中译本读起来可能会感觉有些“异样”,希望这不致降低本书的学术与使用价值。译者在使用本书过程中积累了一些教学辅助材料,包括与部分章节有关的幻灯片、动画和书中的全部插图(矢量格式),有兴趣的老师可通过电子邮件与译者直接联系(fanlei2002@sinacom),或通过华章网站(wwwhzbookcom)下载。
　　鉴于我们的学术和语言水平有限,译文中难免有不妥甚至错误之处,欢迎读者及专家批评指正。

　　樊磊
　　2007年4月

出版者的话
专家指导委员会
译者序
第1版序
第2版前言
第1章命题逻辑
11判断语句
12自然演绎
121自然演绎规则
122派生规则
123自然演绎总结
124逻辑等价
125侧记：反证法
13作为形式语言的命题逻辑
14命题逻辑的语义
141逻辑连接词的含义
142数学归纳法
143命题逻辑的合理性
144命题逻辑的完备性
15范式
151语义等价、满足性和有效性
152合取范式和有效性
153霍恩子句和可满足性
16SAT求解机
161线性求解机
162三次求解机
17习题
18文献注释
第2章谓词逻辑
21我们需要更丰富的语言
22作为形式语言的谓词逻辑
221项
222公式
223自由变量和约束变量
224代换
23谓词逻辑的证明论
231自然演绎规则
232量词的等价
24谓词逻辑的语义
241模型
242语义推导
243相等的语义
25谓词逻辑的不可判定性
26谓词逻辑的表达能力
261存在式二阶逻辑
262全称式二阶逻辑
27软件的微观模型
271状态机
272Alma重观
273软件的微模型
28习题
29文献注释
第3章通过模型检测进行验证
31验证的动机
32线性时态逻辑
321LTL的语法
322LTL的语义
323规范的实际模式
324LTL公式之间的重要等价
325LTL的适当连接词集
33模型检测: 系统、工具和性质
331例: 互斥
332NuSMV模型检测器
333运行NuSMV
334重温互斥
335摆渡者难题
336交错位协议
34分支时间逻辑
341CTL的语法
342计算树逻辑的语义
343规范的实际模式
344CTL公式间的重要等价
345CTL连接词的适当集
35CTL*与LTL和CTL的表达能力
351CTL中时态公式的布尔组合
352LTL中的过去算子
36模型检测算法
361CTL模型检测算法
362具有公平性的CTL模型检测
363LTL模型检测算法
37CTL的不动点特征
371单调函数
372SATEG的正确性
373SATEU的正确性
38习题
39文献注释
第4章程序验证
41为什么要规范和验证编码
42软件验证的一种框架
421一种核心程序设计语言
422霍尔三元组
423部分正确性和完全正确性
424程序变量和逻辑变量
43部分正确性的证明演算
431证明规则
432证明布景
433案例研究：最小和截段
44完全正确性的证明演算
45合同编程
46习题
47文献注释
第5章模态逻辑与代理
51真值的模式
52基本模态逻辑
521语法
522语义
53逻辑工程
531有效公式储备
532可达关系的重要性质
533对应理论
534一些模态逻辑
54自然演绎
55多代理系统中的知识推理
551一些例子
552模态逻辑KT45n
553KT45n的自然演绎
554例子的形式化
56习题
57文献注释
第6章二叉判定图
61布尔函数的表示
611命题公式和真值表
612二叉判定图
613有序BDD
62简约OBDD的算法
621算法reduce
622算法apply
623算法restrict
624算法exists
625OBDD的评价
63符号模型检测
631表示状态集合的子集
632表示迁移关系
633实现函数pre和pre
634综合OBDD
64关系μ演算
641语法和语义
642对CTL模型及规范说明的编码
65习题
66文献注释
参考文献