One of the techniques for tackling the ABox reasoning is the precompletion algo-
rithm, this technique is to split the KB satisability algorithm in two parts. In
the rst part all the information implicit in the role assertions is made explicit,
generating what we call a \precompletion" of the knowledge base, then a termi-
nological reasoner is used for verifying the consistency of the concept assertions
for each individual name [5, 6].
The work presented in  extended the precompletion algorithm for Knowl-
edge Base satiability to the DL language SHF. The main advantages of this
approach are its ability of using existing highly optimised TBox reasoners, and
the fact that it may be able to handle very large ABox by partitioning them
into disconnected parts.
However, the logic concerned in  is a subset of that required by Semantic
Web knowledge representation languages such as OWL, and it is not easy to
see how the technique can be extended to deal with more expressive languages.
Besides, as we stated in the motivation, we will be facing a huge amount of
service advertisements which might be more challenging for the traditional ABox
reasoning. Therefore, we chose an alternative approach | the instance store.
2.3 Instance Store
A instance store provides weaker functinality than a full ABox, but which is
probably sucient to support a number of app