Editing Negation normal form

{{Short description|Logical formula with NOT only on variables}}
In [[mathematical logic]], a formula is in '''negation normal form''' ('''NNF''') if the [[negation]] operator (<math>\lnot</math>, {{smallcaps|not}}) is only applied to variables and the only other allowed [[Boolean algebra|Boolean operators]] are [[logical conjunction|conjunction]] (<math>\land</math>, {{smallcaps|and}}) and [[logical disjunction|disjunction]] (<math>\lor</math>, {{smallcaps|or}}). 

Negation normal form is not a [[canonical form]]: for example, <math>a \land (b\lor \lnot c)</math> and <math>(a \land b) \lor (a \land \lnot c)</math> are equivalent, and are both in negation normal form.

== Definition == 
The following is a [[context-free grammar]] for ''NNF'':
:{|
|-
| ''NNF'' || <math>\to</math> || ''Literal''
|-
|  || || {{spaces|1}}<math>\mid \quad</math>( ''NNF'' <math>\, \land \,</math> ''NNF'' {{spaces|1}})
|-
|  || || {{spaces|1}}<math>\mid \quad</math>( ''NNF'' <math>\, \lor \,</math> ''NNF'' {{spaces|1}})
|-
|
|-
| ''Literal'' || <math>\to</math> || ''Variable''
|-
|  || || {{spaces|1}}<math>\mid \quad \neg \,</math> ''Variable''
|}
where ''Variable'' is any variable.

==Examples and counterexamples==
:{|style="float:right; margin: 1em;"
|<pre>
         ∨
       /   \
      ∧     D
    /   \
   ∧     ¬
 /   \   |
A     ∨  C
     /  \
    ¬    C
    |
    B         
</pre>
|}
The following formulae are all in negation normal form:
:<math>\begin{align}
&((A \lor B) \land C) \\
&(A \lor \lnot B) \\
&(A \land \lnot B) \\
&\{[(A \land (\lnot B \lor C)) \land \lnot C] \lor D \}
\end{align}</math>
The first example is also in [[conjunctive normal form]], the next two are in both [[conjunctive normal form]] and [[disjunctive normal form]], but the last example is in neither.

The following formulae are not in negation normal form:
:<math>\begin{align}
         (A &\to B) \\
  \lnot (A &\lor B) \\
  \lnot (A &\land B) \\
  \lnot (A &\lor \lnot C)
\end{align}</math>

They are however respectively equivalent to the following formulae in negation normal form:
:<math>\begin{align}
  (\lnot A &\lor B) \\
  (\lnot A &\land \lnot B) \\
  (\lnot A &\lor \lnot B) \\
  (\lnot A &\land C)
\end{align}</math>

== Conversion to NNF == 

In [[predicate logic|classical logic]] and many [[modal logic]]s, every formula can be brought into this form by replacing [[Material conditional|implications]] (<math>\to</math>) and [[If and only if|equivalences]] (<math>\leftrightarrow</math>) by their definitions, using [[De Morgan's laws]] to push negation inwards, and eliminating double negations.  This process can be represented using the following [[Rewriting|rewrite rules]]:{{sfn|Robinson|Voronkov|2001|p=204}}

:<math>\begin{align}
    A \to B &~\rightsquigarrow~ \lnot A \lor B \\
    A \leftrightarrow B &~\rightsquigarrow~ (\lnot A \lor B) \land (A \lor \lnot B) \\
   \lnot (A \lor B) &~\rightsquigarrow~ \lnot A \land \lnot B \\
  \lnot (A \land B) &~\rightsquigarrow~ \lnot A \lor \lnot B \\
      \lnot \lnot A &~\rightsquigarrow~ A \\
  \lnot \exists x A &~\rightsquigarrow~ \forall x \lnot A \\
  \lnot \forall x A &~\rightsquigarrow~ \exists x \lnot A
\end{align}</math>

Transformation into negation normal form can increase the size of a formula only linearly: the number of occurrences of atomic formulas remains the same, the total number of occurrences of <math>\land</math> and <math>\lor</math> is unchanged, and the number of occurrences of <math>\lnot</math> in the normal form is bounded by the length of the original formula.

A formula in negation normal form can be put into the stronger [[conjunctive normal form]] or [[disjunctive normal form]] by applying [[Distributive property|distributivity]]. Repeated application of distributivity may exponentially increase the size of a formula. In the classical [[propositional logic]], transformation to negation normal form does not impact computational properties: the [[Boolean satisfiability problem|satisfiability problem]] continues to be [[NP-complete]], and the validity problem continues to be [[co-NP-complete]]. For formulas in conjunctive normal form, the validity problem is solvable in polynomial time, and for formulas in disjunctive normal form, the satisfiability problem is solvable in polynomial time.

==See also==
* [[Conjunctive normal form]]
* [[Disjunctive normal form]]

==Notes==
{{Reflist}}

==References==
* {{Cite book
|editor1-last=Robinson
|editor1-first=John Alan
|editor1-link=John Alan Robinson
|editor2-last=Voronkov
|editor2-first=Andrei
|editor2-link=Andrei Voronkov
|date=2001
|title=Handbook of Automated Reasoning
|title-link=Handbook of Automated Reasoning
|volume=1
|publisher=[[MIT Press]]
|pages=203 ff
|isbn=0444829490
}}

==External links==
* [https://archive.today/20121208184549/http://www.izyt.com/BooleanLogic/applet.php Java applet for converting logical formula to Negation Normal Form, showing laws used]

[[Category:Propositional calculus]]
[[Category:Normal forms (logic)]]
[[Category:Knowledge compilation]]
{{Normal forms in logic}}