Tableaux Extension Rules for DL

Created on March 10, 2013, 4:28 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:36 p.m.

When one has a Negated Normal Form one can apply the Tableaux Extension Rules for Description Logics. They are split into an upper part that is applied directly to the Knowledge Base and a lower part for Formulas that are already in the Decision Tree.

If one has already in the Knowledge Base in the ABox a Class Instantiation with the Individual a and the Class C one can add this to the Decision Tree. Likewise one can do that with the Instantiation of a Role. If one has a Role that connects Individual a and Individual b and it is already in the ABox one can put this down in the Decision Tree. Furthermore, if one has a Class in the Knowledge Base C and an already known Individual a, one can Instantiate this Class with Individual a and put this into the Decision Tree.

For the Formulas in the Decision Tree one has Conjunctions and Disjunctions which comply to the alpha and beta Rules. This means if one has already a Conjunction in the Decision Tree that is instantiated on an Individual a, one can put C of a and D of a, so the Instantiation of both of these Classes into the same Path of the Decision Tree. Otherwise if one has a Disjunction one has to split the Path and the left site one puts C of a and on the right Site D of a.

The Quantifier Rules are different to those from the First Order Logic, simply because the functionality of the Quantifiers is a little bit different. In Description the Existential Quantifier is applied to a Role and the Range of a Role, its property is restricted to Class C. Therefore if one has in the Decision tree and Existential Quantifier on Role R restricted to Class C instantiated on an Individual a, one might add the Relation R with the Individual a and b into the Decision Tree and one might also infer that there must be the Individual b which is new and this Individual must be of Class C, because of the Class Restriction. So C of b for a new Individual b will eb together with R of a,b added to the already existing Decision Tree. For the Universal Quantification it is quite similar, but only there a and b must already exists instantiated with the Role R inside the Decision Tree. Then one might also add that b must belong to Class C to the Decision Tree.

Then if the resulting Tableaux is closed the original Knowledge Base is unsatisfiable. So it is the same like for propositional Logic and First Order Logic.

Selection Action
C(a)∈W(ABox) Add C(a)
R(a,b)∈W(ABox) Add R(a,b)
C∈W(TBox) Add C(a) for a known Individual a
(C⊓D)(a)∈A Add C(a) and D(a)
(C⊔D)(a)∈A Split the path. Add (1) C(a) and (2) D(a)
(∃R.C)(a)∈A Add R(a,b) and C(b) for a new Individual b
(∀R.C)(a)∈A if R(a,b)∈A, then add C(b)
  • If the resulting Tableaux is closed, the original Knowledge Base is unsatisfiable.
  • Only select Elements that lead to new Elements within the Tableaux. If this is not possible, then the Algorithm terminates and the original Knowledge Base is satisfiable.

Tags: extension, logic, satisfiability
Categories: Concept, reST
Parent: Tableaux Algorithm

Update entry (Admin) | See changes

Comment on This Data Unit