Forma normal disyuntiva
# Forma normal disyuntiva

En lógica booleana, una forma normal disyuntiva (FND) es una estandarización (o normalización) de una fórmula lógica que es una disyunción de cláusulas conjuntivas. Como una forma normal, es útil en la demostración automática de teoremas. Una fórmula FND está en forma normal disyuntiva completa si cada una de sus variables aparece exactamente una vez en cada cláusula.
Al igual que en forma normal conjuntiva (FNC), los únicos operadores proposicionales en FND son la conjunción, disyunción y negación. Una negación solo se puede aplicar a un literal, lo que significa que solo puede preceder a una variable proposicional. Por ejemplo, todas las siguientes fórmulas están en FND:
* $A\land B$
* $A\!$
* $(A\land B)\lor C$
* $(A\land \neg B\land \neg C)\lor (\neg D\land E\land F)$
Sin embargo, las siguientes fórmulas no están en FND:
* $\neg (A\lor B)$ (la negación se aplica a una cláusula disyuntiva, no a un literal).
* $A\lor (B\land (C\lor D))$ (una disyunción está anidada a una conjunción).

# Forma normal disyuntiva
## Convertir una fórmula en FND

La conversión de una fórmula para FND implica el uso de equivalencias lógicas como la eliminación de la doble negación, las leyes de De Morgan, y uso de la distributividad.
Todas las fórmulas lógicas se pueden convertir en forma normal disyuntiva. Sin embargo, en algunos casos, la conversión a FND puede conducir a una explosión exponencial de la fórmula. Por ejemplo, en FND, las fórmulas lógicas de las siguientes formas tienen términos 2$^n$:
    $(X_{1}\lor Y_{1})\land (X_{2}\lor Y_{2})\land \dots \land (X_{n}\lor Y_{n})$
Cualquier función booleana en particular puede ser representada por una y solo una forma normal disyuntiva completa, una de las dos formas canónicas.
Una variación importante utilizada en el estudio de la complejidad computacional es k-DNF. Una fórmula está en k-FND si está en FND y cada cláusula contiene en la mayoría de los literales k. A diferencia de las subclases correspondientes de forma normal conjuntiva para k> = 3, no hay algoritmo fácil de convertir una instancia arbitraria de una fórmula en FND a k-FND.
La siguiente fórmula es una gramática formal para FND:
* disyunción → conjunción
* disyunción → disyunción ∨ conjunción
* conjunción → literal
* conjunción → (conjunción ∧ literal)
* literal → variable
* literal → ¬variable
Donde variable es cualquier variable.