Конъюнктивная нормальная форма
В булевой логике формула находится в конъюнктивной нормальной форме ( CNF ) или клаузальной нормальной форме , если она является конъюнкцией одного или нескольких предложений , где предложение является дизъюнкцией литералов ; иначе говоря, это произведение сумм или И ИЛИ . Как каноническая нормальная форма , она полезна в автоматизированном доказательстве теорем и теории цепей .
Все соединения литералов и все дизъюнкции литералов находятся в CNF, поскольку их можно рассматривать как соединения однобуквенных предложений и союзов одного предложения соответственно. Как и в дизъюнктивной нормальной форме (ДНФ), единственные пропозициональные связки, которые может содержать формула в КНФ, это и , или , и не . Оператор not может использоваться только как часть литерала, что означает, что он может предшествовать только пропозициональной переменной или символу предиката .
В автоматизированном доказательстве теорем понятие « клаузальная нормальная форма » часто используется в более узком смысле, означая конкретное представление формулы КНФ в виде набора наборов литералов.
Все следующие формулы в переменных и находятся в конъюнктивной нормальной форме:
Для ясности разделительные предложения написаны внутри круглых скобок выше. В дизъюнктивной нормальной форме с союзными предложениями в скобках последний случай такой же, но предпоследним является . Константы true и false обозначаются пустым конъюнктом и одним предложением, состоящим из пустого дизъюнкта, но обычно записываются явно. [1]
Каждая формула может быть эквивалентно записана как формула в конъюнктивной нормальной форме. Три не-примера в CNF: