程序验证（一）：命题逻辑

概念

命题逻辑

例如 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 ⊭ F I\not \models F I⊨F	assum.
2	I ⊨ P ∧ Q I\models P\wedge Q I⊨P∧Q	1 and → \to →
3	I ⊭ P ∨ ¬ Q I\not\models P\vee\neg Q I⊨P∨¬Q	1 and → \to →
4	I ⊨ P I\models P I⊨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 算法.