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 otro modo, 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 .
Todas las conjunciones de literales y todas las disyunciones de literales están en CNF, ya que pueden verse como conjunciones de cláusulas de un literal y conjunciones de una cláusula única, respectivamente. Como en la forma normal disyuntiva (DNF), los únicos conectivos proposicionales que puede contener una fórmula en CNF son y , o , 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 o un símbolo de predicado .
En la demostración automatizada de teoremas, la noción " forma normal clausal " se usa 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.
Ejemplos y no ejemplos
Todas las siguientes fórmulas en las variables , y están en forma conjuntiva normal:
Para mayor claridad, las cláusulas disyuntivas están escritas entre paréntesis arriba. En forma normal disyuntiva con cláusulas conjuntivas entre paréntesis, el último caso es el mismo, pero el penúltimo es. Las constantes verdadero y falso se indican mediante la conjunción vacía y una cláusula que consta de la disyunción vacía, pero normalmente se escriben explícitamente. [1]
Las siguientes fórmulas no están en forma conjuntiva normal:
- , ya que un OR está anidado dentro de un NOT
- , ya que un AND está anidado dentro de un OR
Cada fórmula se puede escribir de forma equivalente como una fórmula en forma normal conjuntiva. Los tres no ejemplos en CNF son:
Conversión a CNF
[2] Toda fórmula proposicional se puede convertir en unafórmula equivalente que está en CNF. Esta transformación se basa en reglas sobre equivalencias lógicas : eliminación de la doble negación , leyes de De Morgan y ley distributiva .
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, la traducción de la siguiente fórmula que no es CNF a CNF produce una fórmula con cláusulas:
En particular, la fórmula generada es:
Esta fórmula contiene cláusulas; cada cláusula contiene o para cada .
Existen transformaciones en CNF que evitan un aumento exponencial de tamaño al preservar la satisfacibilidad en lugar de la equivalencia . [3] [4] Estas transformaciones están garantizadas para aumentar solo linealmente el tamaño de la fórmula, pero introducen nuevas variables. Por ejemplo, la fórmula anterior se puede transformar en CNF agregando variables como sigue:
Una interpretación satisface esta fórmula solo si al menos una de las nuevas variables es verdadera. Si esta variable es, entonces ambos y son ciertas también. Esto significa que todo modelo que satisface esta fórmula también satisface al original. Por otro lado, solo algunos de los modelos de la fórmula original satisfacen esta: dado que lano se mencionan en la fórmula original, sus valores son irrelevantes para su satisfacción, 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 equisatisfactorios pero no equivalentes .
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" ser un nombre para .
Lógica de primer orden
En la 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 una resolución de primer orden . En la demostración automatizada de teoremas basada en resolución, una fórmula CNF
, con literales, se representa comúnmente como un conjunto de conjuntos | |||||||||||||||||||
. |
Vea a continuación un ejemplo.
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 de k -SAT con k > 2) mientras que se sabe que 2-SAT tiene soluciones en tiempo polinomial . Como consecuencia, [5] la tarea de convertir una fórmula en un DNF , preservando la satisfacibilidad, es NP-difícil ; doblemente , convertir a CNF, preservando la validez , también es NP-hard; por tanto, la conversión que conserva la equivalencia en DNF o CNF es de nuevo NP-hard.
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 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 equisatisfactable 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.
Conversión de lógica de primer orden
Para convertir la lógica de primer orden a CNF: [2]
- Convierta a la forma normal de negación .
- Eliminar implicaciones y equivalencias: reemplazar repetidamente con ; reemplazar con . Eventualmente, esto eliminará todas las apariciones de y .
- Mueva los NOT hacia adentro aplicando repetidamente la ley de De Morgan . Específicamente, reemplace con ; reemplazar con ; y reemplazar con ; reemplazar con ; con . Después de eso, un puede aparecer sólo inmediatamente antes de un símbolo de predicado.
- Estandarizar variables
- Para oraciones como que utilizan el mismo nombre de variable dos veces, cambie el nombre de una de las variables. Esto evita confusiones posteriores al descartar cuantificadores. Por ejemplo, se renombra a .
- Skolemize la declaración
- Mueva los cuantificadores hacia afuera: reemplace 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 no ocurre en . Después de estos reemplazos, un cuantificador puede ocurrir solo en el prefijo inicial de la fórmula, pero nunca dentro de un, , o .
- Reemplazar repetidamente con , dónde es un nuevo -símbolo de función aria, una denominada " función Skolem ". Este es el único paso que conserva solo la satisfacibilidad en lugar de la equivalencia. Elimina todos los cuantificadores existenciales.
- Suelta todos los cuantificadores universales.
- Distribuya los OR hacia adentro sobre los AND: reemplace repetidamente con .
A modo de ejemplo, la fórmula que dice "Cualquiera que ama a todos los animales, a su vez es amado por alguien" se convierte en CNF (y posteriormente en forma de cláusula en la última línea) de la siguiente manera (resaltando la regla de reemplazo redexes en):
por 1.1 | ||||||||||||||||||||||||||||||||||||
por 1.1 | ||||||||||||||||||||||||||||||||||||
por 1.2 | ||||||||||||||||||||||||||||||||||||
por 1.2 | ||||||||||||||||||||||||||||||||||||
por 1.2 | ||||||||||||||||||||||||||||||||||||
por 2 | ||||||||||||||||||||||||||||||||||||
por 3,1 | ||||||||||||||||||||||||||||||||||||
por 3,1 | ||||||||||||||||||||||||||||||||||||
por 3.2 | ||||||||||||||||||||||||||||||||||||
por 4 | ||||||||||||||||||||||||||||||||||||
por 5 | ||||||||||||||||||||||||||||||||||||
( representación de cláusula ) |
De manera informal, la función Skolem puede pensarse que cede a la persona por quien es amado, mientras produce el animal (si lo hay) que no ama. La tercera última línea de abajo se lee como " no ama al animal , si no es amado por " .
La segunda última línea desde arriba, , es el CNF.
Notas
- ^ Peter B. Andrews, Introducción a la lógica matemática y la teoría de tipos , 2013, ISBN 9401599343 , p. 48
- ^ a b Inteligencia artificial: un enfoque moderno Archivado el 31 de agosto de 2017 en la Wayback Machine [1995 ...] Russell y Norvig
- ^ Tseitin (1968)
- ^ Jackson y Sheridan (2004)
- ^ dado que una forma de verificar la satisfacción de un CNF es convertirlo en un DNF , cuya satisfacción se puede verificar en tiempo lineal
Ver también
- Forma normal algebraica
- Forma normal disyuntiva
- Cláusula de cuerno
- Algoritmo de Quine-McCluskey
Referencias
- J. Eldon Whitesitt (24 de mayo de 2012). Álgebra booleana y sus aplicaciones . Corporación de mensajería. ISBN 978-0-486-15816-7.
- Hans Kleine Büning; Theodor Lettmann (28 de agosto de 1999). Lógica proposicional: deducción y algoritmos . Prensa de la Universidad de Cambridge. ISBN 978-0-521-63017-7.
- Paul Jackson, Daniel Sheridan: Conversiones de forma de cláusula para circuitos booleanos . En: Holger H. Hoos, David G. Mitchell (Eds.): Teoría y aplicaciones de las pruebas de satisfacción, 7ª Conferencia Internacional, SAT 2004, Vancouver, BC, Canadá, 10 al 13 de mayo de 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, págs. 183–198
- GS Tseitin: Sobre la complejidad de la derivación en el cálculo proposicional . En: Slisenko, AO (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (traducido del ruso), págs. 115-125. Instituto de Matemáticas Steklov (1968)
enlaces externos
- "Forma normal conjuntiva" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
- Applet de Java para convertir a CNF y DNF, que muestra las leyes utilizadas