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:
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 on This Data Unit