Hi All,<div><br></div><div>I have a question about the expansion rule of Tableaux algorithm.</div><div><br></div><div>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.</div>

<div><br></div><div>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?</div><div><br></div><div>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?</div>
<div><br></div><div>If the {C} is right, should inclusion expansion rule be applied to every node?</div><div>if the {C, \exists r.C} is right, then the tree is infinite if there are \exist concept  (need blocking checking frequently?).</div>
<div><br></div><div>Thanks in advance.</div><div><br></div><div><br></div><div><br></div><div><br></div><div>-- <br><div>Best Regards!</div>
<div> </div>
<div>Jun Fang</div><br>
</div>