Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ.[1] Для этого можно использовать: Закон двойного отрицания, Закон де Моргана, Дистрибутивность.

Алгоритм построения КНФ
1) Избавиться от всех логических операций, содержащихся в формуле, заменив их основными: конъюнкцией, дизъюнкцией, отрицанием. Это можно сделать, используя равносильные формулы:


2) Заменить знак отрицания, относящийся ко всему выражению, знаками отрицания, относящимися к отдельным переменным высказываниям на основании формул:


3) Избавиться от знаков двойного отрицания.
4) Применить, если нужно, к операциям конъюнкции и дизъюнкции свойства дистрибутивности и формулы поглощения.

Пример построения КНФ
Приведем к КНФ формулу

Преобразуем формулу F к формуле не содержащей → :

В полученной формуле перенесем отрицание к переменным и сократим двойные отрицания:

По закону дистрибутивности получим КНФ:

k-конъюнктивная нормальная форма
k-конъюнктивной нормальной формой называют конъюнктивную нормальную форму, в которой каждая дизъюнкция содержит ровно k литералов.
Например, следующая формула записана в 2-КНФ:

Переход от КНФ к СКНФ
Если в простой дизъюнкции не хватает какой-то переменной (например, z, то добавляем в нее выражение : (это не меняет самой дизъюнкции), после чего раскрываем скобки с использованием распределительного закона):

Таким образом, из КНФ получена СКНФ.