## [Forma Normal Conjuntiva](/es/node/60816) Definición Una fórmula expresada como una conjunción de disyunciones de literales, comúnmente usada en resolución de satisfacibilidad y normalización lógica. ## Principio Principio La FNC organiza una fórmula en una conjunción finita de cláusulas, donde cada cláusula es una disyunción de literales; equivalencias lógicas (De Morgan, distributividad) y manipulaciones de cuantificadores se usan para convertir fórmulas a FNC preservando satisfacibilidad o equivalencia según las transformaciones aplicadas. ## Demostración Demostración La fórmula (p ∨ q) ∧ (¬p ∨ r) está en FNC; para convertir (p ∧ q) ∨ r a FNC se aplica distributividad y se obtiene (p ∨ r) ∧ (q ∨ r). En razonamiento automático las cláusulas de FNC suelen tratarse como conjuntos de literales. ## Aplicación incorrecta Aplicación incorrecta Asumir que la conversión a FNC siempre preserva la equivalencia lógica de la fórmula original es erróneo; algunos procedimientos introducen símbolos nuevos o funciones de Skolem y producen solo una FNC equisatisfacible, no equivalente, lo que conduce a afirmaciones incorrectas sobre preservación de modelos. ## Consecuencia Consecuencia Expresar fórmulas en FNC permite el uso directo de solvers SAT y demostradores basados en resolución, facilita la indexación de cláusulas y la propagación unitaria, y estandariza la entrada para muchos procedimientos de decisión. ## Inversión Inversión La perspectiva dual es la Forma Normal Disyuntiva (FND), donde la fórmula es una disyunción de conjunciones de literales; pasar de FNC a FND puede revelar implicantes primos pero comúnmente causa un estallido exponencial del tamaño. ## Límite Límite La FNC exige que las cláusulas sean disyunciones de literales; no prescribe la colocación de cuantificadores ni trata conectivos más ricos sin transformación, y una conversión ingenua puede provocar un incremento exponencial del tamaño de la fórmula. ## Tensión semántica Tensión semántica FNC vs conjunto de cláusulas vs teoría normalizada: la FNC como forma sintáctica está estrechamente relacionada con el conjunto abstracto de cláusulas usado por los solvers, pero la correspondencia uno a uno puede distorsionarse cuando símbolos nuevos o la skolemización alteran la equivalencia. ## Síntesis Síntesis La Forma Normal Conjuntiva es la disposición canónica que organiza una fórmula como conjunción de cláusulas disyuntivas de literales; es fundamental para algoritmos de satisfacibilidad y flujos de normalización, requiriendo precaución sobre equivalencia frente a equisatisfacibilidad.