• 引入
• CNF & DNF
• PNF
• Transformation to Prenex Normal Forms
• Examples
• References

• 引入

说到逻辑运算，最基本的就是与或非了。

AND	合取	∧
OR	析取	∨
NOT	非	┐

考虑下面这个数学式，其中A，B为有理数

A + B

那么我们一看就知道这是一个加法式。我们也知道，因为A，B是有理数，所以A，B可以分别写为两个整数的比值：

A = A₁/A₂
B = B₁/B₂

其中A₂，B₂都是非零整数，且上面两个分式都是既约分数。因为A₂，B₂都是非零整数，所以1/A₂，1/B₂也为 非零有理数，我们令

1/A₂ = A₃
1/B₂ = B₃

那么A和B就可以写为两个有理数的乘积，

A = A₁ * A₃
B = B₁ * B₃

现在，我们的式子就变成了

A₁ * A₃ + B₁ * B₃

这里面包含了乘法和加法，不过这个式子最终还是加法，因为我们可以做如下变形

(A₁ * A₃) + (B₁ * B₃)

Note：此时不能将A₁替换为(A₁₁ + A₁₂)。即对于每一个+，它的两个操作数可以是常数或表达式，如果是表达式的话，表达式内只允许*。也就是说，这里如果将A₁替换为另外两个数的乘积的话，是允许的。那么为什么要定义这个规则呢？因为我们就是想要这种形式的表达式。之后提到的CNF与DNF均有类似规则，

有了这个之后，我们可以推广出对于

X₁ + X₂ + ... + X_n

我们可以写成

(X₁₁ * X₁₂) + (X₂₁ * X₂₂) + ... + (X_n1 * X_n2)

这里面也包含了乘法和加法，同样的，这个式子最终还是加法。

对于乘法式A * B（其中A，B为有理数），我们有类似的变换，只需将A写作(A₁ + A₂)，将B写作(B₁ + B₂)即可。

P.S:
对于上面的内容，可以通过lisp来思考，我们是将

(+ A B)

写为了

(+
    (* A1 A3)
    (* B1 B3)
)

显然，外层为加法

 

• CNF & DNF

下面介绍CNF与DNF。

CNF即Conjunctive normal form，合取范式
DNF即Disjunctive normal form，析取范式

我们可以将合取考虑为*，析取考虑为+。则CNF就是以∧为主，而DNF是以∨为主。

这里我们就以CNF为例子。考虑如下逻辑表达式，其中P，Q为非原子命题

P ∧ Q

因为P，Q为非原子命题，我们假设P，Q可写为

P = P₁ ∨ P₂
Q = Q₁ ∨ Q₂

那么原来的逻辑表达式就变为了

(P₁ ∨ P₂) ∧ (Q₁ ∨ Q₂)

同样的，我们也可以用lisp来思考这一过程（不过这里只是借用了lisp语言的形式），将

(∧ P Q)

写为

(∧
    (∨ P1 P2)
    (∨ Q1 Q2)
)

如果你还记得刚才的Note的话，那么你应该知道这里的P₁不能写为(P₁₁ ∧ P₁₂)了。对于CNF，这条规则的准确描述是，

若干个互不相同的析取项的合取称为一个合取范式

相应的，DNF的规则就是

若干个互不相同的合取项的析取称为一个析取范式

• PNF

PNF即Prenex Normal Forms，前束范式。

考虑如下形式的式子，其中Q₁，Q₂，...，Q_n是量词，A为命题公式。

Q₁Q₂...Q_nA

在这里，Q₁Q₂...Q_n被称为前缀，而A则是前束范式的矩阵（the matrix of prenex form）
同样的，前束范式与CNF和DNF有类似的规则，比如

∀_x∃_y(x > 0 → (y > 0 ∧ x = y²))
对于所有大于0的x都存在大于0的y可以使得x=y²成立。

就是前束范式。

而

∃_x(x = 0) ∧ ∃_y(y > 0)
∀_x(x > 0 ∨ ∃_y(y > 0 ∧ x = y²))

都不是前束范式。

如果在一个PNF中，A是CNF的话，这个PNF可以具体称为PCNF，前束合取范式；如果A是DNF的话，则为PDNF，前束析取范式。

• Transformation to Prenex Normal Forms

算法如下，

1. 消去所有出现的if和iff
2. 否定深入
3. 等价变换
    (a) ∀_xP ∧ ∀_xQ ≡ ∀_x(P ∧ Q)
    (b) ∃_xP ∨ ∃_xQ ≡ ∃_x(P ∨ Q)
在必要的时候使用换名规则
4. 扩张量词的辖域（可以理解为编程语言中的作用域）
    (c) ∀_xP ∧ Q ≡ Q ∧ ∀_xP ≡ ∀_x(P ∧ Q)
    (d) ∀_xP ∨ Q ≡ Q ∨ ∀_xP ≡ ∀_x(P ∨ Q)
    (e) ∃_xP ∧ Q ≡ Q ∧ ∃_xP ≡ ∃_x(P ∧ Q)
    (f) ∃_xP ∨ Q ≡ Q ∨ ∃_xP ≡ ∃_x(P ∨ Q)
5. 将A（前束范式的矩阵）变形为CNF或者DNF

• Examples

• 1. 用做例子的谓词公式如下

A = ∀_x(P(x) → ∃_y(Q(x, y)))

1. 消去所有出现的if和iff:

A ≡ ∀_x(¬P(x) ∨ ∃_y(Q(x, y)))

2. 因为否定已经直接作用在命题前面了，所以此题无需否定深入
3. 这道题也不需要等价变换或是换名
4. 扩张量词的辖域:

A ≡ ∀_x∃_y(¬P(x) ∨ Q(x, y))

5. 现在已经是PCNF了（将(¬P(x) ∨ Q(x, y))看成一个整体与1合取，即

∀_x∃_y(¬P(x) ∨ Q(x, y)) ∧ 1)

如果要写成PDNF的话，我们需要做如下变换(将矩阵变换为析取范式, 此时将¬P(x) ∨ Q(x, y)分开看)

A ≡ ∀_x∃_y((¬P(x) ∧ 1) ∨ (Q(x, y) ∧ 1))
A ≡ ∀_x∃_y((¬P(x) ∧ (¬Q(x, y) ∨ Q(x, y))) ∨ (Q(x, y) ∧ (¬P(x) ∨ P(x))))
A ≡ ∀_x∃_y(((¬P(x) ∧ ¬Q(x, y)) ∨ (¬P(x) ∧ Q(x, y))) ∨ ((Q(x, y) ∧ ¬P(x)) ∨ (Q(x, y) ∧ P(x))))
A ≡ ∀_x∃_y((¬P(x) ∧ ¬Q(x, y)) ∨ (¬P(x) ∧ Q(x, y)) ∨ (Q(x, y) ∧ P(x)))

---

 

 

• 2. 用做例子的谓词公式如下

A = ∀_xP(x) → ∃_xQ(x)

1. 消去所有出现的if和iff:

A ≡ ¬∀_xP(x) ∨ ∃_xQ(x)

2. 否定深入:

A ≡ ∃_x¬P(x) ∨ ∃_xQ(x)

3. 等价变换:

A ≡ ∃_x(¬P(x) ∨ Q(x))

---

 

 

3. 用做例子的谓词公式如下

A = ∃_z(∃_xQ(x, z) ∨ ∃_xP(x)) → ¬(¬∃_xP(x) ∧ ∀_x∃_zQ(z, x))

1. 消去所有出现的if和iff:

A ≡ ¬∃_z(∃_xQ(x, z) ∨ ∃_xP(x)) ∨ ¬(¬∃_xP(x) ∧ ∀_x∃_zQ(z, x))

2. 否定深入:

A ≡ ∀_z(¬∃_xQ(x, z) ∧ ¬∃_xP(x)) ∨ (¬¬∃_xP(x) ∨ ¬∀_x∃_zQ(z, x))
   ≡ ∀_z(∀_x¬Q(x, z) ∧ ∀_x¬P(x)) ∨ (∃_xP(x) ∨ ∃_x∀_z¬Q(z, x))

3. 等价变换:

A ≡ ∀_z∀_x(¬Q(x, z) ∧ ¬P(x)) ∨ ∃_x(P(x) ∨ ∀_z¬Q(z, x))

4. 应用换名规则:

A ≡ ∀_z∀_x(¬Q(x, z) ∧ ¬P (x)) ∨ ∃_y (P (y) ∨ ∀_w ¬Q (w, y))

5. 扩张量词的辖域:

A ≡ ∀_z∀_x∃_y∀_w ((¬Q (x, z) ∧ ¬P (x)) ∨ P (y) ∨ ¬Q (w, y))

6. 我们得到了PDNF，我们也可以将它改写为PCNF

A ≡ ∀_z∀_x∃_y∀_w((¬Q(x, z) ∨ P(y) ∨ ¬Q(w, y)) ∧ (¬P(x) ∨ P(y) ∨
¬Q(w, y)))

• References

• First Order Logic: Prenex normal form. Skolemization. Clausal form