Forma conjuntiva normal
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 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.
Todas las fórmulas siguientes en las variables y están en forma normal conjuntiva:
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]
Cada fórmula se puede escribir de forma equivalente como una fórmula en forma normal conjuntiva. Los tres no ejemplos en CNF son: