前言

这是一本关于数理逻辑基础理论及其在形式化验证方向应用的教材。数

理逻辑是计算机科学的重要基础理论。近年来，以数理逻辑系统为严格数学基

础的形式化方法、技术与工具取得了长足进展，涌现出以编译器、操作系统内

核验证为代表的成功应用案例，在提高软件/硬件可靠性方面展现出无可替代

的潜力。随着人工智能和自动化技术的飞速发展，数理逻辑的应用领域也在不

断拓展。随着逻辑证明自动化和形式化验证技术的进步，未来软件/硬件系统

的可靠性有可能出现大幅提升。

掌握数理逻辑的基础理论，了解形式化方法相关技术和工具，有意识地使

用严格的数学方法对计算机软件/硬件进行建模和验证，对培养软件/硬件方向

的专门人才、提高其技术工作能力和专业发展潜力具有重要意义，也是技术发

展大势所趋。更为重要的是，在大语言模型不断迭代升级、能力一日千里的当

下，学生甚至专业程序员依赖人工智能生成代码已成为常态，但无法消除的模

型“幻觉”（如逻辑错误、虚构“事实”等）易埋下隐患。经过系统学习数理

逻辑和形式化方法训练所获得的严谨细致的推理能力和思维习惯，将是对抗人

工智能不确定性的“良药”。

传统上数理逻辑教材偏重介绍基础理论，鲜少涉猎计算机科学方面的应

用，数学味较浓。对于计算机学科方向的读者，在了解数理逻辑的经典系统和

理论之外，更渴望提高应用形式化方法技术的能力。为此，亟须一本兼顾理论

基础与形式化方法应用的教材。

本教材在内容选择和行文风格上努力做到三个平衡。

（1）基础与应用平衡。基础方面，通过完整介绍命题、谓词等形式演算系

统及其性质，使读者不仅熟悉数理逻辑的经典理论，还熟悉其一般研究方法。

应用方面，透过程序逻辑、模型检测等主题，使读者了解基于逻辑的软件/硬件

验证主流方法与技术，并通过代表性工具软件学习使用，具备初步实践能力。

（2）深度和广度平衡。深度适中，对经典逻辑系统、程序逻辑和模型检测

等内容进行完整讨论，通过证明形式系统的合理性、完备性等性质，训练严密

的数学思维和推理能力。避免过深过难，舍弃以哥德尔不完全定理为代表的数

理逻辑高阶内容。追求一定的广度，简要介绍基于一阶谓词演算的几个经典数

学理论，梳理软件验证方面有代表性的算法和工具环境，扩大知识面。

（3）严谨性和易读性平衡。文字表述严谨、尽力避免歧义和含糊，同时语

言朴实直白、解释到位、例子丰富，便于读者自学。

本教材内容分为三部分，按知识发展脉络展开：第一部分（第1、2 章）为基础知识，涵

盖集合、关系、函数、归纳等基本知识点，奠定学习基础；第二部分（第36 章）介绍数

理逻辑经典理论，包括命题演算、一阶谓词演算、消解原理以及基于一阶谓词演算的几个

经典数学理论；第三部分（第7、8 章）介绍数理逻辑在软件/硬件验证方面的应用与发展，

包括程序逻辑、模型检测等，也包括相关方法与工具的介绍。编者之间的分工是：韩敬利

负责第1、2 章的编写，王兆丽负责第3、4 章的编写，宋丽华负责第58 章的编写，王元元

负责内容体系设计以及第0 章绪论的编写，夏青负责课后习题设计。

本教材面向计算机大方向学生，尤其是软件工程方向的高年级本科生和硕士研究生。

除作为数理逻辑课程教材使用外，也可供各高校相关课程使用或从事相关方向工作的人员

阅读。本教材具有自含性，不要求离散数学等前修课程。

由于编者水平有限，编写过程中难免出现笔误错漏。欢迎读者积极反馈意见，我们将

在后续版本中进行订正。

编者

2026 年2 月