查看“︁析取范式”︁的源代码

{{Unreferenced|time=2024-07-22T15:14:34+00:00}}
在[[布尔逻辑]]中，'''析取范式'''（DNF）是逻辑公式的标准化（或规范化），它是合取[[子句 (逻辑)|子句]]的析取。作为[[规范形式]]，它在[[自动定理证明]]中有用。一个逻辑公式被认为是 DNF 的，[[当且仅当]]它是一个或多个[[文字 (数理逻辑)|文字]]的一个或多个[[逻辑合取|合取]]的[[逻辑析取|析取]]。同[[合取范式]]（CNF）一样，在 DNF 中的命题算子是[[逻辑合取|与]]、[[逻辑析取|或]]和[[逻辑否定|非]]。非算子只能用做文字的一部分，这意味着它只能领先于命题变量。例如，下列公式都是 DNF:

:<math>A \lor B</math>
:<math>A\!</math>
:<math>(A \land B) \lor C</math>
:<math>(A \land \neg B \land \neg C) \lor (\neg D \land E \land F)</math>

但如下公式不是 DNF:

:<math>\neg(A \lor B)</math> NOT 是最外层的算子
:<math>A \lor (B \land (C \lor D))</math> 一个 OR 嵌套在一个 AND 中

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

:<math>(X_1 \lor Y_1) \land (X_2 \lor Y_2) \land \dots \land (X_n \lor Y_n)</math>

==参见==

* [[合取范式]]
* [[代数范式]]
* [[霍恩子句]]
* [[奎因－麦克拉斯基算法]]

[[Category:布尔代数|X]]