Дизъюнкти́вная норма́льная фо́рма (ДНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид дизъюнкции нескольких конъюнктов.
Например, следующие формулы записаны в ДНФ:
Дизъюнктивная нормальная форма удобна для автоматического доказывания теорем.
Приведение булевой формулы к ДНФ[]
Любая булева формула может быть приведена к ДНФ. Впрочем, при этом размер булевой формулы может возрасти экспоненциально. Так, например, 2n конъюнктов потребуется, чтобы записать следующую формулу:
Формальная грамматика, описывающая ДНФ[]
Следующая формальная грамматика описывает все формулы, приведенные к ДНФ:
- <ДНФ> → <конъюнкт>
- <ДНФ> → <ДНФ> ∨ <конъюнкт>
- <конъюнкт> → <литерал>
- <конъюнкт> → (<конъюнкт> ∧ <литерал>)
- <литерал> → <терм>
- <литерал> → ¬<терм>
где <терм> обозначает произвольную булеву переменную.
См. также[]
he:DNF hu:Diszjunktív normálforma pl:Dysjunkcyjna postać normalna