数理逻辑是计算机科学的基础之一，在模型与系统的规约与验证等方面有着广泛的应用。随着当今软硬件产品 (电路、程序和通信协议等) 日趋复杂，数理逻辑已经成为越来越多设计开发人员的日常工具。本书适合作为高等院校计算机及相关专业的数理逻辑/形式化方法课程教材，涵盖了命题逻辑、谓词逻辑、模态逻辑与Agent、二元决策图、模型检查和程序验证等内容。与传统数理逻辑教科书相比，它的主要特色就是紧紧围绕软硬件规约和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性 (SAT) 算法、紧致性理论和L?enheim-Skolem定理，并介绍了Alloy语言和NuSMV工具。
　　本书自出版以来受到广泛好评，已经被包括美国普林斯顿大学、卡内基-梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰Vrije大学、印度理工学院在内的多个国家几十所高校采纳为教材。

无

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

1. Propositional logic;
2. Predicate logic;
3. Verification by model checking;
4. Program verification;
5. Modal logics and agents;
6. Binary decision diagrams;
Bibliography;
Index.