En lógica matemática , una fórmula está en forma normal de negación (NNF) si el operador de negación (, not ) solo se aplica a variables y los únicos otros operadores booleanos permitidos son las conjunciones (, y ) y disyunción (, o ).
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.
En la lógica clásica y 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 se puede representar mediante las siguientes reglas de reescritura ( Handbook of Automated Reasoning 1, p. 204):
[En estas reglas, el El símbolo indica una implicación lógica en la fórmula que se está reescribiendo, y es la operación de reescritura.]
La transformación a la forma normal de negación puede aumentar el tamaño de una fórmula solo de forma lineal: el número de apariciones de fórmulas atómicas permanece igual, el número total de apariciones de y no ha cambiado, y el número de apariciones de puede duplicarse.
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 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 CNF, el problema de validez se puede resolver en tiempo polinomial, y para fórmulas en DNF, el problema de satisfacibilidad se puede resolver en tiempo polinomial.
Ejemplos y contraejemplos
Las siguientes fórmulas están todas en forma normal de negación:
El primer ejemplo es también en forma normal conjuntiva y las dos últimas son tanto en forma normal conjuntiva y forma normal disyuntiva , pero el segundo ejemplo está en ninguno de ellos.
Las siguientes fórmulas no están en forma normal de negación:
Sin embargo, son respectivamente equivalentes a las siguientes fórmulas en forma normal de negación:
Referencias
- Alan JA Robinson y Andrei Voronkov, Manual de razonamiento automatizado 1 : 203 y siguientes (2001) ISBN 0444829490 .