# [DL] A question about the expansion rule of Tableaux algorithm

Uli Sattler sattler at cs.man.ac.uk
Fri Jul 1 16:32:45 CEST 2011

```Hi Jun, yes you are (mostly) correct, especially when it comes to
observing that you need blocking to prevent (!) non-termination, i.e.,
to make sure that you end after a finite number of steps, with a
finite structure. I guess you could look at

F. Baader and U. Sattler. An Overview of Tableau Algorithms for
Description Logics. Studia Logica, 69:5-40, 2001.

for a high-level discussion of this and similar cases, and also for
references to the literature.

Cheers, Uli

On 30 Jun 2011, at 15:10, Jun Fang wrote:

> Hi All,
>
> I have a question about the expansion rule of Tableaux algorithm.
>
> Given a knowledge base K := <T, A>. In order to check consistency of
> the knowledge base, for every individual in the Abox, we try to use
> expansion rules to construct a model of tree from concepts related
> to the individual in the Abox and the whole concepts transformed
> from the TBox.
>
> When a new node is created (such as from the \exists r.C), should we
> need to copy the whole concepts of the TBox into it?
>
> For instance, let T={D \subclass \exists r.C} A={D(a)}, then the
> concept set of individual a is {\neg D \union \exists r.C, D}--
> {exists r.C, D}, then a new node b1 is created by using expansion
> rule of \exists r.C, the concept set of b1 is {C}, or {C, \neg D
> \union \exists r.C} by adding concepts from the Tbox?
>
> If the {C} is right, should inclusion expansion rule be applied to
> every node?
> if the {C, \exists r.C} is right, then the tree is infinite if there
> are \exist concept  (need blocking checking frequently?).
>
>
>
>
>
> --
> Best Regards!
>
> Jun Fang
>
> ---
> **  You received this mail via the description logic mailing list;
> for more  **
> **  information, visit the description logic homepage at http://dl.kr.org/
> .  **

```