Change - Blocking

Created on March 10, 2013, 4:32 p.m. by Hevok & updated on March 11, 2013, 5:21 p.m. by Hevok

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.