Reasoning in very expressive Description Logics (DLs) such as SROIQ is often hard since non-determinism, e.g., from disjunctions or cardinality restrictions, requires a case-by-case analysis and since a strict separation between intensional (TBox) and extensional (ABox) knowledge is not possible due to nominals. Current state-of-the-art reasoners for SROIQ are typically based on (hyper-)tableau algorithms, where higher level reasoning tasks such as classification are reduced to possibly many consistency tests. For large ABoxes and more expressive DLs, reasoning then easily becomes infeasible since the ABox has to be considered in each test.
For less expressive DLs, optimisations have been proposed that allow for considering only parts of the ABox for checking whether an individual is an instance of a specific concept [22,23]. It is, however, not clear how these optimisations can be extended to SROIQ. Furthermore, approaches based on partitioning and modularisation require a syntactic pre-analysis of the concepts, roles, and individuals in a KB, which can be quite costly for more expressive DLs and, due to the static analysis, only queries with specific concepts are supported. Rewriting axioms such that ABox reasoning is improved also carries the risk that this negatively influences other reasoning tasks for which ABox reasoning is potentially not or less relevant.
Another possibility is the caching of the completion graph that is built by the tableau
algorithm during the initial consistency check. The re-use of (parts of) the cached
completion graph in subsequent tests reduces the number of consequences that have to be
re-derived for the individuals of the ABox. Existing approaches based on this idea (e.g.,
[
The paper is organised as follows: We next introduce some preliminaries and then
present the basic completion graph caching technique in Section 3. In Section 4, we
present several extensions and applications to support nominals in ordinary satisfiability
caching, to perform incremental reasoning for changing ABoxes, and to handle very
large ABoxes by storing data in a representative way. Finally, we present an evaluation
of the presented techniques in Section 5 and conclude in Section 6. Further details and
an extended evaluation are available in a technical report [
For brevity, we do not introduce DLs (see, e.g., [
Model construction calculi such as tableau [
Unrestricted application of rules for existential or at-least cardinality restrictions
can lead to the introduction of infinitely many new nodes. To guarantee termination,
a cycle detection technique called (pairwise) blocking [
In the following, we use superscripts to distinguish di erent versions of completion graphs. We denote with Gd = (Vd; Ed; Ld; ,˙d; Md) the last completion graph of the initial consistency test that is obtained with only deterministic rule applications and with Gn = (Vn; En; Ln; ,˙n; Mn) the fully expanded (and clash-free) completion graph that possibly also contains non-deterministic choices. Obviously, instead of starting with the initial completion graph G0 to which no rule has (yet) been applied, we can use Gd to initialise a completion graph G for subsequent consistency tests which are, for example, required to prove or refute assumptions of higher level reasoning tasks. To be more precise, we extend Gd to G by the new individuals or by additional assertions to original individuals as required for a subsequent test and then we can apply the tableau expansion rules to G. Note, in order to be able to distinguish the nodes/nominals in the di erent completion graphs, we assume that all nodes/nominals that are newly created for G do not occur in existing completion graphs, such as Gd or Gn.
This re-use of Gd is an obvious and straightforward optimisation and it is already
used by many state-of-the-art reasoning systems to successfully reduce the work that
has to be repeated in subsequent consistency tests [
To improve the handling of non-deterministic knowledge bases, our approach uses criteria to check whether nodes in G (or the nodes in a completion graph G0 obtained from G by further rule applications) are “cached”, i.e., there exist corresponding nodes in the cached completion graph of the initial consistency test and, therefore, it is not required to process them again. These caching criteria check whether the expansion of nodes is possible as in the cached completion graph Gn without influencing modified nodes in G0, thus, only the processing of new and modified nodes is required. Definition 1 (Caching Criteria). Let Gd = (Vd; Ed; Ld; ,˙d; Md) be a completion graph with only deterministically derived consequences and Gn = (Vn; En; Ln; ,˙ n; Mn) a fully expanded and clash-free expansion of Gd. Moreover, let G be an extension of Gd and G0 = (V0; E0; L0; ,˙0; M0) a completion graph that is obtained from G by applying tableau expansion rules.
A node v0 2 V0 is cached in G0 if caching of the node is not invalid, where the caching is invalid (we then also refer to the node as non-cached) if C1 v0 < Vd or mergedToMn (v0) < Vn;
n C2 L0(v0) * Ln(mergedToM (v0));
n C3 8r:C 2 Ln(mergedToM (v0)) and there is an r-neighbour node w0 of v0 such that w0 is not cached and C < L(w0); C4 6 m r:C 2 Ln(mergedToMn (v0)) and the number of the non-cached r-neighbour nodes of v0 without nnf(:C) in their labels together with the r-neighbours in Gn of n mergedToM (v0) with C in their labels is greater than m;
n C5 9r:C 2 Ln(mergedToM (v0)) and every r-neighbour node w0 of v0 with C < L(w0) n and C 2 Ln(mergedToM (w0)) is not cached;
n C6 > m r:C 2 Ln(mergedToM (v0)) and the number of r-neighbour nodes wn1; : : : ; wkn of mergedToMn (v0) with C 2 Ln(wn); : : : ; C 2 Ln(wkn), for which there is either no n 1 n node wi0 2 V0 with mergedToM (wi0) = win or wi0 with mergedToM (wi0) = win and C < L(wi0) is not cached for 1 i k, is less than m; C7 mergedToMn (v0) is a nominal node with 6 m r:C in its label and there exists a blockable and non-cached inv(r)-predecessor node w0 of v0 with nnf(:C) < L(w0); n n C8 mergedToM (w0) is an r-neighbour node of mergedToM (v0) such that w0 is not cached and w0 is not an r-neighbour node of v0;
n C9 mergedToM (v0) has a successor node un such that un or a descendant of un has n a successor node mergedToM (w0) for which w0 2 V0, w0 is not cached, and there exists no node u0 2 V0 with mergedToMn (u0) = un;
n n C10 mergedToM (v0) is blocked by mergedToM (w0) and w0 2 V0 is non-cached; n n C11 there is a non-cached node w0 2 V0 and mergedToM (v0) = mergedToM (w0); or n n C12 there is a node w0 2 V0 such that v0 ,˙0w0 and mergedToM (v0) = mergedToM (w0).
Conditions C1 and C2 ensure that a node also exists in the cached completion graph Gn and that its label is a subset of the corresponding label in Gn such that the same expansion is possible. C3 checks whether the expansion of a node would add a concept of the form 8r:C such that it could propagate C to a non-cached neighbour node. Analogously, C4 checks for potentially violated at-most cardinality restrictions by counting the new or modified neighbours in G0 and the neighbours in Gn. C5 and C6 verify that existential and at-least cardinality restrictions are still satisfied if the cached nodes are expanded identically. C7 checks whether the NN-rule of the tableau algorithm would be applicable after the expansion, i.e., we check whether all potentially relevant neighbours in G0 are nominal nodes. C8 checks whether the expansion would add additional roles to edge labels between cached and non-cached nodes, which could be problematic for disjoint roles. For C9: If a node w0, for which caching is invalid, is connected to nodes in Gn that are only available in Gn (e.g., non-deterministically created ones), then we have to identify caching as invalid for those ancestors of these nodes that are also in G0 such that these connections to w0 can be re-built. Otherwise, we would potentially miss new consequences that could be propagated from w0. C10 is used to reactivate the processing of nodes for which the caching of the blocker node is invalid. C11 and C12 ensure that merging is possible as in Gn: C11 checks whether the node into which the node is merged is also cached and C12 ensures that there is no additional entry for ,˙0 that would cause a clash if the nodes were merged as in Gn.
L(va) = n >; fag; 9r:fbg; B t A1; A1 o va r
vb L(v1) = n >; 9r:(fcg u A2) o
s r v1 r
vc L(vc) = ( >; fcg; 9s:fbg; )
fcg u A2;A2;A3
L(vb) = ( >; fbg; B9tr:99rr::9(frc:g(fucgAu2)A;82)s; B:At3 8s :A3; )
Since only those nodes can be cached, which are available in the “deterministic”
completion graph Gd, it is important to maximise the deterministic processing of the
completion graph. This can, for example, be achieved by processing the completion
graph with deterministic rules only until the generation of new nodes is subset blocked.
Subset blocking is not su cient for more expressive DLs, but it prevents the expansion
of too many successor nodes in case non-deterministic rule applications merge and
prune some parts of the completion graph. Absorption techniques (e.g., [
Most conditions can be checked locally: For a non-cached node, we simply follow its edges w.r.t. G0 and Gn to (potentially indirect) neighbour nodes that are also available in Gd. Exceptions are Conditions C10, C11, and C12, for which we can, however, simply trace back established blocking relations or Mn to find nodes for which the caching criteria have to be checked. The implementation can also be simplified by keeping the caching of a node invalid once it has been identified as invalid (even if the caching becomes possible again after the node has been expanded identically). Instead of directly checking the caching criteria, the relevant nodes can also be stored in a set/queue to check the conditions when it is (more) convenient. Clearly, it depends on the ontology, whether it is more beneficial to test the caching criteria earlier or later. If the criteria are tested early, then we could unnecessarily re-process some parts of the cached completion graph since the application of (non-deterministic) expansion rules can satisfy some conditions. A later testing could cause a repeated re-processing of the same parts if a lot of backtracking is required and consequences of re-activated nodes are involved in clashes. Alternatively, one could learn for the entire ontology or for single nodes, whether the criteria should be checked earlier or later. Unfortunately, this cannot easily be realised for all reasoning systems since it requires that dependencies between derived facts are precisely tracked in order to identify nodes that are often involved in the creation of clashes and for which the criteria should be checked early.
It is also possible to non-deterministically re-use derived consequences from Gn, n i.e., if the caching is invalid for a node v and mergedToM (v) is in Gn, then we can nonn deterministically add the missing concepts from Ln(mergedToM (v)) to L(v). Since the resulting completion graph is very similar to the cached one, caching can often be established quickly for many nodes. Of course, if some of the non-deterministically added concepts are involved in clashes, then we potentially have to backtrack and process the alternative where this node is ordinarily processed. Another nice side e ect of storing Gn is that we can use the non-deterministic decisions from Gn as an orientation in subsequent consistency tests. By prioritising the processing of the same non-deterministic alternatives as for Gn, we can potentially find a solution that is very similar to Gn without exploring much of the search space. 4
In this section, we sketch additional applications of the caching technique, which allow for supporting nominals for the satisfiability caching of node labels and for reducing the incremental reasoning e ort for changing ABoxes. Furthermore, we describe an extension that allows for caching (parts of) the completion graph in a representative way, whereby an explicit representation of many nodes in the completion graph can be avoided and, therefore, the memory consumption can be reduced.
Satisfiability Caching with Nominals: Caching the satisfiability status of labels of
(blockable) nodes in completion graphs is an important optimisation technique for
tableau-based reasoning systems [
However, in combination with completion graph caching, we re-gain the possibility to cache some labels of (blockable) nodes for knowledge bases with nominals. Roughly speaking, we first identify which nodes “depend on” which nominals, i.e., which nominal nodes are existentially quantified as a successor/descendant for a node. The labels of such nodes can then be cached together with the dependent nominals, i.e., with those nominals on which the nodes depend, if all nodes for the dependent nominals are still cached w.r.t. the initial completion graph. These cache entries can be re-used for nodes with identical labels in subsequent completion graphs as long as the completion graph caching of the nodes for the dependent nominals is not invalid. Of course, the blocked processing of nodes due to matching cache entries has to be reactivated if the completion graph caching of a node for a dependent nominal becomes invalid. Moreover, we cannot cache the labels of blockable nodes that depend on newly generated nominals since possible interactions over these nodes are not detected.
Incremental Reasoning for Changing ABoxes: Many reasoning systems re-start
reasoning from scratch if a few axioms in the knowledge base have been changed. However,
it is not very likely that a few changes in the ABox of a knowledge base have a huge
impact on reasoning. In particular, many ABox assertions only propagate consequences
to the local neighbourhood of the modified individuals and, therefore, the results of
reasoning tasks such as classification are often not a ected, even if nominals are used in
the knowledge base. With the presented completion graph caching, we can easily track
which nodes from the cached completion graph are modified in subsequent tests and
for which caching is invalidated to perform higher level reasoning tasks. Hence, if the
changed ABox assertions have only a known, locally limited influence, then the
reasoning e ort for many (higher level) reasoning tasks can be reduced by checking whether
a tracked node is a ected by the changes. To detect the influences of the changes, an
incremental consistency check can be performed where all modified individuals and
their neighbours are deterministically re-constructed step-by-step until “compatibility”
with the previous deterministic completion graph is achieved, i.e., the same
deterministic consequences are derived for the nodes as in the previous completion graph. The
non-deterministic version of the new completion graph can then be obtained by
continuing the (non-deterministic) processing of the re-constructed nodes and by using
the presented completion graph caching for all remaining nodes. Hence, we can
identify the influenced nodes by comparing the newly obtained completion graph with the
previous one. Compared to other incremental consistency checking approaches (e.g.,
[
The completion graph caching introduced in Section 3 is integrated in our reasoning system Konclude [20] and we selected several well-known benchmark ontologies (cf. Table 1) for the evaluation of the presented techniques. The evaluation was carried out on a Dell PowerEdge R420 server running with two Intel Xeon E5-2440 hexa core processors at 2.4 GHz with Hyper-Threading and 144 GB RAM under a 64bit Ubuntu 12.04.2 LTS. In order to make the evaluation independent of the number of CPU cores, we used only one worker thread for Konclude. We ignored the time spent for parsing ontologies and writing results and we used a time limit of 5 minutes, i.e., 300 seconds.
Table 2 shows the reasoning times for consistency checking (including preprocessing), classification, and realisation (in seconds) with di erent completion graph caching techniques integrated in Konclude. Please note that the class hierarchy is required to realise an ontology, i.e., classification is a prerequisite of realisation, and, analogously, consistency checking as well as preprocessing are prerequisites of classification. Thus, realisation cannot be performed if the time limit is already reached for classification.
If no completion graph caching is activated (No-C), then the realisation and classification can often require a large amount of time since Konclude has to re-process the entire ABox for all instance and subsumption tests (if the ontology uses nominals). For several ontologies, such as Wine and DOLCE, the caching and re-use of the deterministic completion graph from the consistency check (Det-C) already leads to significant improvements. Nevertheless, with the two variants ET-C and LT-C of the presented completion graph caching technique, where ET-C uses an “early testing” and LT-C a “late testing” of the defined caching criteria, Konclude can further reduce the reasoning times. In particular, with both completion graph caching techniques, all evaluated ontologies can easily be classified and also the realisation can be realised e ciently for all but UOBM-1. Table 2 also reveals that only for COMSO there is a remarkable di erence between ET-C and LT-C, where this di erence can be explained by the fact that there is often more interaction with the individuals from the ABox for instance tests than for satisfiability and subsumption tests and, therefore, ET-C can be better for realisation due to the potentially lower e ort in combination with backtracking.
The e ects of the di erent completion graph caching techniques can also be observed for the OWL DL Realisation dataset of the ORE 2014 competition,3 which contains several ontologies with non-deterministic language features and non-trivial ABoxes. By excluding 1; 331 s spent for preprocessing and consistency checking, the accumulated classification times over the contained 200 ontologies are 3; 996 s for the version No-C, 2; 503 s for Det-C, 1; 801 s for ET-C, and 1; 606 s for LT-C. Clearly, the dataset also contains many ontologies for which completion graph caching does not seem to have a significant impact, for example, if the ontologies can be processed deterministically or the ontologies are too di cult to even perform consistency checking (which is the case for 3 ontologies). Nevertheless, our completion graph caching improves the classification time with similar performances for LT-C and ET-C. By using 3 http://www.easychair.org/smart-program/VSL2014/ORE-index.html Ontology j j 100
jKj USDA-5 USDA-5 USDA-5 COSMO COSMO COSMO DPC1 DPC1 DPC1 UOBM-1 UOBM-1 UOBM-1 the satisfiability caching extension for nominals, as presented in Section 4, the accumulated classification time can be further improved to 725 s. Similar results are also achieved for the realisation of these ontologies. By excluding the times for all prerequisites, the accumulated realisation times over all 200 ontologies are 1; 740 s for No-C, 1; 498 s for Det-C, 1; 061 s for ET-C, 1; 256 s for LT-C, and 923 s for the version where the satisfiability caching extension for nominals is additionally activated. Incremental Reasoning Experiments: To test the incremental reasoning based on the presented completion graph caching, we used those ontologies of Table 1 that have a large amount of ABox assertions and for which Konclude still has a clearly measurable reasoning time, i.e., USDA-5, COSMO, DPC1, and UOBM-1. We simulated a changed ABox for these ontologies by randomly removing a certain amount of assertions from the ontology (denoted by K ) and by re-adding the removed assertions and removing new assertions (denoted by K ). For each ontology, we evaluated 10 random modifications that have 1, 2, and 4 % of the size of the ontology’s ABox. For simplicity, all modifications have the same amount of removed and added assertions. The obtained results for the presented incremental reasoning approach are shown in Table 3.
For consistency, the first two columns show the (incremental) consistency checking time (in seconds) for K and K , respectively, and the third column shows the percentage of the nodes in the completion graph for K that has been changed for the application of the modification. It can be observed that, especially for smaller modifications, the incremental consistency check often requires much less time than the initial consistency check. In particular, the individuals of USDA-5 are sparsely connected via object properties and, therefore, often only the modified individuals have to be re-built. For larger modifications, the incremental consistency checking time increases significantly for some ontologies, e.g., UOBM-1, and does almost catch up to the consistency checking time for the initial ontology. On the one hand, our incremental consistency checking approach clearly has some additional overhead due to the fact that nodes are re-built step by step until an expansion as for the initial completion graph can be guaranteed, but, on the other hand, our prototypical implementation has still a lot of room for improvements. For example, we currently also re-build nodes for individuals for which only new assertions have been added although it would be su cient to simply extend the nodes of the previous deterministic completion graph by the new consequences.
For classification, the first two columns show analogously the (incremental) classification time for K and K , respectively, and the third column represents the percentage of the classes for which satisfiability and subsumption tests were re-calculated. At the moment, the used/modified nodes from the cached completion graph are tracked together for all satisfiability and subsumption tests and we mark those classes for which nodes have been tracked. It can be observed that for the ontologies with nominals (e.g., UOBM-1), only a few classes have to be re-classified and, in several cases, reclassification is not required at all.
Also for realisation, the first two columns show the (incremental) realisation time for K and K , respectively, and the last column shows the percentage of the number of individuals that are potentially a ected by the changes and for which the (possible) types have to be re-computed. For this, we separately track, for each individual, the nodes of the cached completion graph that are used/modified by the instance tests. Representative Caching Experiments: We integrated a first prototypical version of the presented representative caching in our reasoning system Konclude, which is, however, not yet compatible with all other integrated features and optimisations. As of now, the integrated representative caching is primarily used for “simple individuals” that do not have too much interaction with other individuals in the ABox. In cases where representative caching could easily cause performance deficits (e.g., through the intensive use of nominals), Konclude caches the relevant parts of such completion graphs by using the ordinary technique. Moreover, data property assertions are, at the moment, internally transformed into class assertions and, as a consequence, nodes for individuals with data property assertions can currently not be representatively cached. However, first experiments are very encouraging. For example, Homo_sapiens is a very large SROIQ ontology from the Oxford ontology library with 244; 232 classes, 255 object properties, and 289; 236 individuals for which Konclude requires 10; 211 MB in total to check the consistency by using representative caching, whereas 19; 721 MB are required by Konclude for consistency checking with a fully expanded completion graph. Note that a large amount (9; 875 MB) of the required memory is used for the (unoptimised) internal representation, the data from the preprocessing, and the parsed OWL objects which are kept in memory to facilitate the handling of added/removed axioms. 6
We have presented a refinement of the completion graph caching technique that improves ABox reasoning also for very expressive Description Logics through a more sophisticated handling of non-deterministic consequences. In addition, we sketched extensions and applications of the caching technique, which allow for supporting nominals for the satisfiability caching of node labels, for reducing the incremental reasoning e ort for changing ABoxes, and for handling very large ABoxes by storing partially processed parts of the completion graph in a representative way. 20. Steigmiller, A., Liebig, T., Glimm, B.: Konclude: system description. J. of Web Semantics 27(1) (2014) 21. Tsarkov, D., Horrocks, I.: E cient reasoning with range and domain constraints. In: Proc.
17th Int. Workshop on Description Logics (DL’04). vol. 104. CEUR (2004) 22. Wandelt, S., Möller, R.: Towards ABox modularization of semi-expressive description logics. Applied Ontology 7(2), 133–167 (2012) 23. Wu, J., Hudek, A.K., Toman, D., Weddell, G.E.: Absorption for ABoxes. J. of Automated Reasoning 53(3), 215–243 (2014)