跳至內容

析取範式

維基百科,自由的百科全書

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

但如下公式不是 DNF:

NOT 是最外層的算子
一個 OR 嵌套在一個 AND 中

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

參見