Created on March 10, 2013, 4:19 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:36 p.m.
The Tableaux Algorithm for the Description Logics Attribute Language Complement (ALC) is based on the same principles as those for the Propositional Logic and First Order Logic.
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.
Further more one has to apply all the Transformation Rules/Equivalence Rules.
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.
In the end the original Knowledge Base and the Negated Normal Form of the Knowledge are logical Equivalent.
W
be a Knoweldge Base,C≡D
by C⊑D
ad D⊑C
C⊑D
by ¬C⊔D
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)
W
W
and NNF(W)
are logically equivalentNegation 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
-> The Statement GoodMagicion is a Subclass of Magician can be deduced from the original Knowledge Base.
Comment on This Data Unit