Forma normal conjuntiva

Forma estándar de la función booleana

En lógica booleana , una fórmula está en forma normal conjuntiva ( CNF ) o forma normal clausular si es una conjunción de una o más cláusulas , donde una cláusula es una disyunción de literales ; en otras palabras, es un producto de sumas o un AND de OR . Como forma normal canónica , es útil en la demostración automática de teoremas y la teoría de circuitos .

En la demostración automatizada de teoremas, la noción de " forma normal clausal " se utiliza a menudo en un sentido más estricto, es decir, una representación particular de una fórmula CNF como un conjunto de conjuntos de literales.

Definición

Se considera que una fórmula lógica está en CNF si es una conjunción de una o más disyunciones de uno o más literales . Al igual que en la forma normal disyuntiva (DNF), los únicos operadores proposicionales en CNF son o ( ), y ( ), y no ( ). El operador no solo se puede usar como parte de un literal, lo que significa que solo puede preceder a una variable proposicional . ${\displaystyle \vee }$ ${\displaystyle \wedge }$ ${\displaystyle \neg }$

La siguiente es una gramática libre de contexto para CNF:

1. CNF → ( Disyunción ) CNF ${\displaystyle \land }$
2. CNF → ( Disyunción )
3. Disyunción → Disyunción literal ${\displaystyle \lor }$
4. Disyunción → Literal
5. Literal → Variable ${\displaystyle \neg }$
6. Literal → Variable

Donde Variable es cualquier variable.

Todas las siguientes fórmulas en las variables , y están en forma normal conjuntiva: ${\displaystyle A,B,C,D,E}$ ${\displaystyle F}$

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F\lor D\lor F)}$
• ${\displaystyle (A\lor B)\land (C)}$
• ${\displaystyle (A\lor B)}$
• ${\displaystyle (A)}$

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

• ${\displaystyle \neg (A\land B)}$, ya que un AND está anidado dentro de un NOT
• ${\displaystyle \neg (A\lor B)\land C}$, ya que un OR está anidado dentro de un NOT
• ${\displaystyle A\land (B\lor (D\land E))}$, ya que un AND está anidado dentro de un OR

Conversión a CNF

En la lógica clásica, cada fórmula proposicional se puede convertir en una fórmula equivalente que esté en CNF. ^[1] Esta transformación se basa en reglas sobre equivalencias lógicas : eliminación de doble negación , leyes de De Morgan y la ley distributiva .

Algoritmo básico

El algoritmo para calcular un equivalente CNF de una fórmula proposicional dada se basa en la forma normal disyuntiva (DNF) : paso 1. ^[2] Luego se convierte a intercambiando AND con OR y viceversa mientras se niegan todos los literales. Eliminar todos los . ^[1] ${\displaystyle \phi }$ ${\displaystyle \lnot \phi }$
${\displaystyle \lnot \phi _{DNF}}$ ${\displaystyle \phi _{CNF}}$ ${\displaystyle \lnot \lnot }$

Conversión por medios sintácticos

Convierte a CNF la fórmula proposicional . ${\displaystyle \phi }$

Paso 1 : Convertir su negación a forma normal disyuntiva. ^[2]

${\displaystyle \lnot \phi _{DNF}=(C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})}$, ^[a]

donde cada uno es una conjunción de literales . ^[b] ${\displaystyle C_{i}}$ ${\displaystyle l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}}}$

Paso 2 : Niega . Luego, desplaza hacia adentro aplicando las equivalencias de De Morgan (generalizadas) hasta que ya no sea posible. donde ${\displaystyle \lnot \phi _{DNF}}$ ${\displaystyle \lnot }$ $${\displaystyle {\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot (C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})\\&\leftrightarrow \lnot C_{1}\land \lnot C_{2}\land \ldots \land \lnot C_{i}\land \ldots \land \lnot C_{m}&&{\text{// (generalized) D.M.}}\end{aligned}}}$$ $${\displaystyle {\begin{aligned}\lnot C_{i}&=\lnot (l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}})\\&\leftrightarrow (\lnot l_{i1}\lor \lnot l_{i2}\lor \ldots \lor \lnot l_{in_{i}})&&{\text{// (generalized) D.M.}}\end{aligned}}}$$

Paso 3 : Eliminar todas las dobles negaciones.

Ejemplo

Convertir a CNF la fórmula proposicional . ^[c] ${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$

El equivalente DNF (completo) de su negación es ^[2]
${\displaystyle \lnot \phi _{DNF}=(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)}$

$${\displaystyle {\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot \{(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)\}\\&\leftrightarrow {\underline {\lnot (p\land q\land r)}}\land {\underline {\lnot (p\land q\land \lnot r)}}\land {\underline {\lnot (p\land \lnot q\land \lnot r)}}\land {\underline {\lnot (\lnot p\land q\land \lnot r)}}&&{\text{// generalized D.M. }}\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor \lnot \lnot r)\land (\lnot p\lor \lnot \lnot q\lor \lnot \lnot r)\land (\lnot \lnot p\lor \lnot q\lor \lnot \lnot r)&&{\text{// generalized D.M. }}(4\times )\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)&&{\text{// remove all }}\lnot \lnot \\&=\phi _{CNF}\end{aligned}}}$$

Conversión por medios semánticos

Se puede derivar un equivalente CNF de una fórmula a partir de su tabla de verdad . Nuevamente, considere la fórmula . ^[c] $${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$$

La tabla de verdad correspondiente es

Un equivalente CNF de es ${\displaystyle \phi }$ $${\displaystyle (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)}$$

Cada disyunción refleja una asignación de variables para las cuales se evalúa como F(también). Si en dicha asignación una variable ${\displaystyle \phi }$
${\displaystyle V}$

• es Verdadero, entonces el literal se establece en la disyunción, ${\displaystyle \lnot V}$
• es F(alse), entonces el literal se establece en la disyunción. ${\displaystyle V}$

Otros enfoques

Dado que todas las fórmulas proposicionales se pueden convertir en una fórmula equivalente en forma normal conjuntiva, las demostraciones a menudo se basan en el supuesto de que todas las fórmulas son CNF. Sin embargo, en algunos casos esta conversión a CNF puede conducir a una explosión exponencial de la fórmula. Por ejemplo, traducir la fórmula no CNF

$${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \ldots \vee (X_{n}\wedge Y_{n})}$$

en CNF produce una fórmula con cláusulas: ${\displaystyle 2^{n}}$

$${\displaystyle (X_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge \ldots \wedge (Y_{1}\vee Y_{2}\vee \ldots \vee Y_{n}).}$$

Cada cláusula contiene o para cada . ${\displaystyle X_{i}}$ ${\displaystyle Y_{i}}$ ${\displaystyle i}$

Existen transformaciones en CNF que evitan un aumento exponencial del tamaño al preservar la satisfacibilidad en lugar de la equivalencia . ^{[3] [4]} Se garantiza que estas transformaciones solo aumentarán linealmente el tamaño de la fórmula, pero introducirán nuevas variables. Por ejemplo, la fórmula anterior se puede transformar en CNF agregando variables de la siguiente manera: ${\displaystyle Z_{1},\ldots ,Z_{n}}$

$${\displaystyle (Z_{1}\vee \ldots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \ldots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).}$$

Una interpretación satisface esta fórmula sólo si al menos una de las nuevas variables es verdadera. Si esta variable es , entonces tanto como son verdaderas también. Esto significa que cada modelo que satisface esta fórmula también satisface la original. Por otro lado, sólo algunos de los modelos de la fórmula original satisfacen esta: dado que no se mencionan en la fórmula original, sus valores son irrelevantes para la satisfacción de esta, lo que no es el caso en la última fórmula. Esto significa que la fórmula original y el resultado de la traducción son equisatisfacibles pero no equivalentes . ${\displaystyle Z_{i}}$ ${\displaystyle X_{i}}$ ${\displaystyle Y_{i}}$ ${\displaystyle Z_{i}}$

Una traducción alternativa, la transformación de Tseitin , incluye también las cláusulas . Con estas cláusulas, la fórmula implica ; a menudo se considera que esta fórmula "define" un nombre para . ${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$ ${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$ ${\displaystyle Z_{i}}$ ${\displaystyle X_{i}\wedge Y_{i}}$

Número máximo de disyunciones

Consideremos una fórmula proposicional con variables, . ${\displaystyle n}$ ${\displaystyle n\geq 1}$

Hay posibles literales: . ${\displaystyle 2n}$ ${\displaystyle L=\{p_{1},\lnot p_{1},p_{2},\lnot p_{2},\ldots ,p_{n},\lnot p_{n}\}}$

${\displaystyle L}$tiene subconjuntos no vacíos. ^[d] ${\displaystyle (2^{2n}-1)}$

Este es el número máximo de disyunciones que puede tener una CNF. ^[e]

Todas las combinaciones veritativas-funcionales se pueden expresar con disyunciones, una por cada fila de la tabla de verdad. En el ejemplo siguiente, están subrayadas. ${\displaystyle 2^{n}}$

Ejemplo

Consideremos una fórmula con dos variables y . ${\displaystyle p}$ ${\displaystyle q}$

La CNF más larga posible tiene disyunciones: ^[e] ${\displaystyle 2^{(2\times 2)}-1=15}$ $${\displaystyle {\begin{array}{lcl}(\lnot p)\land (p)\land (\lnot q)\land (q)\land \\(\lnot p\lor p)\land {\underline {(\lnot p\lor \lnot q)}}\land {\underline {(\lnot p\lor q)}}\land {\underline {(p\lor \lnot q)}}\land {\underline {(p\lor q)}}\land (\lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q)\land (\lnot p\lor p\lor q)\land (\lnot p\lor \lnot q\lor q)\land (p\lor \lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q\lor q)\end{array}}}$$

Esta fórmula es una contradicción .

Complejidad computacional

Un conjunto importante de problemas en la complejidad computacional implica encontrar asignaciones a las variables de una fórmula booleana expresada en forma normal conjuntiva, de modo que la fórmula sea verdadera. El problema k -SAT es el problema de encontrar una asignación satisfactoria a una fórmula booleana expresada en CNF en la que cada disyunción contiene como máximo k variables. 3-SAT es NP-completo (como cualquier otro problema k -SAT con k >2) mientras que se sabe que 2-SAT tiene soluciones en tiempo polinomial . Como consecuencia, ^[f] la tarea de convertir una fórmula en una DNF , preservando la satisfacibilidad, es NP-difícil ; dually , convertir en CNF, preservando la validez , también es NP-difícil; por lo tanto, la conversión preservando la equivalencia en DNF o CNF es nuevamente NP-difícil.

Los problemas típicos en este caso son las fórmulas en "3CNF": forma normal conjuntiva con no más de tres variables por conjunto. Los ejemplos de este tipo de fórmulas que se encuentran en la práctica pueden ser muy numerosos, por ejemplo, con 100.000 variables y 1.000.000 de conjuntos.

Una fórmula en CNF se puede convertir en una fórmula equisatisfacible en " k CNF" (para k ≥3) reemplazando cada conjunción con más de k variables por dos conjunciones y con Z una nueva variable, y repitiendo tantas veces como sea necesario. ${\displaystyle X_{1}\vee \ldots \vee X_{k}\vee \ldots \vee X_{n}}$ ${\displaystyle X_{1}\vee \ldots \vee X_{k-1}\vee Z}$ ${\displaystyle \neg Z\vee X_{k}\lor \ldots \vee X_{n}}$

Lógica de primer orden

En lógica de primer orden, la forma normal conjuntiva se puede llevar más allá para obtener la forma normal clausal de una fórmula lógica, que luego se puede utilizar para realizar una resolución de primer orden . En la demostración automatizada de teoremas basada en resolución, una fórmula CNF

Vea un ejemplo a continuación.

Conversión desde la lógica de primer orden

Para convertir la lógica de primer orden a CNF: ^[5]

1. Convertir a forma normal de negación .
   1. Eliminar implicaciones y equivalencias: reemplazar repetidamente con ; reemplazar con . Con el tiempo, esto eliminará todas las apariciones de y . ${\displaystyle P\rightarrow Q}$ ${\displaystyle \lnot P\lor Q}$ ${\displaystyle P\leftrightarrow Q}$ ${\displaystyle (P\lor \lnot Q)\land (\lnot P\lor Q)}$ ${\displaystyle \rightarrow }$ ${\displaystyle \leftrightarrow }$
   2. Mueva los NOT hacia adentro aplicando repetidamente la ley de De Morgan . Específicamente, reemplace con ; reemplace con ; y reemplace con ; reemplace con ; con . Después de eso, a puede aparecer solo inmediatamente antes de un símbolo de predicado. ${\displaystyle \lnot (P\lor Q)}$ ${\displaystyle (\lnot P)\land (\lnot Q)}$ ${\displaystyle \lnot (P\land Q)}$ ${\displaystyle (\lnot P)\lor (\lnot Q)}$ ${\displaystyle \lnot \lnot P}$ ${\displaystyle P}$ ${\displaystyle \lnot (\forall xP(x))}$ ${\displaystyle \exists x\lnot P(x)}$ ${\displaystyle \lnot (\exists xP(x))}$ ${\displaystyle \forall x\lnot P(x)}$ ${\displaystyle \lnot }$
2. Estandarizar variables
   1. En el caso de oraciones como las que usan el mismo nombre de variable dos veces, cambie el nombre de una de las variables. Esto evita confusiones posteriores al eliminar cuantificadores. Por ejemplo, se cambia el nombre a . ${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$ ${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]}$ ${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]}$
3. Skolemizar la declaración
   1. Mueva los cuantificadores hacia afuera: reemplace repetidamente con ; reemplace con ; reemplace con ; reemplace con . Estos reemplazos preservan la equivalencia, ya que el paso de estandarización de variables anterior aseguró que no ocurra en . Después de estos reemplazos, un cuantificador puede aparecer solo en el prefijo inicial de la fórmula, pero nunca dentro de un , o . ${\displaystyle P\land (\forall xQ(x))}$ ${\displaystyle \forall x(P\land Q(x))}$ ${\displaystyle P\lor (\forall xQ(x))}$ ${\displaystyle \forall x(P\lor Q(x))}$ ${\displaystyle P\land (\exists xQ(x))}$ ${\displaystyle \exists x(P\land Q(x))}$ ${\displaystyle P\lor (\exists xQ(x))}$ ${\displaystyle \exists x(P\lor Q(x))}$ ${\displaystyle x}$ ${\displaystyle P}$ ${\displaystyle \lnot }$ ${\displaystyle \land }$ ${\displaystyle \lor }$
   2. Reemplace repetidamente con , donde es un nuevo símbolo de función -aria, una denominada " función de Skolem ". Este es el único paso que conserva únicamente la satisfacibilidad en lugar de la equivalencia. Elimina todos los cuantificadores existenciales. ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)}$ ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))}$ ${\displaystyle f}$ ${\displaystyle n}$
4. Abandone todos los cuantificadores universales.
5. Distribuir OR hacia adentro sobre AND: reemplazar repetidamente con . ${\displaystyle P\lor (Q\land R)}$ ${\displaystyle (P\lor Q)\land (P\lor R)}$

Ejemplo

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 CNF (y posteriormente en forma de cláusula en la última línea) de la siguiente manera (resaltando las reglas de reemplazo redexes en ): ${\displaystyle {\color {red}{\text{red}}}}$

De manera informal, se puede pensar que la función Skolem da como resultado la persona que ama, mientras que da como resultado el animal (si lo hay) que no ama. La tercera última línea desde abajo se lee como " no ama al animal , o bien es amado por " . ${\displaystyle g(x)}$ ${\displaystyle x}$ ${\displaystyle f(x)}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle f(x)}$ ${\displaystyle x}$ ${\displaystyle g(x)}$

La segunda última línea desde arriba, , es el CNF. ${\displaystyle (\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))}$

Véase también

• Forma normal algebraica
• Dualidad conjunción/disyunción
• Forma normal disyuntiva
• Cláusula Horn : Una cláusula Horn es una cláusula disyuntiva (una disyunción de literales ) con como máximo un literal positivo, es decir , no negado .
• Algoritmo de Quine-McCluskey

Notas

1. número máximo de conjunciones para ${\displaystyle 1\leq m\leq }$ ${\displaystyle \phi }$
2. número máximo de literales para ${\displaystyle 1\leq in_{i}\leq }$ ${\displaystyle \phi }$
3. = (( NO (p Y q)) SI FALSO (( NO r) N Y (p XOR q))) ${\displaystyle \phi }$
4. ${\displaystyle \left|{\mathcal {P}}(L)\right|=2^{2n}}$
5. Se supone que no ocurren repeticiones y variaciones (como ) basadas en la conmutatividad y asociatividad de y . ${\displaystyle (a\land b)\lor (b\land a)\lor (a\land b\land b)}$ ${\displaystyle \lor }$ ${\displaystyle \land }$
6. dado que una forma de comprobar la satisfacibilidad de una CNF es convertirla en una DNF , cuya satisfacibilidad se puede comprobar en tiempo lineal
7. número máximo de disyunciones número máximo de literales ${\displaystyle 1\leq m\leq }$
   ${\displaystyle 1\leq in_{i}\leq }$

Referencias

1. Howson 2005, pág. 46.
2. ver Forma normal disyuntiva § Conversión a DNF
3. Tseitín 1968.
4. Jackson y Sheridan 2004.
5. Russel y Norvig 2010, págs. 345–347, 9.5.1 Forma normal conjuntiva para lógica de primer orden.

• Andrews, Peter B. (2013). Introducción a la lógica matemática y la teoría de tipos: hacia la verdad a través de la prueba . Springer. ISBN 978-9401599344.
• Howson, Colin (11 de octubre de 2005) [1997]. Lógica con árboles: una introducción a la lógica simbólica. Routledge. ISBN 978-1-134-78550-6.
• Jackson, Paul; Sheridan, Daniel (10 de mayo de 2004). "Conversiones de la forma de cláusula para circuitos booleanos" (PDF) . En Hoos, Holger H.; Mitchell, David G. (eds.). Teoría y aplicaciones de las pruebas de satisfacibilidad . 7.ª Conferencia internacional sobre teoría y aplicaciones de las pruebas de satisfacibilidad, SAT. Documentos seleccionados revisados. Notas de clase en informática. Vol. 3542. Vancouver, BC, Canadá: Springer 2005. pp. 183–198. doi :10.1007/11527695_15. ISBN 978-3-540-31580-3.
• Kleine Büning, Hans; Lettmann, Theodor (28 de agosto de 1999). Lógica proposicional: deducción y algoritmos. Cambridge University Press . ISBN 978-0-521-63017-7.
• Russel, Stuart ; Norvig, Peter , eds. (2010) [1995]. Inteligencia artificial: un enfoque moderno (PDF) (3.ª ed.). Upper Saddle River, NJ: Prentice Hall. ISBN 978-0-13-604259-4. Archivado (PDF) del original el 31 de agosto de 2017.
• Tseitin, Grigori S. (1968). "Sobre la complejidad de la derivación en el cálculo proposicional" (PDF) . En Slisenko, AO (ed.). Estructuras en matemáticas constructivas y lógica matemática, parte II, Seminarios de matemáticas (traducido del ruso) . Instituto Matemático Steklov. pp. 115–125.
• Whitesitt, J. Eldon (24 de mayo de 2012) [1961]. Álgebra de Boole y sus aplicaciones. Courier Corporation. ISBN 978-0-486-15816-7.

Enlaces externos

• "Forma normal conjuntiva", Enciclopedia de Matemáticas , EMS Press , 2001 [1994]

• "Herramienta Java para convertir una tabla de verdad en CNF y DNF". Universidad de Marburgo . Consultado el 31 de diciembre de 2023 .