析取范式

维基百科,自由的百科全书
跳转至: 导航搜索

布尔逻辑中,析取范式(DNF)是逻辑公式的标准化(或规范化),它是合取子句的析取。作为规范形式,它在自动定理证明中有用。一个逻辑公式被认为是 DNF 的,当且仅当它是一个或多个文字的一个或多个合取析取。同合取范式(CNF)一样,在 DNF 中的命题算子是。非算子只能用做文字的一部分,这意味着它只能领先于命题变量。例如,下列公式都是 DNF:

A \or B
A\!
(A \and B) \or C
(A \and \neg B \and \neg C) \or (\neg D \and E \and F)

但如下公式不是 DNF:

\neg(A \or B) NOT 是最外层的算子
A \or (B \and (C \or D)) 一个 OR 嵌套在一个 AND 中

把公式转换成 DNF 要使用逻辑等价,比如双重否定除去德·摩根定律分配律。注意所有逻辑公式都可以转换成析取范式。但是,在某些情况下转换成 DNF 可能导致公式的指数性爆涨。例如,在 DNF 形式下,如下逻辑公式有 2n 个项:

(X_1 \or Y_1) \and (X_2 \or Y_2) \and \dots \and (X_n \or Y_n)

参见[编辑]