Blocking

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

If Iteration steps in the Tableaux Algorithms do not terminate one cannot deduce further information from it. Thus there is also ways the same Construct or Formula applied over and over again, e.g. to deduce there must be further Person who exists, i.e. a new Individual or which the same Class membership holds. The idea is instead of repeating this all over again to reuse this with a Method that is called Blocking. This makes a shortcut, but the Correctness of this methods must be proven.

• Idea: reuse old Nodes
• Correctness of this short cut must be proven!

If the Class extension of x1 is already contained the Class Extension of a previous already existing Individual then one might stop, because one can say we will end. Thus, the Algorithm stops here. However the Path is then not closed, only the Algorithm terminates.

σ(Hevok) = {Person,
          ¬Person ⊔ ∃hasParent.Person,
          ∃hasParent.Person}
σ(x1) = {Person,
          ¬Person ⊔ ∃hasParent.Person,
          ∃hasParent.Person}

σ(Hevok) ⊆ σ(x1), so Hevok blocks x1

Sigma (σ) denotes the Negation Normal Form (NNF) and refers to "Class Extension" - All Classes that got generated for that Individual.

Tags: termination, coding, block, algorithm, stop
Categories: Concept
Parent: Tableaux Algorithm
Children: Tableaux Algorithm (DL) with Blocking

Update entry (Admin) | See changes

---

Back to top

---