Loading AI tools
З Вікіпедії, вільної енциклопедії
Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції.
Наступні формули записані в КНФ:
Наступні формули не є в КНФ:
Проте ці формули еквівалентні наступним формулам записаним у кон'юнктивній нормальній формі:
Довільна булева формула може бути приведена до КНФ за допомогою наступного алгоритму:
Втім, при цьому розмір булевої формули може зрости експоненціально. Так, наприклад, щоб записати наступну формулу буде потрібно 2n диз'юнктів:
КНФ цієї формули має вигляд:
Наступна формальна граматика описує всі формули, приведені до КНФ:
де <терм> позначає довільну булеву змінну.
Shawn Hedman. A First Course in Logic. Oxford University Press 2004 ISBN 0-19-852980-5
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.