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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Приклади[ред.ред. код]

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

A \and B
A\!
(A \or B) \and \neg A
(A \or B \or \neg C) \and (\neg D \or E \or F) \and (C \or D) \and 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))

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

(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and 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).

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

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

<КНФ> → <диз'юнкт>
<КНФ> → <КНФ> ∧ <диз'юнкт>
<диз'юнкт> → <літерал>
<диз'юнкт> → (<диз'юнкт> ∨ <літерал>)
<літерал> → <терм>
<літерал> → ¬<терм>

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

Див. також[ред.ред. код]

Джерела[ред.ред. код]

Shawn Hedman. A First Course in Logic. Oxford University Press 2004 ISBN 0-19-852980-5