析合範式

析合範式(disjunctive normal form)亦稱析取範式一種析取式。是若干簡單合取式的析取式。

在布爾邏輯中，析取範式(DNF)是邏輯公式的標準化（或規範化），它是合取子句的析取。作為規範形式，它在自動定理證明中有用。一個邏輯公式被認為是 DNF 的，若且唯若它是一個或多個文字的一個或多個合取的析取。同合取範式（CNF）一樣，在 DNF 中的命題運算元是與、或和非。非運算元只能用做文字的一部分，這意味著它只能領先於命題變數。

下列公式都是 DNF:

但如下公式不是 DNF:

一個析取範式嵌套在一個 合取範式 中

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