命题逻辑与谓词逻辑：从基础到推理
逻辑，说白了就是形式化验证的“语法”。你想想看，我们要用工具去证明一个系统是对的，总得先有一套大家都懂的语言吧？命题逻辑和谓词逻辑就是这套语言的基础。我个人习惯把命题逻辑看作是“开关逻辑”，而谓词逻辑则是“带参数的开关逻辑”。
命题逻辑基础
命题是什么？就是一个能判断真假的陈述句。比如“今天下雨了”，要么真要么假，没有中间态。在形式化验证里，我们经常用命题来表示系统的状态。
举个例子，我在项目中验证过一个简单的门控电路：
// 命题逻辑表示
P: 时钟信号为高
Q: 使能信号有效
R: 输出信号为高
// 逻辑表达式
R = P ∧ Q // 输出为高当且仅当时钟为高且使能有效这里有几个基本操作符，你得记住：
- ¬（非）：取反，真变假，假变真
- ∧（与）：两个都真才真
- ∨（或）：一个真就真
- →（蕴含）：如果P则Q，注意这个容易搞混
- ↔（等价）：两个命题同真同假
避坑指南：我曾经在写验证脚本时，把蕴含（→）和等价（↔）搞混了。蕴含的意思是“如果P成立，那么Q一定成立”，但P不成立时，这个式子依然为真。很多新手会在这里栽跟头。
谓词逻辑基础
命题逻辑有个局限——它只能处理完整的句子。比如“x大于5”，在命题逻辑里你没法表达“x”这个变量。这时候就需要谓词逻辑了。
谓词逻辑引入了两个核心概念：
- 谓词：比如 P(x) 表示“x是正数”
- 函数：比如 f(x) 表示“x的平方”
我习惯把谓词理解成“带参数的函数，返回值是真假”。比如：
// 谓词定义
Even(x): x是偶数
Prime(x): x是质数
// 用谓词表达命题
Even(4) → True
Prime(4) → False个人经验：在写形式化规约时，我建议把谓词命名得尽量语义化。比如用 isValidAddress(addr) 而不是 VA(addr)，这样三个月后你自己回来看代码还能看懂。
量词与约束
量词是谓词逻辑的灵魂。两个核心量词：
- ∀（全称量词）：对所有x，P(x)成立
- ∃（存在量词）：存在某个x，使得P(x)成立
你想想看，如果没有量词，我们怎么表达“所有中断请求都会被处理”？用命题逻辑你得枚举所有中断号，那得写到猴年马月去。
// 用量词表达
∀irq: IRQ_Type, isHandled(irq)
// 意思是：对所有类型为IRQ_Type的中断，它们都被处理了
∃buffer: Buffer, isEmpty(buffer)
// 意思是：存在一个缓冲区，它是空的这里有个容易踩的坑——量词的顺序。∀x ∃y 和 ∃y ∀x 完全不是一回事。我在验证一个多核缓存一致性协议时就吃过这个亏。
关键点：量词的作用域一定要搞清楚。比如 ∀x (P(x) → ∃y Q(x,y))，这里的y只在Q(x,y)里有效，出了这个括号就不认了。
逻辑等价与蕴含
这部分说白了就是“逻辑变形术”。两个公式逻辑等价，意味着它们在任何情况下真值都一样。常用的等价关系：
| 等价关系 | 形式 | 说明 |
|---|---|---|
| 双重否定 | ¬¬P ≡ P | 负负得正 |
| 德摩根律 | ¬(P∧Q) ≡ ¬P ∨ ¬Q | 与变或，取反 |
| 蕴含改写 | P→Q ≡ ¬P ∨ Q | 这个很实用 |
| 分配律 | P∧(Q∨R) ≡ (P∧Q)∨(P∧R) | 和代数分配律类似 |
逻辑蕴含则更强一些：如果P蕴含Q，那么只要P为真，Q必然为真。我在做形式化验证时，经常用蕴含来写“前提-结论”式的规约。
// 实际项目中的例子
// 前提：发送缓冲区非空
// 结论：数据会被发送
hasData(sendBuffer) → willSend(data)自然演绎推理
自然演绎，说白了就是“一步步推导出结论”。它模仿了人类自然的推理方式——从前提开始，用规则一步步推出新结论。
常用的推理规则：
- 假言推理：如果P→Q且P为真，则Q为真
- 拒取式：如果P→Q且Q为假，则P为假
- 全称实例化：从∀x P(x)推出P(a)
- 存在实例化：从∃x P(x)推出P(c)，c是新常量
我记得有一次调试一个并发锁的实现，就是用自然演绎一步步推导出死锁条件的。过程虽然繁琐，但每一步都清晰可见，最后定位到问题所在时，那种成就感真的很棒。
// 自然演绎示例
// 前提：
1. ∀x (Lock(x) → ¬Deadlock(x)) // 所有锁都不会死锁
2. Lock(mutex1) // mutex1是一个锁
// 推理：
3. Lock(mutex1) → ¬Deadlock(mutex1) // 全称实例化，从1推出
4. ¬Deadlock(mutex1) // 假言推理，从2和3推出
// 结论：mutex1不会死锁实用建议：刚开始学自然演绎时，我建议你像写数学证明一样，每一步都标注用了哪条规则、引用了哪个前提。这样即使推错了，也能快速回溯找到问题。
嗯，逻辑这部分内容确实有点抽象。但相信我，一旦你掌握了这些基础，后面学形式化验证工具就会顺畅很多。毕竟，工具只是把人的推理过程自动化了而已。