合取範式

在布爾邏輯中，如果一個公式是子句的合取，那麼它是合取範式（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})$

參見

• 析取範式
• 代數範式
• 霍恩子句
• 奎因－麥克拉斯基算法

外部連結

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