[科普中国]-析取范式定理

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

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

但如下公式不是 DNF：

是最外层的算子

一个 OR 嵌套在一个 AND 中

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

布尔函数在数学中，布尔函数（Boolean function）描述如何基于对布尔输入的某种逻辑计算确定布尔值输出。它们在复杂性理论的问题和数字计算机的芯片设计中扮演基础角色。布尔函数的性质在密码学中扮演关键角色，特别是在对称密钥算法的设计中（参见S-box）。1

参见代数范式

Horn子句

Quine-McCluskey算法

合取范式

本词条内容贡献者为:

任毅如 - 副教授 - 湖南大学