析取範式定理

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

基本介紹

• 中文名：析取範式定理
• 外文名：Disjunctive normal form

簡介

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

但如下公式不是 DNF：

是最外層的運算元

一個 OR 嵌套在一個 AND 中

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

布爾函式

在數學中，布爾函式（Boolean function）描述如何基於對布爾輸入的某種邏輯計算確定布爾值輸出。它們在複雜性理論的問題和數字計算機的晶片設計中扮演基礎角色。布爾函式的性質在密碼學中扮演關鍵角色，特別是在對稱密鑰算法的設計中（參見S-box）。

參見

• 代數範式
• Horn子句
• Quine-McCluskey算法
• 合取範式