forma normal conjuntiva

En álgebra booleana , una fórmula está en forma normal conjuntiva ( FNC ) 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 otro modo, es un producto de sumas o un AND de OR .

En la demostración automatizada de teoremas , la noción de " forma normal clausal " se usa a menudo en un sentido más restringido, refiriéndose a una representación particular de una fórmula en forma normal clausal como un conjunto de conjuntos de literales.

Definición

Una fórmula lógica se considera en forma normal conjuntiva (FNC) 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 (FND), los únicos operadores proposicionales en FNC son o ( $\vee$ ), y ( $\land$ ), y no ( $\neg$ ). El operador not solo puede usarse como parte de un literal, lo que significa que solo puede preceder a una variable proposicional .

La siguiente es una gramática libre de contexto para la forma normal de contexto (FNC):

CNF

\,\to \,

Desunido

\,\mid \,

Desunido

\,\land \,

CNF

Desunido

\,\to \,

Literal

\,\mid \,

Literal

\,\lor \,

Desunido

Literal

\,\to \,

Variable

\,\mid \,

\,\neg \,

Variable

Donde Variable es cualquier variable.

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

$(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)$
$(A\lor B)\land (C)$
$(A\lor B)$
$(A)$

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

$\neg (A\land B)$ , ya que un AND está anidado dentro de un NOT
$\neg (A\lor B)\land C$ , ya que un OR está anidado dentro de un NOT
$A\land (B\lor (D\land E))$ , ya que un AND está anidado dentro de un OR
$A\land (B\lor (C\lor D))$ , ya que un OR anidado debe escribirse sin paréntesis

Conversión a FNC

En lógica clásica, cada fórmula proposicional puede convertirse en una fórmula equivalente que está en FNC. ^{[ 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 en forma normal conjuntiva (FNC) de una fórmula proposicional dada. $\phi$ se basa en $\lnot \phi$ en forma normal disyuntiva (FND) : paso 1. ^{[ 2 ]} Entonces $\lnot \phi _{DNF}$ se convierte en $\phi _{CNF}$ intercambiando AND con OR y viceversa mientras se niegan todos los literales. Eliminar todo $\lnot \lnot$ . ^{[ 1 ]}

Conversión por medios sintácticos

Convierta la fórmula proposicional a FNC $\phi$ .

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

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

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

Paso 2 : Negar $\lnot \phi _{DNF}$ Luego cambia. $\lnot$ hacia adentro aplicando las equivalencias (generalizadas) de De Morgan hasta que ya no sea posible. ${\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{// DM (generalizado)}}\end{aligned}}$ dónde ${\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{// DM (generalizado)}}\end{aligned}}$

Paso 3 : Eliminar todas las negaciones dobles.

Ejemplo

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

El equivalente DNF (completo) de su negación es ^{[ 2 ]} $\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)$

${\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 en forma normal conjuntiva (FNC) de una fórmula a partir de su tabla de verdad . Consideremos nuevamente la fórmula. $\phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))$ . ^{[ 5 ]}

La tabla de verdad correspondiente es

Un equivalente CNF de $\phi$ es $(\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 $\phi$ se evalúa como F(alse). Si en dicha asignación una variable $V$

es T(verdadero), entonces el literal se establece en $\lnot V$ en la disyunción,
es F(alse), entonces el literal se establece en $V$ en la disyunción.

Otros enfoques

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

$(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 $2^{n}$ cláusulas:

$(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 $X_{i}$ o $Y_{i}$ para cada $i$ .

Existen transformaciones a FNC que evitan un aumento exponencial del tamaño al preservar la satisfacibilidad en lugar de la equivalencia . ^{[ 6 ]}^{[ 7 ]} Estas transformaciones garantizan que el tamaño de la fórmula solo aumente linealmente, pero introducen nuevas variables. Por ejemplo, la fórmula anterior se puede transformar a FNC añadiendo variables. $Z_{1},\ldots ,Z_{n}$ como sigue:

$(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 solo si al menos una de las nuevas variables es verdadera. Si esta variable es verdadera, $Z_{i}$ , entonces ambos $X_{i}$ y $Y_{i}$ También son ciertas. Esto significa que cada modelo que satisface esta fórmula también satisface la original. Por otro lado, solo algunos de los modelos de la fórmula original satisfacen esta: puesto que $Z_{i}$ Como no se mencionan en la fórmula original, sus valores son irrelevantes para su satisfacción, lo cual 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 .

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

Número máximo de disyunciones

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

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

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

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

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

Ejemplo

Consideremos una fórmula con dos variables. $p$ y $q$ .

La CNF más larga posible tiene $2^{(2\times 2)}-1=15$ disyunciones: ^{[ 9 ]} ${\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 . Se puede simplificar a $(\neg p\land p)$ o para $(\neg q\land q)$ , que también son contradicciones, así como FNC válidas.

Complejidad computacional

Un conjunto importante de problemas en complejidad computacional implica encontrar asignaciones a las variables de una fórmula booleana expresada en forma normal conjuntiva, de tal manera 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, ^{[ 10 ]} la tarea de convertir una fórmula en una DNF , preservando la satisfacibilidad, es NP-difícil ; dualmente , convertirla en CNF, preservando la validez , también es NP-difícil; por lo tanto, la conversión que preserva la equivalencia a DNF o CNF es nuevamente NP-difícil.

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 tales fórmulas que se encuentran en la práctica pueden ser muy extensos, por ejemplo, con 100 000 variables y 1 000 000 de conjunciones.

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

Lógica de primer orden

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

Vea a continuación un ejemplo.

Conversión desde lógica de primer orden

Para convertir la lógica de primer orden a FNC: ^{[ 12 ]}

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

Ejemplo

Como 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 las reglas de reemplazo redexes en ${\color {red}{\text{red}}}$ ):

De manera informal, la función de Skolem $g(x)$ puede pensarse como ceder a la persona por quien $x$ es amado, mientras que $f(x)$ produce el animal (si lo hay) que $x$ no ama. La antepenúltima línea desde abajo dice entonces " $x$ no ama al animal $f(x)$ o de lo contrario $x$ es amado por $g(x)$ " .

La penúltima línea desde arriba, $(\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))$ , es la FNC.

Véase también

Forma normal algebraica
Dualidad conjunción/disyunción
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 2 Howson 2005 , pág. 46.
1 2 3 ver Forma normal disyuntiva § Conversión a FND
↑ $1\leq m\leq$ número máximo de conjunciones para $\phi$
↑ $1\leq in_{i}\leq$ número máximo de literales para $\phi$
1 2 $\phi$ = (( NO (p Y q)) SI Y SOLO SI (( NO r) NAND (p XOR q)))
↑ Tseitin 1968 .
↑ Jackson y Sheridan 2004 .
↑ $\left|{\mathcal {P}}(L)\right|=2^{2n}$
1 2 Se supone que las repeticiones y variaciones (como $(a\land b)\lor (b\land a)\lor (a\land b\land b)$ ) basado en la conmutatividad y asociatividad de $\lor$ y $\land$ no ocurren.
↑ ya que una forma de comprobar la satisfacibilidad de una CNF es convertirla en una DNF , cuya satisfacibilidad se puede comprobar en tiempo lineal.
↑ $1\leq m\leq$ número máximo de disyunciones $1\leq in_{i}\leq$ número máximo de literales
↑ Russel y Norvig 2010 , págs. 345–347, 9.5.1 Forma normal conjuntiva para la 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 demostración . 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 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 . Artículos seleccionados revisados. Lecture Notes in Computer Science. 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-4Archivado (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 booleana 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 a FNC y FND" . Universidad de Marburgo . Consultado el 31 de diciembre de 2023 .

[FOOTNOTEHowson200546-1] 1 2 Howson 2005 , pág. 46.

[dnf-2] 1 2 3 ver Forma normal disyuntiva § Conversión a FND

[3] $1\leq m\leq$ número máximo de conjunciones para $\phi$

[4] $1\leq in_{i}\leq$ número máximo de literales para $\phi$

[phiverbose-5] 1 2 $\phi$ = (( NO (p Y q)) SI Y SOLO SI (( NO r) NAND (p XOR q)))

[FOOTNOTETseitin1968-6] Tseitin 1968 .

[FOOTNOTEJacksonSheridan2004-7] Jackson y Sheridan 2004 .

[8] $\left|{\mathcal {P}}(L)\right|=2^{2n}$

[noreps-9] 1 2 Se supone que las repeticiones y variaciones (como $(a\land b)\lor (b\land a)\lor (a\land b\land b)$ ) basado en la conmutatividad y asociatividad de $\lor$ y $\land$ no ocurren.

[10] ya que una forma de comprobar la satisfacibilidad de una CNF es convertirla en una DNF , cuya satisfacibilidad se puede comprobar en tiempo lineal.

[11] $1\leq m\leq$ número máximo de disyunciones $1\leq in_{i}\leq$ número máximo de literales

[FOOTNOTERusselNorvig2010345–3479.5.1_Conjunctive_normal_form_for_first-order_logic-12] Russel y Norvig 2010 , págs. 345–347, 9.5.1 Forma normal conjuntiva para la lógica de primer orden.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 12 ]