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

{{Unreferenced|time=2024-07-22T15:14:04+00:00}}
在[[布尔逻辑]]中，如果一个[[公式 (数理逻辑)|公式]]是[[子句 (逻辑)|子句]]的[[逻辑合取|合取]]，那么它是'''合取范式'''（CNF）的。作为[[规范形式]]，它在[[自动定理证明]]中有用。它类似于在电路理论中的[[规范和之积形式]]。

所有的文字的合取和所有的文字的析取是CNF的，因为可以被分别看作一个文字的子句的合取和析取。和[[析取范式]]（DNF）中一样，在CNF公式中可以包含的命题连结词是[[逻辑合取|与]]、[[逻辑析取|或]]和[[逻辑否定|非]]。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。

例如，下列所有公式都是CNF:

:<math>A \wedge B</math>
:<math>\neg A \wedge (B \vee C)</math>
:<math>(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)</math>
:<math>(\neg B \vee C)</math>

而下列不是:

:<math>\neg (B \vee C)</math>
:<math>(A \wedge B) \vee C</math>
:<math>A \wedge (B \vee (D \wedge E))</math>

上述三个公式分别等价于合取范式的下列三个公式:

:<math>\neg B \wedge \neg C</math>
:<math>(A \vee C) \wedge (B \vee C)</math>
:<math>A \wedge (B \vee D) \wedge (B \vee E)</math>

所有命题公式都可以转换成 CNF 的[[逻辑等价|等价]]公式。这种变换基于了关于[[逻辑等价]]的规则: [[双重否定消去|双重否定律]]、[[德·摩根定律]]和[[分配律]]。 

因为所有逻辑公式都可以转换成合取范式的等价公式，证明经常基于所有公式都是 CNF 的假定。但是在某些情况下，这种到 CNF 的转换可能导致公式的指数性爆涨。例如，把下述非-CNF 公式转换成 CNF 生成有 <math>2^n</math> 个子句的公式:

:<math>(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n)</math>

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

==外部链接==
* [https://web.archive.org/web/20070312055054/http://www.g615.co.uk/riftor/content.php?view=5&type=1 Scheme and Ocaml programs for converting propositional logic statements into CNF]

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