First of all we have to transform a given Knowledge Base in the Negation Normal form. This is necessary because we try to put the Negation in front of the Atomic Classes, i.e. so far as possible into the Braces of a Formula.
Given a Knowledge Base W, one has to substitute the Class Equivalences and also the Class Inclusions by its Logical Equivalences that are only based on Conjunctions and Disjunctions. The Class Equivalences are first substituted by two Class Inclusions and the Class Inclusions are substitutes by its Logical Equivalent Disjunction.
For instance if C is atomic its negated Normal Form is C. Also the negated normal form of not C will be not C, if C is atomic. Otherwise if we have a double Negation the negation Normal Form corresponds to the Negation Norma Form of the original Class. Then one has Disjunction and Conjunction as well as the application of the De Morgan Rule. For the Universal and Existential Quantification one can put the Negation Normal Form inside the Formula that is bound by the Quantifier. One only need to take care when the Quantifier is negated then it switches from the negated universal Quantification to the existential Quantification if the negation is put inside the Formula. The negated Existential Quantification is switched to the Universal Quantification.
Wbe a Knoweldge Base,
Apply the NNF Transformations
NNF(C) = C, if C s atomic NNF(¬C) = ¬C, if C is atomic NNF(¬¬C) = NNF(C) NNF(C⊔D) = NNF(C) ⊔ NNF(D) NNF(C⊓D) = NNF(C) ⊓ NNF(D) NNF(¬C⊔D) = NNF(¬C) ⊔ NNF(¬D) NNF(¬(C⊓D)) = NNF(¬C) ⊓ NNF(¬D) NNF(∀R.C) = ∀R.NNF(C) NNF(∃R.C) = ∃R.NNF(C) NNF(¬∀R.C) = ∀R.NNF(¬C) NNF(¬∃R.C) = ∃R.NNF(¬C)
Resulting Knowledge Base
NNF(W)are logically equivalent
Negation is placed directly in front of Atomic Classes.
Example: GoodMagician ⊑ (Magician ⊓ ¬DeathEater) ⊔ (Magician ⊓ HarryPotterFriend) GoodMagician ⊑ Magician
(1) (GoodMagician ⊔ ¬Magician) (from the Knowledge Base - the negated Consequence) (2|α from 1) **GoodMagician(a)** (3|α from 1) **¬Magician(a)** (4) ¬GoodMagician ⊔ (Magician ⊓ ¬DeathEater) ⊔ (Magician ⊓ HarryPotterFriend)(a) (from Knowledge Base) (5|β from 4) **¬GoodMagician(a)** (6|β from 4) (Magician ⊓ ¬DeathEater) ⊔ (Magician ⊓ HarryPotterFriend)(a) |(7|β from 6) (Magician ⊓ ¬DeathEater)(a) (8|β from 6) (Magician ⊓ HarryPotterFriend)(a) (9|α from 7) **Magician(a)** (10|α from 7) ¬DeathEater(a) (11|α from 8) **Magician(a)** | (12|α from 8) HarryPotterFriend(a)
All brachnes of the Tableaux caontain a Contradiction. The Tableaux Algroithm using the negated Consequences is closed