合取範式

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

布爾邏輯中,如果一個公式子句合取,那麼它是合取範式(CNF)的。作為規範形式,它在自動定理證明中有用。它類似於在電路理論中的規範和之積形式

所有的文字的合取和所有的文字的析取是 CNF 的,因為可以被分別看作一個文字的子句的合取和析取。和析取範式(DNF)中一樣,在 CNF 公式中可以包含的命題連結詞是。非算子只能用做文字的一部分,這意味著它只能在命題變量前出現。

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

而下列不是:

上述三個公式分別等價於合取範式的下列三個公式:

所有命題公式都可以轉換成 CNF 的等價公式。這種變換基於了關於邏輯等價的規則: 雙重否定律德·摩根定律分配律

因為所有邏輯公式都可以轉換成合取範式的等價公式,證明經常基於所有公式都是 CNF 的假定。但是在某些情況下,這種到 CNF 的轉換可能導致公式的指數性爆漲。例如,把下述非-CNF 公式轉換成 CNF 生成有 個子句的公式:

參見[編輯]

外部連結[編輯]