跳转到内容

析取范式

维基百科,自由的百科全书
(重定向自积之和

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

但如下公式不是 DNF:

NOT 是最外层的算子
一个 OR 嵌套在一个 AND 中

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

参见