Handling knowledge bases that are formulated with expressive Description Logics (DLs), such as SROIQ [8], and that contain large amounts of facts is still challenging for state-of-the-art reasoning systems despite the huge range of developed optimisation techniques. For example, there are several summarisation [2,5] as well as abstraction techniques [6] and some problems are well-suited for a reduction to datalog [1,4,15]. However, these techniques do not necessarily work well for all ontologies, may be limited to certain queries or (fragments of) DLs, or require expensive computations (e.g., justi cations). Particularly challenging is the support of conjunctive queries with complex concept terms and/or with existential variables that may bind to anonymous individuals since these features typically make it di cult to appropriately split the ABox upfront [13,14]. Although many tableau-based reasoning systems for expressive DLs directly integrate techniques that improve ABox reasoning, e.g., bulk processing with binary retrieval [7], caching and reusing the partial model (aka completion graph) from the initial consistency check [9,11], these techniques typically require signi cant amounts of main memory, which may be more than what is typically available. We propose to dynamically split the model construction process with tableau algorithms. This allows for (i) handling larger ABoxes since not everything has to be processed at once and for (ii) exploiting parallelisation. In particular, we can ensure similarly sized work packages that can be processed concurrently without direct synchronisation. To ensure that the partial models constructed in parallel are \compatible" with each other, we employ a cache where selected consequences for individuals are stored and utilise appropriate reuse and expansion strategies in the model construction process for the cached consequences. Conjunctive query answering is supported by adapting the expansion criteria and by appropriately splitting the propagation work through the (partial) models. For consistency checking, the work- ow with this individual derivations cache is roughly as follows: A thread gets a new part of the ABox assigned and retrieves stored derivations from the cache for the individuals in that part. The thread then tries to construct a fully expanded and clash-free local completion graph for the ABox part by reusing cached derivations and/or by expanding the
processing to individuals until they are \compatible" with the cache.
Compatibility requires that the local completion graph is fully expanded and clash-free
and that it can be expanded such that it matches the derivations for the
remaining individuals in the cache. If it is required to extend the processing to some
\neighbouring" individuals for achieving compatibility (e.g., if di erent
nondeterministic decisions are required for the already processed individuals), then
also the cached derivations for these individuals are retrieved and considered. If
this process succeeds, the cache is updated with the new or changed derivations
for the processed individuals. If compatibility cannot be obtained (e.g., due to
expansion limitations that ensure similarly sized work packages), then the
corresponding cache entries are marked such that these parts are considered later
separately, i.e., a thread loads the data for (some) marked individuals and tries
to construct a fully expanded and clash-free completion graph for the
problematic part until full compatibility is obtained. If clashes occur that depend on
reused (non-deterministic) derivations from the cache, then the corresponding
individuals can be identi ed such that their expansion can be prioritized and/or
the reuse of their derivations can be avoided. As a result, (in)consistency of
the knowledge base can eventually be detected, as soon as all problematic
individuals are directly expanded and all relevant non-deterministic decisions are
investigated together. More details can be found in the accompanying technical
report [
We implemented the proposed individual derivations cache with a few
extensions and adaptations in the tableau-based reasoning system Konclude [12]. For
evaluating the approach, we used the large ontologies and complex queries from
the PAGOdA and VLog evaluations [
Semantics 27(1) (2014) 13. Wandelt, S., Moller, R.: Distributed island-based query answering for expressive ontologies. In: Proc. 5th Int. Conf. on Advances in Grid and Pervasive Computing (GPC'10). pp. 461{470. Springer (2010) 14. Wandelt, S., Moller, R.: Towards ABox modularization of semi-expressive description logics. J. of Applied Ontology 7(2), 133{167 (2012) 15. Zhou, Y., Cuenca Grau, B., Nenov, Y., Kaminski, M., Horrocks, I.: PAGOdA: Pay-as-you-go ontology query answering using a datalog reasoner. J. of Arti cial Intelligence Research 54, 309{367 (2015)