登录在布尔逻辑中，析取范式（DNF）是逻辑公式的标准化（或规范化），它是合取子句的析取。作为规范形式，它在自动定理证明中有用。一个逻辑公式被认为是 DNF 的，当且仅当它是一个或多个文字的一个或多个合取的析取。
具体来说，如果每个合取式（conjunction）中的每个变量恰好出现一次，则DNF公式为完全析取范式。与合取范式（CNF）一样，DNF中唯一的命题运算符是和（and），或（or），不是（not）。 not运算符只能用作文字的一部分，因此它只能放在命题变量之前。
以下是DNF的正式语法：
析取→（合取∨析取）
析取→合取
合取→（字面∧合取）
合取→文字
文字→¬变量
文字→变量
变量可以是任何变量，下面是一些DNF的例子：
但是以下例子不属于DNF：
前者因为OR嵌套在NOT中，后者则因为OR嵌套在AND中。
[描述来源：维基百科 URL：https://en.wikipedia.org/wiki/Disjunctive_normal_form]
发展历史
1971年，Stephen A. Cook介绍和讨论了一种测量谓词演算证明程序复杂性的方法，其中就使用了DNF。
1986年，YU.I. ZHUBAVLEV 和 A.YU. KOGAN 给出了一种算法，用于构造布尔函数的析取正态形式，并给出了估计的算法复杂度。他们也给出了使用该算法构造一些特殊类函数的最短析取范式的例子。
作为计算机科学的基础概念，1990年，Davey和Priestley在他们的书中提出所有逻辑公式都可以转换为等价的析取范式。
2001年，Adnan Darwiche提出了一种新的目标编译语言，称为可分解否定范式（DNNF），他们表明DNNF是普遍的：支持时间逻辑运算、比OBDD更节省空间并且就其结构和算法而言，它非常简单。此外，他们提出了一种算法，用于将任何命名形式的命题理论转换为DNNF，并表明如果条件形式具有有界树宽，则其DNNF编译具有线性大小并且可以在线性时间内计算。DNNF中即包含了DNF和CNF等情况。
主要事件
| 年份 | 事件 | 相关论文/Reference |
| 1971 | Stephen A. Cook介绍和讨论了一种测量谓词演算证明程序复杂性的方法，其中就使用了DNF | Cook, S. A. (1971). The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing. pp 151-158. |
| 1986 | YU.I. ZHUBAVLEV 和 A.YU. KOGAN 给出了一种算法，用于构造布尔函数的析取正态形式，并给出了估计的算法复杂度 | ZHUBAVLEV, Y. I. and KOGAN, A. Y. (1986). AN ALGORITHM FOR CONSTRUCTING A DISJUNCTIVE NORMAL FORM EQUIVALENT TO THE PRODUCT OF THE LEFT-HAND SIDES OF NELSON BOOLEAN EQUATIONS. U.S.S.R. Canput.Maths.Math.Phys., 26(4): 184-188. |
| 1990 | Davey和Priestley在他们的书中提出所有逻辑公式都可以转换为等价的析取范式 | B.A. Davey and H.A. Priestley (1990). Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press. |
| 2001 | Adnan Darwiche提出了一种新的目标编译语言，称为可分解否定范式（DNNF） | Darwiche, A. (2001). Decomposable negation normal form. Journal of the ACM (JACM). 48(4): 608-647. |
发展分析
瓶颈
DNF本身只是计算机科学的基础概念，其作用范围十分有限。
未来发展方向
上文已经提及，作为基础概念，有关研究需要在此基础上提出更高级的编译语言。
Contributor: Yuanyuan Li
