合取范式

维基百科,自由的百科全书
跳转至: 导航搜索

布尔逻辑中,一个公式合取范式(CNF)的,如果它是子句合取。作为规范形式,它在自动定理证明中有用。它类似于在电路理论中的规范和之积形式

所有的文字的合取和所有的文字的析取是 CNF 的,因为可以被分别看作一个文字的子句的合取和一个单一子句的合取。和析取范式(DNF)中一样,在 CNF 公式中可以包含的命题连结词是。非算子只能用做文字的一部分,这意味着它只能在命题变量前出现。

例如,下列所有公式都是 CNF:

A \wedge B
\neg A \wedge (B \vee C)
(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)
(\neg B \vee C)

而下列不是:

\neg (B \vee C)
(A \wedge B) \vee C
A \wedge (B \vee (D \wedge E))

上述三个公式分别等价于合取范式的下列三个公式:

\neg B \wedge \neg C
(A \vee C) \wedge (B \vee C)
A \wedge (B \vee D) \wedge (B \vee E)

所有命题公式都可以转换成 CNF 的等价公式。这种变换基于了关于逻辑等价的规则: 双重否定律德·摩根定律分配律

因为所有逻辑公式都可以转换成合取范式的等价公式,证明经常基于所有公式都是 CNF 的假定。但是在某些情况下,这种到 CNF 的转换可能导致公式的指数性爆涨。例如,把下述非-CNF 公式转换成 CNF 生成有 2^n 个子句的公式:

(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n)

参见[编辑]

外部链接[编辑]