## Tableaux Algorithm for ALC

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.

• Proof Algorithm to check the Consistency of a logical Formula by inferring that its Negation is a Contradiction (Proof by Refutation).
• Construct Tree, where each Node is marked with a logical Formula. A Path from the Root to a Leaf is the Conjunction of all Formulas represented with the Nodes of the Path; a Branch of the Path represents a Disjunction.
• The Tree is created by successive Application of the Tableaux Extension Rules.

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.

• Transformation to Negation Normal Form necessary
• Let `W` be a Knoweldge Base,
• Substitute `C≡D` by `C⊑D` ad `D⊑C`
• Substitute `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)`

• Negation Normal Form of `W`
• `W` and `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

-> The Statement GoodMagicion is a Subclass of Magician can be deduced from the original Knowledge Base. Tags: transformation, logic, algorithm, decision tree
Categories: Concept
Parent: Tableaux Algorithm
Children: Normalform

Update entry (Admin) | See changes