Forma normal disjuntiva

Na lógica booleana, uma forma normal disjuntiva (FND) é uma normalização de uma fórmula lógica a qual é uma disjunção de cláusulas conjuntivas. Como uma forma normal, a FND é útil em provas automáticas de teoremas. Uma fórmula lógica é considerada uma FND se, e somente se, fôr uma disjunção de uma ou mais conjunções de um ou mais literais. Como na forma normal conjuntiva (FNC), os únicos operadores proposicionais na FND são e, ou e não. O operador não pode ser usado apenas como parte de um literal, o qual significa que pode apenas preceder uma variável proposicional. Por exemplo, todas as seguintes fórmulas estão na FND:

$A\lor B$

$A\!$

$(A\land B)\lor C$

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

$(A\wedge B\wedge \neg C)\vee (B\wedge \neg D\wedge \neg E)\vee (A\wedge F)$

Todavia, as seguintes fórmulas não estão na FND:

$\neg (A\lor B)$ — NÃO é o operador mais extremo

$A\lor (B\land (C\lor D))$ — um OU está aninhado com um E

A conversão de uma fórmula para FND envolve o uso de equivalências lógicas, tais como eliminação de duplo negativo, Leis de De Morgan, e a distributividade. Note que todas as fórmulas lógicas podem ser convertidas em forma normal disjuntiva. Contudo, em alguns casos, essa conversão para FND pode levar para uma explosão exponencial da fórmula. Por exemplo, na FND, fórmulas lógicas das seguintes formas têm $2^{n}$ termos:

$(X_{1}\lor Y_{1})\land (X_{2}\lor Y_{2})\land \dots \land (X_{n}\lor Y_{n})$

A seguinte fórmula é uma gramática formal para FND:

1. <ou> → ∨

2. <e> → ∧

3. <não> → ¬

4. <disjunção> → <conjunção>

5. <disjunção> → <disjunção> <ou> <conjunção>

6. <conjunção> → <literal>

7. <conjunção> → (<conjunção> <e> <literal>)

8. <literal> → <termo>

9. <literal> → <não><termo>

Onde <termo> é qualquer variável.

Ver também

• Forma Normal Algébrica
• Álgebra booleana
• Função de Valor Booleano
• Forma Normal Conjuntiva
• Forma Normal Implicativa
• Cláusula de Horn
• Diagrama de Pierce
• Algoritmo de Quine-McCluskey
• Tabela verdade
• Lógica de Ordem Zero