合取范式

在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的规范和之积形式。 所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和一个单一子句的合取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。