程序验证（一）：命题逻辑
概念
命题逻辑
例如 P ∨ ¬ Q → R P\vee \neg Q \to R P∨¬Q→R
- 一个原子(atom)是一个或为真或为假的判断。
- 一个文字(literal)是一个原子或它的非。
- 命题公式(propositional formulas)由文字和逻辑连接符组成。
合式公式
合式公式(well-formed formulas) 由以下语法得到：
- a t o m \langle atom\rangle atom ::= ⊤ ( t r u e ) ∣ ⊥ ( f a l s e ) ∣ P , Q , . . . ( 命 题 变 量 ) \top (true) | \bot (false)|P,Q, ... (命题变量) ⊤(true)∣⊥(false)∣P,Q,...(命题变量)
- l i t e r a l \langle literal\rangle literal::= a t o m \langle atom\rangle atom| ¬ \neg ¬ a t o m \langle atom\rangle atom（非）
- f o r m u l a \langle formula\rangle formula::= l i t e r a l \langle literal\rangle literal
| ¬ \neg ¬ f o r m u l a \langle formula\rangle formula (negation)
| f o r m u l a \langle formula\rangle formula ∧ \wedge ∧ f o r m u l a \langle formula\rangle formula (conjunction)
| f o r m u l a \langle formula\rangle formula ∨ \vee ∨ f o r m u l a \langle formula\rangle formula (disjunction)
| f o r m u l a \langle formula\rangle formula → \to → f o r m u l a \langle formula\rangle formula (implication)
| f o r m u l a \langle formula\rangle formula ↔ \leftrightarrow ↔ f o r m u l a \langle formula\rangle formula (equivalence)
举例：
| 公式 | 是否为合式公式 |
|---|---|
| ⊤ \top ⊤ | 是 |
| P ∧ ( Q ∨ R → P ) P\wedge (Q \vee R\to P) P∧(Q∨R→P) | 是 |
| P P P | 是 |
| P ⇒ Q P\Rightarrow Q P⇒Q | 否 |
语义
目的：给命题逻辑赋予涵义
把布尔值赋值给（公式，解释）对
即
F o r m u l a : F + I n t e r p r e t a t i o n : I = T r u t h V a l u e ( t r u e , f a l s e ) Formula: F + Interpretation: I=TruthValue(true, false) Formula:F+Interpretation:I=TruthValue(true,false)
什么是解释？
对于一个命题公式 F F F，一个解释 I I I将 F F F中每个命题变元映射为一个布尔值，也就是说：
I = P ↦ t r u e , Q ↦ f a l s e , R ↦ f a l s e , . . . I={P\mapsto true, Q\mapsto false, R\mapsto false,...} I=P↦true,Q↦false,R↦false,...
满足解释：
如果命题公式在解释 I I I下值为真，那么说 I I I是 F F F的满足解释(satisfying interpretation)，记作：
I ⊨ F I \models F I⊨F
不满足解释：
如果命题公式在解释 I I I下值为假，那么说 I I I是 F F F的不满足解释(falsifying interpretation)，记作：
I ⊭ F I \not \models F I⊨F
语义的归纳定义：
首先定义原子的涵义，然后根据这些定义，定义每个逻辑连接的涵义。
举例：
F : P ∧ Q → P ∨ ¬ Q F: P\wedge Q \to P\vee \neg Q F:P∧Q→P∨¬Q
I : { P ↦ t r u e , Q ↦ f a l s e } I:\{P\mapsto true,Q\mapsto false\} I:{P↦true,Q↦false}
| Step No. | Step | Reason |
|---|---|---|
| (1) | I ⊨ P I\models P I⊨P | I [ P ] = t r u e I[P]=true I[P]=true |
| (2) | I ⊭ Q I\not\models Q I⊨Q | I [ Q ] = f a l s e I[Q]=false I[Q]=false |
| (3) | I ⊨ ¬ Q I\models\neg Q I⊨¬Q | ( 2 ) a n d ¬ (2) and \neg (2)and¬ |
| (4) | I ⊭ P ∧ Q I\not\models P\wedge Q I⊨P∧Q | ( 2 ) a n d ∧ (2) and \wedge (2)and∧ |
| (5) | I ⊨ P ∧ Q → P ∨ ¬ Q I\models P\wedge Q\to P\vee \neg Q I⊨P∧Q→P∨¬Q | ( 4 ) a n d → (4) and \to (4)and→ |
可满足性与永真性
一个公式 F F F是可满足的(satisfiable)当且仅当存在一个解释 I I I使得 I ⊨ F I\models F I⊨F。
一个公式 F F F是永真的(valid)当且仅当对于所有解释 I I I， I ⊨ F I\models F I⊨F。
注意：可满足性与永真性是成对的(dual)符号，即 F F F是永真的当且仅当 ¬ F \neg F ¬F是不可满足的。
如何证明可满足性？
- 真值表穷举：蛮力搜索复杂度为 2 n 2^n 2n，其中 n n n为变元的数量
- 演绎推理：语义讨论
- 假定 F F F为非永真的，即存在 I I I， I ⊭ F I\not \models F I⊨F
- 应用推理规则
- 如果每一分支都得到矛盾，那么 F F F是永真的
- 如果没有矛盾，且不能进一步应用推理规则，那么 F F F是非永真的
语义规则
公式
I ⊨ ¬ F I ⊭ F \frac{I\models \neg F}{I\not \models F} I⊨FI⊨¬F
I ⊭ ¬ F I ⊨ F \frac{I\not \models \neg F}{I\models F} I⊨FI⊨¬F
I ⊨ F ∧ G I ⊨ F I ⊨ G \frac{I\models F\wedge G}{I\models F ~ I\models G} I⊨F I⊨GI⊨F∧G
I ⊭ F ∧ G I ⊭ F ∣ I ⊭ G \frac{I\not\models F\wedge G}{I\not \models F | I\not\models G} I⊨F∣I⊨GI⊨F∧G这个规则产生了分支
I ⊨ F ∨ G I ⊨ F ∣ I ⊨ G \frac{I\models F\vee G}{I\models F | I\models G} I⊨F∣I⊨GI⊨F∨G
I ⊭ F ∨ G I ⊭ F I ⊭ G \frac{I\not\models F\vee G}{I\not\models F~I\not \models G} I⊨F I⊨GI⊨F∨G
I ⊨ F → G I ⊭ F ∣ I ⊨ G \frac{I\models F\to G}{I\not\models F | I\models G} I⊨F∣I⊨GI⊨F→G
I ⊭ F → G I ⊨ F I ⊭ G \frac{I\not\models F\to G}{I\models F~I\not\models G} I⊨F I⊨GI⊨F→G
I ⊨ F ↔ G I ⊨ F ∧ G ∣ I ⊨ ¬ F ∧ ¬ G \frac{I\models F\leftrightarrow G}{I\models F\wedge G|I\models \neg F\wedge \neg G} I⊨F∧G∣I⊨¬F∧¬GI⊨F↔G
I ⊭ F ↔ G I ⊨ F ∧ ¬ G ∣ I ⊨ ¬ F ∧ G \frac{I\not \models F\leftrightarrow G}{I\models F\wedge \neg G|I\models \neg F\wedge G} I⊨F∧¬G∣I⊨¬F∧GI⊨F↔G
举例
- F : P ∧ Q F: P\wedge Q F:P∧Q
| 步骤 | 推理 | 备注 |
|---|---|---|
| 1 | I ⊭ P ∧ Q I\not\models P\wedge Q I⊨P∧Q | assumption |
| 2 | $I\not\models P | 1 and ∧ \wedge ∧, case A |
| 3 | $I\not\models Q | 1 and ∧ \wedge ∧, case B |
- F : P ∧ Q → P ∨ ¬ Q F: P\wedge Q \to P\vee \neg Q F:P∧Q→P∨¬Q
| 步骤 | 推理 | 备注 |
|---|---|---|
| 1 | $I\not \models F | assum. |
| 2 | I ⊨ P ∧ Q I\models P\wedge Q I⊨P∧Q | 1 and → \to → |
| 3 | $I\not\models P\vee\neg Q | 1 and → \to → |
| 4 | $I\models P | 2 and ∧ \wedge ∧ |
| 5 | I ⊭ P I\not\models P I⊨P | 3 and ∨ \vee ∨ |
| 6 | $\bot | 4 and 5 |
发现矛盾，所以 F F F是永真的。
注意： ⇒ \Rightarrow ⇒这样的双线箭头不属于命题逻辑的符号集。
范式(Normal Forms)
概念
一种逻辑的范式，应当：
- 限制公式的语法(Restricts the syntax of formulas)
- 对于此逻辑中的任意公式，范式具有等价的表达能力(Has equivalent representation for any formula in the logic)
三种主要范式
Negation Normal Form (NNF)
只包含 ∧ \wedge ∧， ∨ \vee ∨， ¬ \neg ¬三个符号，且 ¬ \neg ¬只能用于文字(literal)
Disjunctive Normal Form (DNF)
合取子句的析取
Conjunctive Normal Form (CNF)
析取子句的合取
举例：
| 命题 | 是否正确 |
|---|---|
| ¬ P ∧ ¬ ( P ∨ Q ) \neg P\wedge\neg(P\vee Q) ¬P∧¬(P∨Q)是NNF | 否 |
| ¬ P ∧ ¬ Q ∨ R \neg P\wedge\neg Q\vee R ¬P∧¬Q∨R是DNF | 是 |
| ( ¬ P ∨ Q ) ∧ ( P → R ) (\neg P\vee Q)\wedge (P\to R) (¬P∨Q)∧(P→R)是CNF | 否 |
| ¬ P ∧ P \neg P\wedge P ¬P∧P是CNF | 是 |
范式转化
由于主流的SAT solver（就是一个程序，输入一个公式，输出这个公式是否是可满足的，例子见一个简单的DPLL实现）一般接受CNF为输入，所以面对一个一般的公式，我们需要先把它转化为一个CNF。如何实现？等价的转换比较困难，但是我们可以采用一种逻辑上更弱的方法，即进行可满足性等价(equisatisfiability)转换。也就是说，我不要求转换后的CNF与原来的公式在所有的解释下真值都一样，我只要求若CNF可满足，则原公式可满足；若原公式可满足，则CNF可满足。
转换的方法，可采用Tseitin 算法.
