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.

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.

## Comment on This Data Unit