Forma normal de negación

En lógica matemática , una fórmula está en forma normal de negación (NNF) si el operador de negación ( , no ) solo se aplica a variables y los únicos otros operadores booleanos permitidos son la conjunción ( , y ) y la disyunción ( , o ). ${\displaystyle \lno}$${\displaystyle \tierra}$${\displaystyle \lor}$

La forma normal de negación no es una forma canónica : por ejemplo, y son equivalentes, y ambos están en forma normal de negación. ${\displaystyle a\land (b\lor \lno c)}$${\displaystyle (a\land b)\lor (a\land \lno c)}$

En la lógica clásica y en muchas lógicas modales , cada fórmula puede adoptar esta forma reemplazando las implicaciones y equivalencias por sus definiciones, utilizando las leyes de De Morgan para empujar la negación hacia adentro y eliminando las negaciones dobles. Este proceso puede representarse utilizando las siguientes reglas de reescritura : ^[1]

${\displaystyle {\begin{aligned}A\Rightarrow B&~\to ~\lno A\lo B\\A\Leftrightarrow B&~\to ~(\lno A\lo B)\land (A\lo \lno B)\\\lno (A\lo B)&~\to ~\lno A\land \lno B\\\lno (A\land B)&~\to ~\lno A\lo \lno B\\\lno \lno A&~\to ~A\\\lno \existe xA&~\to ~\para todo x\lno A\\\lno \para todo xA&~\to ~\existe x\lno A\end{aligned}}}$

(En estas reglas, el símbolo indica implicación lógica en la fórmula que se está reescribiendo, y es la operación de reescritura). ${\displaystyle \Flecha derecha}$${\displaystyle \to}$

La transformación a la forma normal de negación puede aumentar el tamaño de una fórmula solo de manera lineal: el número de ocurrencias de fórmulas atómicas permanece igual, el número total de ocurrencias de y no cambia, y el número de ocurrencias de en la forma normal está limitado por la longitud de la fórmula original. ${\displaystyle \tierra}$${\displaystyle \lor}$${\displaystyle \lno}$

Una fórmula en forma normal de negación se puede poner en la forma normal conjuntiva más fuerte o en la forma normal disyuntiva aplicando distributividad . La aplicación repetida de la distributividad puede aumentar exponencialmente el tamaño de una fórmula. En la lógica proposicional clásica , la transformación a la forma normal de negación no afecta las propiedades computacionales: el problema de satisfacibilidad continúa siendo NP-completo y el problema de validez continúa siendo co-NP-completo . Para fórmulas en forma normal conjuntiva, el problema de validez es solucionable en tiempo polinomial, y para fórmulas en forma normal disyuntiva, el problema de satisfacibilidad es solucionable en tiempo polinomial.

Las siguientes fórmulas están todas en forma normal de negación:

${\displaystyle {\begin{alineado}(A&\vee B)\wedge C\\(A&\wedge (\lno B\vee C)\wedge \lno C)\vee D\\A&\vee \lno B\\A&\wedge \lno B\end{alineado}}}$

El primer ejemplo también está en forma normal conjuntiva y los dos últimos están tanto en forma normal conjuntiva como en forma normal disyuntiva , pero el segundo ejemplo no está en ninguna de las dos.

Las siguientes fórmulas no están en forma normal de negación:

${\displaystyle {\begin{aligned}A&\Rightarrow B\\\lno (A&\vee B)\\\lno (A&\wedge B)\\\lno (A&\vee \lno C)\end{aligned}}}$

Sin embargo, son respectivamente equivalentes a las siguientes fórmulas en forma normal de negación:

${\displaystyle {\begin{aligned}\lno A&\vee B\\\lno A&\wedge \lno B\\\lno A&\vee \lno B\\\lno A&\wedge C\end{aligned}}}$

• Forma normal conjuntiva
• Forma normal disyuntiva

• Robinson, John Alan ; Voronkov, Andrei , eds. (2001). Manual de razonamiento automatizado . Vol. 1. MIT Press . Págs. 203 y siguientes. ISBN . 0444829490.

• Subprograma Java para convertir fórmulas lógicas a la forma normal de negación, mostrando las leyes utilizadas