[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
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: <https://mailman.informatik.uni-bremen.de/pipermail/dl/attachments/20110630/46fe4b77/attachment.html>
More information about the dl
mailing list