合取范式

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

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

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

${\displaystyle A\wedge B}$

${\displaystyle \neg A\wedge (B\vee C)}$

${\displaystyle (A\vee B)\wedge (\neg B\vee C\vee \neg D)\wedge (D\vee \neg E)}$

${\displaystyle (\neg B\vee C)}$

而下列不是:

${\displaystyle \neg (B\vee C)}$

${\displaystyle (A\wedge B)\vee C}$

${\displaystyle A\wedge (B\vee (D\wedge E))}$

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

${\displaystyle \neg B\wedge \neg C}$

${\displaystyle (A\vee C)\wedge (B\vee C)}$

${\displaystyle A\wedge (B\vee D)\wedge (B\vee E)}$

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

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

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n})}$

参见

• 析取范式
• 代数范式
• 霍恩子句
• 奎因－麦克拉斯基算法

外部链接

• Scheme and Ocaml programs for converting propositional logic statements into CNF