Forma normal conjuntiva

Forma estándar de función booleana

En lógica booleana , una fórmula está en forma normal conjuntiva ( CNF ) o en forma normal clausal si es una conjunción de una o más cláusulas , donde una cláusula es una disyunción de literales ; Dicho de otra manera, es un producto de sumas o un AND de OR . Como forma normal canónica , es útil en la demostración automatizada de teoremas y en 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

Una fórmula lógica se considera en CNF si es una conjunción de una o más disyunciones de uno o más literales . Como en la forma normal disyuntiva (DNF), los únicos operadores proposicionales en CNF son o ( ), y ( ), y no ( ). El operador not solo puede usarse 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. Literales → Variables ${\displaystyle \neg }$
6. Literales → Variables

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 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 la 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 intercambiando AND con OR y viceversa mientras se niegan todos los literales. Eliminar todo . ^[1] ${\displaystyle \phi }$ ${\displaystyle \lnot \phi }$
${\displaystyle \lnot \phi _{DNF}}$ ${\displaystyle \phi _{CNF}}$ ${\displaystyle \lnot \lnot }$

Conversión por medios sintácticos

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

Paso 1 : convierte 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})}$, ^[3]

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

Paso 2 : Negar . Luego, muévase hacia adentro aplicando las equivalencias (generalizadas) de De Morgan hasta que ya no sea posible. ${\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}}}$

dónde
${\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 : Elimina todas las dobles negaciones.

Ejemplo

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

El equivalente (completo) DNF 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 . De nuevo, considere la fórmula

${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$. ^[5]

La tabla de verdad correspondiente es

Un equivalente de CNF 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 cuya evaluación es F(alse). Si en tal asignación una variable ${\displaystyle \phi }$
${\displaystyle V}$

• es T(rue), 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 pruebas 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 provocar 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 uno . ${\displaystyle X_{i}}$ ${\displaystyle Y_{i}}$ ${\displaystyle i}$

Existen transformaciones en CNF que evitan un aumento exponencial de tamaño al preservar la satisfacibilidad en lugar de la equivalencia . ^{[6] [7]} 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 ambos y también son verdaderos. 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 éste: dado que no se mencionan en la fórmula original, sus valores son irrelevantes para su satisfacción, lo que no ocurre 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" como 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

Considere 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. ^[8] ${\displaystyle (2^{2n}-1)}$

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

Todas las combinaciones de funciones de verdad se pueden expresar con disyunciones, una para cada fila de la tabla de verdad. En el siguiente ejemplo están subrayados. ${\displaystyle 2^{n}}$

Ejemplo

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

El CNF más largo posible tiene disyunciones: ^[10] ${\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 de 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 de k -SAT con k >2), mientras que se sabe que 2-SAT tiene soluciones en tiempo polinomial . Como consecuencia, ^[11] la tarea de convertir una fórmula en un DNF , preservando la satisfacibilidad, es NP-difícil ; dualmente , convertir a CNF, preservar la validez , también es NP-duro; por lo tanto, la conversión que preserva la equivalencia a DNF o CNF es nuevamente NP-duro.

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

Una fórmula en CNF se puede convertir en una fórmula equisatisfactible 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 la lógica de primer orden, la forma normal conjuntiva se puede llevar más lejos para producir 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 a continuación un ejemplo.

Conversión de lógica de primer orden

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

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, reemplácelo con ; reemplazar con ; y reemplazar con ; reemplazar con ; con . Después de eso, a puede aparecer sólo 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. Para 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 le 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: reemplácelos repetidamente con ; reemplazar con ; reemplazar con ; reemplazar con . Estos reemplazos preservan la equivalencia, ya que el paso anterior de estandarización de variables aseguró que eso no ocurriera en . Después de estos reemplazos, un cuantificador puede aparecer solo en el prefijo inicial de la fórmula, pero nunca dentro de , 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 hay un nuevo símbolo de función -aria, la llamada " función Skolem ". Este es el único paso que preserva sólo la satisfacibilidad y no 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. Elimina todos los cuantificadores universales.
5. Distribuya los OR hacia adentro sobre los AND: reemplácelos repetidamente con . ${\displaystyle P\lor (Q\land R)}$ ${\displaystyle (P\lor Q)\land (P\lor R)}$

Ejemplo

Como ejemplo, la fórmula que dice "Cualquiera que 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 redex en ): ${\displaystyle {\color {red}{\text{red}}}}$

Informalmente, se puede considerar que la función Skolem produce la persona que es amada, mientras que produce el animal (si lo hay) que no ama. La tercera y última línea desde abajo dice " no ama al animal , o es amado por " . ${\displaystyle g(x)}$ ${\displaystyle x}$ ${\displaystyle f(x)}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle f(x)}$ ${\displaystyle x}$ ${\displaystyle g(x)}$

La penú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))}$

Ver también

• Forma normal algebraica
• Forma normal disyuntiva
• Cláusula de Horn : una cláusula de 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. Howson 2005, pág. 46.
2. ver Forma normal disyuntiva#Conversión a DNF
3. número máximo de conjunciones para ${\displaystyle 1\leq m\leq }$ ${\displaystyle \phi }$
4. número máximo de literales para ${\displaystyle 1\leq in_{i}\leq }$ ${\displaystyle \phi }$
5. = (( NO (p Y q)) IFF (( NO r) NAND (p XOR q))) ${\displaystyle \phi }$
6. Tseitín 1968.
7. Jackson y Sheridan 2004.
8. ${\displaystyle \left|{\mathcal {P}}(L)\right|=2^{2n}}$
9. me gusta ${\displaystyle (a\land b)\lor (b\land a)\lor (a\land b\land b)}$
10. Se supone que las repeticiones y variaciones ^[9] basadas en la conmutatividad y asociatividad de y no ocurren. ${\displaystyle \lor }$ ${\displaystyle \land }$
11. dado que una forma de verificar la satisfacibilidad de un CNF es convertirlo en un DNF , cuya satisfacibilidad se puede verificar en tiempo lineal
12. número máximo de disyunciones número máximo de literales ${\displaystyle 1\leq m\leq }$
    ${\displaystyle 1\leq in_{i}\leq }$
13. Russel & Norvig 2010, págs. 345–347, 9.5.1 Forma normal conjuntiva para lógica de primer orden.

Referencias

• 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 . ISBN 9401599343.

• Howson, Colin (11 de octubre de 2005) [1997]. Lógica con árboles: una introducción a la lógica simbólica. Rutledge. ISBN 978-1-134-78550-6.

• Jackson, Pablo; Sheridan, Daniel (10 de mayo de 2004). "Conversiones de formularios de cláusulas para circuitos booleanos" (PDF) . En Hoos, Holger H.; Mitchell, David G. (eds.). Teoría y aplicaciones de las pruebas de satisfacción . VII Congreso Internacional sobre Teoría y Aplicaciones de las Pruebas de Satisfabilidad, SAT. Artículos seleccionados revisados. Apuntes de conferencias sobre informática. vol. 3542. Vancouver, BC, Canadá: Springer 2005. págs. 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. Prensa de la Universidad de Cambridge . ISBN 978-0-521-63017-7.

• Russell, Estuardo ; Norvig, Peter , eds. (2010) [1995]. Inteligencia artificial: un enfoque moderno (PDF) (3ª ed.). Upper Saddle River, Nueva Jersey: Prentice Hall. ISBN 978-0-13-604259-4. Archivado (PDF) desde el original el 31 de agosto de 2017.

• Tseitin, Grigori S. (1968). "Sobre la complejidad de la derivación en cálculo proposicional" (PDF) . En Slisenko, AO (ed.). Estructuras en Matemática Constructiva y Lógica Matemática, Parte II, Seminarios de Matemáticas (traducido del ruso) . Instituto de Matemáticas Steklov. págs. 115-125.

• Whitesitt, J. Eldon (24 de mayo de 2012) [1961]. Álgebra booleana y sus aplicaciones. Corporación de mensajería. 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 .