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

[Uli Sattler]

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?).
>
> Thanks in advance.
>
>
>
>
> -- 
> 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/ 
> .  **