Mostrar código-fonte de Forma normal conjuntiva

{{sem-fontes|data=Outubro de 2012}}
Na [[lógica]] [[Álgebra booleana|booleana]], uma [[fórmula]] está na '''forma normal conjuntiva''' (FNC) se é uma [[Conjunção lógica|conjunção]] de [[Cláusulas (Lógica)|cláusulas]], onde uma cláusula é uma [[Disjunção Lógica|disjunção]] de [[Literal (lógica)|literais]]. Sendo uma forma normal, a FNC é útil em [[demonstrações automáticas de teoremas]]. Ela é similar à [[forma canônica de produto de somas]] usada na [[teoria dos circuitos]].

Toda conjunção de literais e toda disjunção de literais estão na FNC, já que elas podem ser vistas como conjunções de cláusulas de um literal e conjunções de uma só cláusula, respectivamente. Assim como na [[forma normal disjuntiva]] (FND), os únicos conectivos proposicionais que uma fórmula na FNC pode conter são os operadores [[Conjunção lógica|e]], [[Disjunção lógica|ou]] e [[Negação|não]]. O operador [[Negação|não]] pode ser usado apenas como parte de um [[Literal (lógica)|literal]], e portanto ele pode aparecer apenas na frente de [[variáveis proposicionais]].

Por exemplo, todas as fórmulas seguintes estão na FNC:

:<math>A \wedge B</math>
:<math>\neg A \wedge (B \vee C)</math>
:<math>(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)</math>
:<math>(\neg B \vee C).</math>:

Porém, as seguintes fórmulas não estão:

:<math>\neg (B \vee C)</math>
:<math>(A \wedge B) \vee C</math>
:<math>A \wedge (B \vee (D \wedge E)).</math>

As três fórmulas acima são equivalentes respectivamente às três fórmulas seguintes que estão na forma normal conjuntiva:

:<math>\neg B \wedge \neg C</math>
:<math>(A \vee C) \wedge (B \vee C)</math>
:<math>A \wedge (B \vee D) \wedge (B \vee E).</math>

Toda fórmula proposicional pode ser convertida para uma fórmula [[equivalente]] que está na FNC.
Essa transformação é baseada em regras sobre [[equivalências lógicas]]: [[Eliminação da dupla negação|Lei da Dupla Negação]], [[Leis de De Morgan]], e a [[Distributividade]].

Uma vez que todas as fórmulas lógicas clássicas podem ser convertidas em fórmulas equivalentes na forma normal conjuntiva, muitas demonstrações são baseadas na suposição de que todas as fórmulas estão na FNC. Contudo, em alguns casos, essa conversão para FNC pode levar a uma explosão exponencial da fórmula. Por exemplo, traduzindo a seguinte fórmula que não está na FNC para FNC, obtemos uma fórmula com <math>2^n</math> cláusulas:

:<math>(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).</math>

A seguinte fórmula é uma gramática formal para FNC:
:1. <ou> → ∨
:2. <e> → ∧
:3. <não/negação> → ¬
:4. <conjunção> → <disjunção>
:5. <conjunção> → <conjunção> <e> <disjunção>
:6. <disjunção> → <literal>
:7. <disjunção> → (<disjunção> <ou> <literal>)
:8. <literal> → <termo>
:9. <literal> → <não><termo>

Onde <termo> é qualquer variável.

Existem transformações das fórmulas na FNC que preservam a [[satisfatibilidade]] ao invés da equivalência e não produzem um aumento exponencial do tamanho. Tais transformações aumentam o tamanho da fórmula apenas por um fator linear, mas introduzem novas variáveis.

A forma normal conjuntiva pode ser levada adiante de modo a produzir a [[forma normal clausal]] de uma fórmula lógica, a qual é usada para se efetuar [[Princípio da Resolução|resolução de primeira ordem]].

Um importante conjunto de problemas em [[complexidade computacional]] envolve encontrar atribuições para as variáveis de uma fórmula booleana expressa na Forma Normal Conjuntiva, tais que a fórmula seja [[Valoração (lógica)|satisfeita]]. O problema ''k''-SAT é o problema de encontrar uma atribuição que satisfaça para uma fórmula booleana expressa na FNC, tal que cada disjunção contenha no máximo k variáveis. [[Problema de satisfatibilidade booleana|3-SAT]] é [[NP-completo]] (assim como qualquer outro problema ''k''-SAT com k>2), enquanto [[2-SAT]] pode ser resolvido em [[tempo polinomial]].

== Ver também ==
* [[Forma normal da negação|Forma Normal Negativa]]
* [[Forma normal disjuntiva|Forma Normal Disjuntiva]]
* [[Forma Normal Implicativa]]
* [[Forma normal algébrica|Forma Normal Algébrica]]
* [[Cláusula de Horn]]
* [[Algoritmo de Quine-McCluskey]]

//

{{DEFAULTSORT:Forma Normal Conjuntiva}}
[[Categoria:Álgebra booliana]]