En lógica booleana, una fórmula está en forma normal conjuntiva (FNC) si corresponde a una conjunción de cláusulas, donde una cláusula es una disyunción de literales, donde un literal y su complemento no pueden aparecer en la misma cláusula.
Al igual que en una forma normal disyuntiva (FND), los únicos conectivos lógicos que pueden aparecer en una fórmula en FNC son la conjunción, disyunción y negación.
El operador negación solo puede aplicarse a un literal, y no a una cláusula completa, lo que significa que este sólo puede preceder a una variable proposicional o un símbolo de predicado.
Las siguientes fórmulas están en FNC: La última forma está en FNC porque puede ser vista como la conjunción de las dos cláusulas de literales
Esta fórmula es también una forma normal disyuntiva.
En particular, este es el caso para los tres contraejemplos recién mencionados; que son, respectivamente, equivalentes a las siguientes tres fórmulas, que están en forma normal conjuntiva: Cada fórmula proposicional puede convertirse en una fórmula equivalente que está en FNC.
Esta transformación se basa en reglas sobre equivalencias lógicas: la doble negación, las leyes de De Morgan, y la distributividad.
Sin embargo, hay algunos casos en que dicha conversión puede producir un crecimiento exponencial del tamaño de la fórmula.
Existen transformaciones en FNC que evitan un crecimiento exponencial en el tamaño preservando la satisfacibilidad en lugar de equivalencia.
[1][2] Estas transformaciones están garantizadas para aumentar solo linealmente el tamaño de la fórmula, pero introduce nuevas variables.
Por ejemplo, la fórmula anterior puede ser transformada en FNC adicionando variables
como sigue: Una traducción alternativa, la transformación Tseitin, incluye también las cláusulas
; esta fórmula muchas veces se considera para "definir"
En la lógica de primer orden, forma normal conjuntiva puede tomarse más para producir la forma normal clausal de una fórmula lógica, que se puede utilizar luego para realizar la resolución de primer orden.
En una resolución basada en la provisión automatizada de teorema, una fórmula FNC Un importante conjunto de problemas en complejidad computacional incluye el encontrar asignaciones para las variables de una fórmula expresada como forma normal conjuntiva, de modo que la fórmula sea verdadera.
El problema k-SAT es un problema computacional que consiste en encontrar una asignación satisfacible para una fórmula expresada en FNC tal que cada disyunción contenga la mayor cantidad de variables k posibles.
Como consecuencia,[nota 1] la tarea de convertir una fórmula a una FND, preservando la satisfactibilidad, es NP-hard; dualmente, convertido en FNC, preservando satisfactilidad, también es NP-hard; por lo tanto la equivalencia preservando conversión en FND o FNC también es un NP-hard.
Los problemas típicos en este caso involucran fórmulas en "3FNC": La forma normal conjuntiva con no más de tres variables por conjunción.
Ejemplos de tales fórmulas encontradas en la práctica pueden ser muy grandes, por ejemplo, con 100.000 variables y 1.000.000 conjunciones.
Una fórmula en FNC se puede convertir en una fórmula equisatisfiable en "kFNC" (para k> = 3) sustituyendo cada uno en conjunción con más de variables k
, y repitiendo cuantas veces sea necesario.
Para convertir lógica de primer orden a FNC:[3] A modo de ejemplo, la fórmula que dice "Quien ama a todos los animales, es a su vez amado por alguien" se convierte en FNC (y posteriormente en forma de cláusula en la última línea) de la siguiente manera (resaltando regla de sustitución redichas con
puede ser pensado como dando a la persona por quien es amado
se obtiene el animal (si los hay) que
La tercera última línea contando desde abajo se lee como "
n i m a l ( f ( x ) ) ∨