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

[Jun Fang]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.zih.tu-dresden.de/pipermail/dl/attachments/20110630/46fe4b77/attachment.htm>