ДНФ

Дизъюнкти́вная норма́льная фо́рма (ДНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид дизъюнкции нескольких конъюнктов.

Например, следующие формулы записаны в ДНФ:

$A \or B$

$A\!$

$(A \and B) \or \neg A$

$(A \and B \and \neg C) \or (\neg D \and E \and F) \or (C \and D) \or B$

Дизъюнктивная нормальная форма удобна для автоматического доказывания теорем.

Приведение булевой формулы к ДНФ

Любая булева формула может быть приведена к ДНФ. Впрочем, при этом размер булевой формулы может возрасти экспоненциально. Так, например, 2ⁿ конъюнктов потребуется, чтобы записать следующую формулу:

$(X_1 \or Y_1) \and (X_2 \or Y_2) \and \dots \and (X_n \or Y_n)$

Формальная грамматика, описывающая ДНФ

Следующая формальная грамматика описывает все формулы, приведенные к ДНФ:

<ДНФ> → <конъюнкт>

<ДНФ> → <ДНФ> ∨ <конъюнкт>

<конъюнкт> → <литерал>

<конъюнкт> → (<конъюнкт> ∧ <литерал>)

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

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

где <терм> обозначает произвольную булеву переменную.

См. также

• Минтерм
• Конъюнктивная нормальная форма