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

Jun Fang jun.fang.nwpu at gmail.com
Thu Jun 30 16:10:07 CEST 2011

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
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: <https://mailman.informatik.uni-bremen.de/pipermail/dl/attachments/20110630/46fe4b77/attachment.html>

More information about the dl mailing list