## Change - Negation Normal Form

Created on March 5, 2013, 9:41 p.m. by Hevok & updated on March 5, 2013, 10:54 p.m. by Hevok

A Negation can be shifted inside the logical Formulas via Equivalences. ¶

In the end one wants to come up with a Conjunctive Normal Form which does not contain Equivalences or Implications, therefore one can remove them via the Equivalences. For example Equivalences can be transformed into two Implications and the Implications can be transformed into a Disjunction. Then one removes simple or multiple Negations. Finally all Negations are placed directly in front of an Atom. ¶

All Negations are moved inwards via the following logical Equivalences ¶

F ↔ G ≡ (F → G) ∧ (G → F) ¶
F → G ≡ ¬F ∨ G ¶
¬(F ∧ G) ≡ ¬(F ∧ G) ¶
¬(F ∨ G) ≡ ¬F ∧ ¬G ¶

¬(∀X) F ≡ (∃X) ¬F ¶
¬(∃X) F ≡ (∀X) ¬F ¶

¬¬F ≡ F ¶

Result: ¶
- implications and equivalences are removed ¶
- multiple Negations are removed ¶
- all Negations are placed directly in front of atoms ¶

* Example ¶

((∀X)( penguin(X) → blackwhite(X) ) ¶
∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) ) ¶
) → (∃X)( penguin(X) ∧ oldTVshow(X) ) ¶

is transformed into ¶

¬( (∀X)( ¬penguin(X) ∨ blackandwhite(X) ) ¶
∧ (∃X)( oldTVshow(X) ∧ blackandwhite(X) ) ¶
) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) ) ¶

is transformed into ¶

( (∃X)( penguin(X) ∧ ¬blackandwhite(X) ) ¶
∨ (∀X)(¬oldTVshow(X) ∨ ¬blackwhite(X) ) ¶
) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) ) ¶

Comment: Corrected code blocks