Forme normale disjonctive

En logique booléenne ou en calcul des propositions, une forme normale disjonctive ou FND (en anglais, disjunctive normal form ou DNF) est une normalisation d'une expression logique qui est une disjonction de clauses conjonctives. Elle est utilisée dans la démonstration automatique de théorèmes. Une expression logique est en FND si et seulement si elle est une disjonction d'une ou plusieurs conjonctions d'un ou plusieurs littéraux. Tout comme dans une forme normale conjonctive (FNC), les seuls opérateurs dans une FND sont le et logique, le ou logique et la négation. L'opérateur non ne peut être utilisé que dans un littéral, c'est-à-dire qu'il ne peut que précéder une variable. Par exemple, toutes les expressions suivantes sont en FND:

${\displaystyle A\lor B}$

${\displaystyle A\!}$

${\displaystyle (A\land B)\lor C}$

${\displaystyle (A\land \neg B\land \neg C)\lor (\neg D\land E\land F)}$

Pour les articles homonymes, voir FND et DNF.

Cependant, les expressions suivantes ne sont pas en FND:

${\displaystyle \neg (A\lor B)}$ — la négation s'applique à toute la parenthèse plutôt que directement à une variable

${\displaystyle A\lor (B\land (C\lor D))}$ — un ou est imbriqué dans un et

Convertir une expression vers une FND requiert l'utilisation d'équivalences logiques, comme l'élimination de double négations, les lois de De Morgan, et la loi de distributivité. Toutes les expressions booléennes peuvent être converties en FND. Cependant, dans quelques cas la conversion à la FND peut mener à un allongement exponentiel de l'expression. Par exemple, la FND d'une expression de la forme suivante a 2ⁿ termes :

${\displaystyle (X_{1}\lor Y_{1})\land (X_{2}\lor Y_{2})\land \dots \land (X_{n}\lor Y_{n})}$

Ce qui suit est une grammaire formelle pour la FND :

1. <ou> → ∨
2. <et> → ∧
3. <non> → ¬
4. <disjonction> → <conjonction>
5. <disjonction> → <disjonction> <ou> <conjonction>
6. <conjonction> → <littéral>
7. <conjonction> → (<conjonction> <et> <littéral>)
8. <littéral> → <terme>
9. <littéral> → <non><terme>

où <terme> est une variable quelconque.