形式化5：否定范式NNF

范式NNF"/>

形式化5：否定范式NNF

NNF规约

否定范式具有如下的规定：

1. 否定仅出现在原子变量前
2. 没有蕴含符 → \to →

如下：

P : : = P ∣ ¬ P ∣ ⊤ ∣ ⊥ ∣ P ∨ P ∣ P ∧ P \begin{aligned} P ::&= P \\ &|\ \neg P \\ &|\ \top \\ &|\ \bot \\ &|\ P\lor P \\ &|\ P\land P \end{aligned} P::​=P∣ ¬P∣ ⊤∣ ⊥∣ P∨P∣ P∧P​

转化为NNF

C ( P ) = P C ( ∼ P ) = ∼ P C ( ∼ ∼ P ) = C ( P ) C ( P ∧ Q ) = C ( P ) ∧ C ( Q ) C ( P ∨ Q ) = C ( P ) ∨ C ( Q ) C ( ∼ ( P ∧ Q ) ) = C ( ∼ P ) ∨ C ( ∼ Q ) C ( ∼ ( P ∨ Q ) ) = C ( ∼ P ) ∧ C ( ∼ Q ) C ( P → Q ) = ∼ C ( P ) ∨ C ( Q ) \begin{aligned} C(P) &= P \\ C(\sim P) &= \sim P \\ C(\sim \sim P) &= C(P) \\ C(P\land Q) &= C(P)\land C(Q) \\ C(P\lor Q) &= C(P)\lor C(Q) \\ C(\sim (P\land Q)) &= C(\sim P)\lor C(\sim Q) \\ C(\sim (P\lor Q)) &= C(\sim P)\land C(\sim Q) \\ C(P \to Q) &= \sim C(P)\lor C(Q) \\ \end{aligned} C(P)C(∼P)C(∼∼P)C(P∧Q)C(P∨Q)C(∼(P∧Q))C(∼(P∨Q))C(P→Q)​=P=∼P=C(P)=C(P)∧C(Q)=C(P)∨C(Q)=C(∼P)∨C(∼Q)=C(∼P)∧C(∼Q)=∼C(P)∨C(Q)​

• 例题1

C ( p → ( q → p ) ) = ∼ C ( p ) ∨ ( q → p ) = ∼ p ∨ ( ∼ C ( q ) ∨ C ( p ) ) = ∼ p ∨ ( ∼ q ∨ p ) [ n n f − o k , b u t f u r t h e r ] = ∼ p ∨ p ∨ ∼ q = ⊤ \begin{aligned} C(p \to (q \to p)) &= \sim C(p) \lor (q \to p) \\ &= \sim p \lor (\sim C(q) \lor C(p)) \\ &= \sim p \lor (\sim q \lor p) \qquad [nnf-ok,\ but\ further] \\ &= \sim p \lor p \lor \sim q \\ &= \top \end{aligned} C(p→(q→p))​=∼C(p)∨(q→p)=∼p∨(∼C(q)∨C(p))=∼p∨(∼q∨p)[nnf−ok, but further]=∼p∨p∨∼q=⊤​

• 例题2

C ( ∼ ( ( p 1 ∧ ∼ p 2 ) ∨ ( p 3 ∨ ∼ p 4 ) ) ) = C ( ∼ ( p 1 ∧ ∼ p 2 ) ) ∧ C ( ∼ ( p 3 ∨ ∼ p 4 ) ) = ( C ( ∼ p 1 ) ∨ C ( ∼ ( ∼ p 2 ) ) ) ∧ ( C ( ∼ p 3 ) ∧ C ( ∼ ( ∼ p 4 ) ) ) = ( ∼ p 1 ∨ p 2 ) ∧ ( ∼ p 3 ∧ p 4 ) \begin{aligned} C&(\sim ((p1 \land \sim p2) \lor (p3 \lor \sim p4))) \\ &= C(\sim (p1 \land \sim p2)) \land C(\sim (p3 \lor \sim p4)) \\ &= (C(\sim p1) \lor C(\sim (\sim p2))) \land (C(\sim p3) \land C(\sim (\sim p4))) \\ &= (\sim p1 \lor p2) \land (\sim p3 \land p4) \end{aligned} C​(∼((p1∧∼p2)∨(p3∨∼p4)))=C(∼(p1∧∼p2))∧C(∼(p3∨∼p4))=(C(∼p1)∨C(∼(∼p2)))∧(C(∼p3)∧C(∼(∼p4)))=(∼p1∨p2)∧(∼p3∧p4)​