Forma normal conjuntiva - Conjunctive normal form

Na lógica booleana , uma fórmula está na forma normal conjuntiva ( CNF ) ou na forma normal oracional se for uma conjunção de uma ou mais cláusulas , onde uma cláusula é uma disjunção de literais ; dito de outra forma, é um produto de somas ou um AND de ORs . Como uma forma normal canônica , é útil na prova automatizada de teoremas e na teoria dos circuitos .

Todas as conjunções de literais e todas as disjunções de literais estão em CNF, pois podem ser vistas como conjunções de cláusulas de um literal e conjunções de uma única cláusula, respectivamente. Como na forma normal disjuntiva (DNF), os únicos conectivos proposicionais que uma fórmula em CNF pode conter são e , ou , e não . O operador not só pode ser usado como parte de um literal, o que significa que só pode preceder uma variável proposicional ou um símbolo predicado .

Na prova automatizada de teoremas, a noção de " forma normal oracional " é freqüentemente usada em um sentido mais restrito, significando uma representação particular de uma fórmula CNF como um conjunto de conjuntos de literais.

Exemplos e não exemplos

Todas as fórmulas a seguir nas variáveis e estão na 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)}$
• ${\displaystyle (A\lor B)\land (C)}$
• ${\displaystyle (A\lor B)}$
• ${\displaystyle (A)}$

Para maior clareza, as cláusulas disjuntivas são escritas entre parênteses acima. Na forma normal disjuntiva com orações conjuntivas entre parênteses, o último caso é o mesmo, mas o penúltimo é . As constantes true e false são denotadas pelo conjunto vazio e por uma cláusula que consiste no disjunto vazio, mas normalmente são escritas explicitamente. ${\displaystyle (A)\lor (B)}$

As seguintes fórmulas não estão na forma normal conjuntiva:

• ${\displaystyle \neg (B\lor C)}$, uma vez que um OR está aninhado em um NOT
• ${\displaystyle (A\land B)\lor C}$
• ${\displaystyle A\land (B\lor (D\land E))}$, uma vez que um AND está aninhado em um OR

Cada fórmula pode ser escrita de forma equivalente como uma fórmula na forma normal conjuntiva. Os três não exemplos em CNF são:

• ${\displaystyle (\neg B)\land (\neg C)}$
• ${\displaystyle (A\lor C)\land (B\lor C)}$
• ${\displaystyle (A)\land (B\lor D)\land (B\lor E).}$

Conversão em CNF

Cada fórmula proposicional pode ser convertida em uma fórmula equivalente que está no CNF. Essa transformação é baseada em regras sobre equivalências lógicas : eliminação da dupla negação , leis de De Morgan e a lei distributiva .

Uma vez que todas as fórmulas proposicionais podem ser convertidas em uma fórmula equivalente na forma normal conjuntiva, as provas são freqüentemente baseadas na suposição de que todas as fórmulas são CNF. No entanto, em alguns casos, essa conversão para CNF pode levar a uma explosão exponencial da fórmula. Por exemplo, traduzir a seguinte fórmula não CNF em CNF produz uma fórmula com cláusulas: ${\displaystyle 2^{n}}$

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).}$

Em particular, a fórmula gerada é:

${\displaystyle (X_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge \cdots \wedge (Y_{1}\vee Y_{2}\vee \cdots \vee Y_{n}).}$

Esta fórmula contém cláusulas; cada cláusula contém um ou para cada um . ${\displaystyle 2^{n}}$${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle i}$

Existem transformações em CNF que evitam um aumento exponencial no tamanho, preservando a satisfatibilidade ao invés da equivalência . Essas transformações têm a garantia de aumentar apenas linearmente o tamanho da fórmula, mas introduzir novas variáveis. Por exemplo, a fórmula acima pode ser transformada em CNF adicionando variáveis ​​da seguinte maneira: ${\displaystyle Z_{1},\ldots ,Z_{n}}$

${\displaystyle (Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).}$

Uma interpretação satisfaz esta fórmula apenas se pelo menos uma das novas variáveis ​​for verdadeira. Se essa variável for , então e também são verdadeiros. Isso significa que todo modelo que satisfaz esta fórmula também satisfaz o original. Por outro lado, apenas alguns dos modelos da fórmula original satisfazem este: uma vez que os não são mencionados na fórmula original, seus valores são irrelevantes para sua satisfação, o que não é o caso na última fórmula. Isso significa que a fórmula original e o resultado da tradução são equivocáveis, mas não equivalentes . ${\displaystyle Z_{i}}$${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle Z_{i}}$

Uma tradução alternativa, a transformação Tseitin , inclui também as cláusulas . Com essas cláusulas, a fórmula implica ; esta fórmula é frequentemente considerada como "definir" um nome 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}}$

Lógica de primeira ordem

Na lógica de primeira ordem, a forma normal conjuntiva pode ser levada adiante para produzir a forma oracional normal de uma fórmula lógica, que pode então ser usada para realizar a resolução de primeira ordem . Na prova automatizada de teoremas baseada em resolução, uma fórmula CNF

${\displaystyle (}$

${\displaystyle l_{11}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{1n_{1}}}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \ldots }$

${\displaystyle \land }$

${\displaystyle (}$

${\displaystyle l_{m1}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{mn_{m}}}$

${\displaystyle )}$

, com literais, é comumente representado como um conjunto de conjuntos ${\displaystyle l_{ij}}$

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle l_{11}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{1n_{1}}}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle l_{m1}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{mn_{m}}}$

${\displaystyle \}}$

${\displaystyle \}}$

.

Veja abaixo um exemplo.

Complexidade computacional

Um importante conjunto de problemas na complexidade computacional envolve encontrar atribuições às variáveis ​​de uma fórmula booleana expressa na forma normal conjuntiva, de forma que a fórmula seja verdadeira. O problema k -SAT é o problema de encontrar uma atribuição satisfatória para uma fórmula booleana expressa em CNF em que cada disjunção contém no máximo k variáveis. 3-SAT é NP-completo (como qualquer outro k problema -SAT com k > 2), enquanto que 2-SAT é conhecido por ter soluções em tempo polinomial . Como consequência, a tarefa de converter uma fórmula em DNF , preservando a satisfatibilidade, é NP-difícil ; duplamente , converter em CNF, preservando a validade , também é NP-difícil; portanto, a conversão que preserva a equivalência em DNF ou CNF é novamente NP-difícil.

Os problemas típicos neste caso envolvem fórmulas em "3CNF": forma normal conjuntiva com não mais do que três variáveis ​​por conjunto. Os exemplos dessas fórmulas encontradas na prática podem ser muito grandes, por exemplo, com 100.000 variáveis ​​e 1.000.000 conjuntos.

Uma fórmula em CNF pode ser convertida em uma fórmula equisatisfatória em " k CNF" (para k ≥3) substituindo cada conjunto com mais de k variáveis por dois conjuntos e com Z uma nova variável, e repetindo quantas vezes for necessário. ${\displaystyle X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}}$${\displaystyle X_{1}\vee \cdots \vee X_{k-1}\vee Z}$${\displaystyle \neg Z\vee X_{k}\cdots \vee X_{n}}$

Conversão da lógica de primeira ordem

Para converter lógica de primeira ordem em CNF:

1. Converta para a forma normal de negação .
   1. Elimine implicações e equivalências: substitua repetidamente por ; substitua por . Eventualmente, isso eliminará todas as ocorrências de e .${\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. Mova as NOTs para dentro aplicando repetidamente a Lei de De Morgan . Especificamente, substitua por ; substitua por ; e substitua por ; substitua por ; com . Depois disso, a pode ocorrer apenas imediatamente antes de um 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. Padronizar variáveis
   1. Para frases como essas que usam o mesmo nome de variável duas vezes, altere o nome de uma das variáveis. Isso evita confusão posteriormente ao descartar quantificadores. Por exemplo, foi renomeado para .${\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. Skolemize a declaração
   1. Mova quantificadores para fora: substitua repetidamente por ; substitua por ; substitua por ; substitua por . Essas substituições preservam a equivalência, pois a etapa anterior de padronização de variáveis ​​garantiu que isso não ocorresse em . Após estas substituições, um quantificador pode ocorrer apenas no prefixo inicial da fórmula, mas não dentro de uma , ou .${\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. Substitua repetidamente por , onde está um novo símbolo de função -ary, uma chamada " função Skolem ". Esta é a única etapa que preserva apenas a satisfatibilidade ao invés da equivalência. Elimina todos os quantificadores existenciais.${\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. Abandone todos os quantificadores universais.
5. Distribuir ORs para dentro sobre ANDs: substitua repetidamente por .${\displaystyle P\lor (Q\land R)}$${\displaystyle (P\lor Q)\land (P\lor R)}$

Como exemplo, a fórmula que diz "Qualquer um que ama todos os animais, por sua vez é amado por alguém" é convertida em CNF (e, posteriormente, na forma de cláusula na última linha) da seguinte forma (destacando os redexes da regra de substituição em ): ${\displaystyle {\color {red}{\text{red}}}}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1,1

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1,1

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle \color {red}\lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 2

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

por 3,1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists z}}}$

${\displaystyle \exists y}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

por 3,1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

por 3,2

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

por 4

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle (}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle )}$

por 5

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

( representação de cláusula )

Informalmente, a função Skolem pode ser considerada como submissa à pessoa por quem é amada, enquanto cede o animal (se houver) que não ama. A 3ª última linha abaixo diz " não ama o animal , ou então é amado por " . ${\displaystyle g(x)}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle g(x)}$

A 2ª última linha acima ,, é o 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))}$

Notas

Veja também

• Forma normal algébrica
• Forma normal disjuntiva
• Cláusula de chifre
• Algoritmo Quine-McCluskey

Referências

• J. Eldon Whitesitt (24 de maio de 2012). Álgebra booleana e suas aplicações . Courier Corporation. ISBN 978-0-486-15816-7.
• Hans Kleine Büning; Theodor Lettmann (28 de agosto de 1999). Lógica proposicional: dedução e algoritmos . Cambridge University Press. ISBN 978-0-521-63017-7.
• Paul Jackson, Daniel Sheridan: Conversões de forma de cláusula para circuitos booleanos . In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, maio 10-13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198
• GS Tseitin: Sobre a complexidade da derivação no cálculo proposicional . In: Slisenko, AO (ed.) Structures in Constructive Mathematics and Mathematical Logic, Parte II, Seminars in Mathematics (traduzido do russo), pp. 115-125. Steklov Mathematical Institute (1968)

links externos

• "Forma normal conjuntiva" , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• Applet Java para conversão para CNF e DNF, mostrando as leis usadas