КНФ

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

Приклади

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

${\displaystyle A\land B}$

${\displaystyle A\!}$

${\displaystyle (A\lor B)\land \neg A}$

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

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

${\displaystyle \neg (B\vee C)}$

${\displaystyle (A\wedge B)\vee C}$

${\displaystyle A\wedge (B\vee (D\wedge E)).}$

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

${\displaystyle \neg B\wedge \neg C}$

${\displaystyle (A\vee C)\wedge (B\vee C)}$

${\displaystyle A\wedge (B\vee D)\wedge (B\vee E).}$

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

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

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

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

${\displaystyle \lnot \lnot A}$ на ${\displaystyle A\;}$

${\displaystyle \lnot (A\land B)}$ на ${\displaystyle (\lnot A\lor \lnot B)}$

${\displaystyle \lnot (A\lor B)}$ на ${\displaystyle (\lnot A\land \lnot B)}$

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

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

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

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

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

${\displaystyle (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}).}$

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

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

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

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

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

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

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

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

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

Див. також

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

Джерела

Shawn Hedman. A First Course in Logic. Oxford University Press 2004