Кон'юнктивна нормальна форма

Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції.

Приклади

Наступні формули записані в КНФ:

$A\land B$

$A\!$

$(A\lor B)\land \neg A$

$(A\lor B\lor \neg C)\land (\neg D\lor E\lor F)\land (C\lor D)\land B$

Наступні формули не є в КНФ:

$\neg (B\vee C)$

$(A\wedge B)\vee C$

$A\wedge (B\vee (D\wedge E)).$

Проте ці формули еквівалентні наступним формулам записаним у кон'юнктивній нормальній формі:

$\neg B\wedge \neg C$

$(A\vee C)\wedge (B\vee C)$

$A\wedge (B\vee D)\wedge (B\vee E).$

Приведення булевої формули до КНФ

Довільна булева формула може бути приведена до КНФ за допомогою наступного алгоритму:

Крок 1 : Усі логічні зв'язки виразити через кон'юнкцію, диз'юнкцію і заперечення.

Крок 2 : Скасувати всі подвійні заперечення і використати, де можливо, правила де Моргана. Тобто замінити:

$\lnot \lnot A$ на $A\;$

$\lnot (A\land B)$ на $(\lnot A\lor \lnot B)$

$\lnot (A\lor B)$ на $(\lnot A\land \lnot B)$

Крок 3 : Використати де можливо дистрибутивність диз'юнкції, тобто замінити:

$(A\lor (B\land C))$ і $((B\land C)\lor A)$ на $((A\lor B)\land (A\lor C))$

Втім, при цьому розмір булевої формули може зрости експоненціально. Так, наприклад, щоб записати наступну формулу буде потрібно 2ⁿ диз'юнктів:

$(X_{1}\land Y_{1})\lor (X_{2}\land Y_{2})\lor \dots \lor (X_{n}\land Y_{n})$

КНФ цієї формули має вигляд:

$(X_{1}\vee \cdots \vee X_{n-1}\vee X_{n})\wedge (X_{1}\vee \cdots \vee X_{n-1}\vee Y_{n})\wedge \cdots \wedge (Y_{1}\vee \cdots \vee Y_{n-1}\vee Y_{n}).$

Формальна граматика, що описує КНФ

Наступна формальна граматика описує всі формули, приведені до КНФ:

<КНФ> → <диз'юнкт>

<КНФ> → <КНФ> ∧ <диз'юнкт>

<диз'юнкт> → <літерал>

<диз'юнкт> → (<диз'юнкт> ∨ <літерал>)

<літерал> → <терм>

<літерал> → ¬<терм>

де <терм> позначає довільну булеву змінну.

Див. також

• Диз'юнктивна нормальна форма
• Нормальна форма формули у логіці предикатів
• Числення висловлень
• Досконала кон'юнктивна нормальна форма

Джерела

• Г. Цейтлін. Елементи теорії булевих функцій. — Київ : Техніка, 1967. — 76 с.(укр.)
• Вітенько І. В. Математична логіка: Курс лекцій. — Ужгород : УжДУ, 1971. — 224 с.(укр.)
• Хромой В. Я. Збірник вправ і задач з математичної логіки. — Київ : Вища школа, 1978. — 160 с.(укр.)
• Дрозд Ю. А. (2005). Основи математичної логіки (PDF). Київ: ВПЦ "Київський університет". с. 96. (укр.)
• Безущак О. О., Ганюшкін О. Г. Математична логіка: Навчальний посібник. — Київ : ВПЦ "Київський університет", 2023. — 143 с.(укр.)