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

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

Приклади

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

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

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

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

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

Крок 1 : Усі логічні зв'язки виразити через кон'юнкцію, диз'юнкцію і заперечення.
Крок 2 : Скасувати всі подвійні заперечення і використати, де можливо, правила де Моргана. Тобто замінити:
на
на
на
Крок 3 : Використати де можливо дистрибутивність диз'юнкції, тобто замінити:
і на

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

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

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

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

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

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

Див. також

Джерела

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

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.