Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції.
Приклади
Наступні формули записані в КНФ:
Наступні формули не є в КНФ:
Проте ці формули еквівалентні наступним формулам записаним у кон'юнктивній нормальній формі:
Приведення булевої формули до КНФ
Довільна булева формула може бути приведена до КНФ за допомогою наступного алгоритму:
Крок 1 : Усі логічні зв'язки виразити через кон'юнкцію, диз'юнкцію і заперечення. Крок 2 : Скасувати всі подвійні заперечення і використати, де можливо, правила де Моргана. Тобто замінити: на на на Крок 3 : Використати де можливо дистрибутивність диз'юнкції, тобто замінити: і на
Втім, при цьому розмір булевої формули може зрости експоненціально. Так, наприклад, щоб записати наступну формулу буде потрібно 2n диз'юнктів:
КНФ цієї формули має вигляд:
Формальна граматика, що описує КНФ
Наступна формальна граматика описує всі формули, приведені до КНФ: <КНФ> → <диз'юнкт> <КНФ> → <КНФ> ∧ <диз'юнкт> <диз'юнкт> → <літерал> <диз'юнкт> → (<диз'юнкт> ∨ <літерал>) <літерал> → <терм> <літерал> → ¬<терм>
де <терм> позначає довільну булеву змінну.
Див. також Диз'юнктивна нормальна форма Нормальна форма формули у логіці предикатів Числення висловлень Досконала кон'юнктивна нормальна форма
Джерела