析取範式

在布爾邏輯中，析取範式（DNF）是邏輯公式的標準化（或規範化），它是合取子句的析取。作為規範形式，它在自動定理證明中有用。一個邏輯公式被認為是 DNF 的，當且僅當它是一個或多個文字的一個或多個合取的析取。同合取範式（CNF）一樣，在 DNF 中的命題算子是與、或和非。非算子只能用做文字的一部分，這意味着它只能領先於命題變量。例如，下列公式都是 DNF:

$A\lor B$

$A\!$

$(A\land B)\lor C$

$(A\land \neg B\land \neg C)\lor (\neg D\land E\land F)$

但如下公式不是 DNF:

$\neg (A\lor B)$ NOT 是最外層的算子

$A\lor (B\land (C\lor D))$ 一個 OR 嵌套在一個 AND 中

把公式轉換成 DNF 要使用邏輯等價，比如雙重否定除去、德·摩根定律和分配律。注意所有邏輯公式都可以轉換成析取範式。但是，在某些情況下轉換成 DNF 可能導致公式的指數性爆漲。例如，在 DNF 形式下，如下邏輯公式有 2ⁿ 個項：

$(X_{1}\lor Y_{1})\land (X_{2}\lor Y_{2})\land \dots \land (X_{n}\lor Y_{n})$

參見

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