面向计算机科学的数理逻辑系统建模与推理

这是一本把数理逻辑'用起来'的书。它不满足于讲清命题逻辑、谓词逻辑、模态逻辑的推演规则，而是始终追问一个实务问题：这些形式化工具如何真正落到软硬件的规约与验证上。模型检查、二元决策图、程序验证、可满足性算法，乃至 Alloy 与 Nusmv 这类工具，都被安排进'设计开发人员的日常'这一语境里，而非孤立的理论章节。正因如此，它被不少导师列为实验室新人的入门首选，也被读者评为对新手友好、入门全面清晰之作。当然，也有声音提醒它'技术偏旧'、'发散性不足，需要老师带'——这恰是它的定位：不是供人闲逛的思想随笔，而是一条被精心规划、指向工程落地的入门路径。