面向计算机科学的数理逻辑：系统建模与推理 原书第2版 pdf电子书[174MB]

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