The success of modern multi-core processors makes it possible to develop parallel ABox reasoning algorithms to facilitate efficient reasoning on large scale ontological data sets. In this paper, we extend a parallel TBox reasoning algorithm for E LHR+ to a parallel ABox reasoning algorithm for E LH?,R+, which also supports the bottom concept so as to model disjointness and inconsistency. In design of algorithms, we exploit the characteristic of ABox reasoning in E LH?,R+ to improve parallelisation and reduce unnecessary resource cost. Particularly, we separate the TBox reasoning, ABox reasoning on types and ABox reasoning on relations. Our evaluation shows that a naive implementation of our approach can compute all ABox entailments of a Not-Galen ontology with about 1 million individuals and 9 million axioms in about 3 minutes.
⋆ This paper is an extended version of “Parallel ABox Reasoning of E L Ontologies” [
In this paper, we extend the parallel TBox reasoning algorithm [
The remainder of the paper is organised as follows: In Sect. 2 we introduce
background knowledge of DLs E LHR+ and E LH⊥;R+, and the parallel E LHR+ TBox
classification algorithm [
The proof of all lemmas and theorems are included in our online tech report at http://www.box.com/s/3636a703614b65f6cdba. 2 2.1
DL E LHR+ and E LH?;R+ A signature of an ontology O is a triple O = (CN O; RN O; IN O) consisting of three mutually disjoint finite sets of atomic concepts CN O, atomic roles RN O and individuals IN O. Given a signature, complex concepts in E LH⊥;R+ can be defined inductively using the E LH⊥;R+ constructors as in Table 1. E LHR+ supports all E LH⊥;R+ constructors except ⊥. Two concepts C and D are equivalent if they mutually include each other, denoted by C ≡ D. An ontology O = (T ; A) consists of a TBox T and an ABox A, which are finite sets of TBox axioms and ABox axioms, respectively. E LH⊥;R+ allows all axioms listed in Table 1. E LHR+ allows all except individual inequalities. The semantics of constructors and axioms are also listed in Table 1. Given an ontology O, we use ⊑O
∗ to represent the reflexive transitive closure of RIs. It is easy to see that in an E LHR+/ E LH⊥;R+ ontology O, all of such ⊑O ∗ relations can be computed in polynomial time w.r.t. the size of O. In ABox reasoning, we are particularly interested in ABox materialisation, i.e. finding all A(a) s.t. a ∈ IN O, A ∈ CN O, O |= A(a) and all r(a; b) s.t. a; b ∈ IN O, r ∈ RN O and O |= r(a; b). Such results can be very useful for efficient on-line instance retrieval and/or query answering. 2.2
Given an ontology O, TBox classification is a reasoning task that computes all
inclusions over atomic concepts in O. Kazakov et. al [
A atomic concept top bottom conjunction existential restriction ⊤ ⊥ C ⊓ D ∃r.C
atomic role r
general concept inclusion (GCI): C ⊑ D role inclusion (RI): r ⊑ s role transitivity: T rans(t)
class assertion: A(a) irnodleivaisdsuearltieoqnu:ality: ra(a=., bb) individual inequality: a̸ =_b AI ∆I rI CI ⊆ DI rI ⊑ sI tI × tI ⊆ tI
aI ∈ AI ⟨aI , bI ⟩ ∈ rI aI = bI aI ̸= bI
∅
CI ∩ DI {x|∃y.⟨x, y⟩ ∈ rI and y ∈ CI } : r ⊑O
∗ t ⊑∗O s; T rans(t) ∈ O
In the above rules, D → E denotes the special form of GCIs where D and E are both existential restrictions. Given an E LHR+ ontology O that has no ABox, these rules infer C ⊑ D iff O |= C ⊑ D for all C and D such that C ⊑ C ∈ S and D occurs in O [4, Theorem 1], where S is the set of axioms closed under the above rules. The completion rules are designed in a way that all premises of each rule have a common concept (the concept C in each rule), which is called a context of the corresponding premise axiom(s). Each context maintains a queue of axioms called scheduled, on which some completion rule can be applied, and a set of axioms called processed, on which some completion rule has already been applied. An axiom can only be included in the scheduled queues and/or processed sets of its own contexts. To ensure that multiple R⊑ CC ⊑⊑ DE : D ⊑ E ∈ O R+ C ⊑ C : ⊤ occurs in O
⊤ C ⊑ ⊤ R+ C ⊑ D1; C ⊑ D2 : D1 ⊓ D2 occurs in O
⊓ C ⊑ D1 ⊓ D2 R+ C ⊑ D : ∃s:D occurs in O
∃ ∃s:C → ∃s:D RH D ⊑ ∃rD:C;⊑∃Es:C → E : r ⊑∗O s
D ⊑ ∃r:C; ∃s:C → E RT
∃t:D → E TBox classification for E LHR+. They devise a set of completion rules as follows. R− C ⊑ D1 ⊓ D2
⊓ C ⊑ D1; C ⊑ D2 R− C ⊑ ∃R:D ∃ D ⊑ D workers can share the queues and sets without locking them, they further devised a concurrency mechanism, in which: (i) each worker will process a single context at a time and vice versa; (ii) the processing of all axioms in the scheduled queue of a context requires no axioms from the processed sets of other contexts. To realise all these, all contexts with non-empty schedules are arranged in a queue called activeContexts. A context can be added into the activeContexts queue only if it is not already in the queue.
Here are the key steps of the parallel TBox algorithm: 1. Tautology axiom A ⊑ A for each A ∈ CN O is added to the scheduled queue of A.
All active contexts are added into the queue of activeContexts. 2. Every idle worker always looks for the next context in the activeContexts queue and processes axioms in its scheduled queue. (a) Pop an axiom from the scheduled queue, add it into the processed set of the context. (b) Apply completion rules to derive conclusions. (c) Add each derived conclusion into the scheduled queue of its corresponding context(s), which will be activated if possible.
Before we extend the parallel TBox reasoning algorithm to support ABox reasoning in Sect. 4, we first discuss the challenges to deal with in parallel ABox reasoning. 3
A naive approach to ABox materialisation is to internalise the entire ABox into TBox (i.e., converting assertions of form C(a) into {a} ⊑ C, and R(a; b) into {a} ⊑ ∃R:{b}) and treat the internalised “nominals” as atomic concepts with TBox classification rules. This is inefficient due to unnecessary computation and maintenance costs. For example, axiom {a} ⊑ ∃r:C has C as a context. Thus once derived, it will be maintained in the processed set of C, as a possible left premise of Rule RH and/or RT . However, E LH⊥;R+ does not support nominals, meaning that any corresponding right premise ∃s:C → E can always be computed independently from (or before) the derivation of {a} ⊑ ∃r:C. Therefore it is unnecessary to maintain {a} ⊑ ∃r:C in context C because with all possible right premises pre-computed, it can be directly used to trigger all rules.
Even with TBox and ABox reasoning separated, performance and scalability can still be improved: (1) The computation of relations in E LH⊥;R+ is independent from the computation of types (Lemma 2). Thus when crafting type reasoning rules, relations can be used as side conditions instead of premises. (2) Among all the relations that can be entailed by an E LH⊥;R+ ontology, some can be trivially computed and do not contribute to type computation. These relations can be easily recovered in retrieval (Lemma 3). (3) Without individual equality, the computation of relations in E LH⊥;R+ can be perfectly parallelised on an individual basis. This indicates that when computing relations, the concurrency mechanism can be simplified. As we will show, we no longer need to maintain the scheduled queue and this improves scalability and performance.
The above optimisations are related to the design of completion rules. For further
optimisation on the execution of algorithms, we refer readers to our original paper [
We first extend the E LHR+ TBox completion rules to support the bottom concept: R⊥
D ⊑ ∃r:C; C ⊑ ⊥
D ⊑ ⊥ In what follows, we call the set containing the above rule and the E LHR+ rules in Sect. 2.2 the R rule set, which is sound and complete for E LH⊥;R+ classification: Lemma 1. For an E LHR+ TBox O, let S be any set of TBox axioms closed under the R rule set, using O axioms as side conditions, and ⊥ ⊑ ⊥ ∈ S if ⊥ occurs in O. Then for any C and D such that C ⊑ C ∈ S, D occurs in O, we have O |= C ⊑ D iff C ⊑ D ∈ S or C ⊑ ⊥ ∈ S.
The ← direction is trivial. The → direction can be proved with contrapositive. Assuming there are X ⊑ X ∈ S and Y occurs in O s.t. X ⊑ Y ∈= S and X ⊑ ⊥ ∈= S, we construct a model of O based on S and shows that this model does not satisfy X ⊑ Y .
With the R rules we can perform TBox reasoning: Definition 1. (TBox Completion Closure) Let O = (T ; A) be an E LH⊥;R+ ontology, its TBox completion closure, denoted by ST , is the smallest set of axioms closed under rule set R, using O axioms as side conditions, such that: for all A ∈ CN O, A ⊑ A ∈ ST ; ⊥ ⊑ ⊥ ∈ ST if ⊥ occurs in O.
According to Lemma 1, we have A ⊑ C ∈ ST or A ⊑ ⊥ ∈ ST for any A and C where A is an atomic concept and C occurs in T . This realises TBox classification. 4.2
As we pointed out in Sect. 3, relations can be computed independently from types. This is characterised by the following lemma.
Lemma 2. Let O = (T ; A) be an E LH⊥;R+ ontology and At ⊆ A be the set of all class assertions. Then O is inconsistent, or for all r ∈ RN O, a; b ∈ IN R, we have O |= r(a; b) iff O \ At |= r(a; b).
Now we present the ABox completion rules for E LH⊥;R+. Although E LH⊥;R+ does not support nominals ({a}), we still denote individuals with nominals since this helps simplify the presentation: (i) ABox rules are more readable, as they have similar syntactic forms to the TBox ones, and (ii) some of the ABox rules can be unified. More precisely, we establish the following mappings as syntactic sugar:
C(a) ⇔ {a} ⊑ C; a =: b ⇔ {a} ≡ {b}; a̸=_ b ⇔ {a} ⊓ {b} ⊑ ⊥; r(a; b) ⇔ {a} ⊑ ∃r:{b};
Obviously, these mappings are semantically equivalent. In the rest of the paper, without further explanation, we treat the LHS and RHS of each of the above mappings as a syntactic variation of each other.
We first present the relation completion rules as follows:
ARR {b} ⊑ ∃r:{a} : {a} ⊑ {c}; {d} ⊑ {b} ∈ A
H d
{ } ⊑ ∃r:{c} ARR {b} ⊑ ∃r:{a} : {c} ⊑ ∃t:{b} ∈ A; r; t ⊑∗O s; T rans(s) ∈ O
T {c} ⊑ ∃s:{a} It is worth noting that (1) without individual equality, the ARR rule is not needed, H rendering the ARTR rule perfectly parallelisable. This is an important property because in E LH⊥;R+ ontologies, individual equality can be easily eliminated by pre-computing equal individuals and using one of them as a representative; (2) relation computation is also independent from TBox completion. We call the reasoning results with the above rules the relation completion closure: Definition 2. (Relation Completion Closure) Let O = (T ; A) be an E LH⊥;R+ ontology, its relation completion closure, denoted by SR, is the smallest set of axioms closed under the rules ARRH and ARTR , using O axioms as side conditions, such that ST ⊆ SR and A \ At ⊆ SR (axioms mapped as elaborated before), where At ⊆ A is the set of all class assertions.
The soundness and tractability of relation completion closure is quite obvious. Its completeness can be characterised by the following lemma.
Lemma 3. For any E LH⊥;R+ ontology O, let SR be its relation completion closure, then O is inconsistent, or O |= r(a; b) only if {a} ⊑ ∃s:{b}; s ⊑∗O r ∈ SR for r ∈ RN O. 4.3
Now we present the other ABox completion rules as follows, which should be applied after a complete closure SR is constructed. In contrast to the R rules, the following rules contain concepts D(i) and E that can take multiple forms including nominals. Thus the mapping between ABox and TBox axioms allows us to describe the rules in a more compact manner. Together with the above two relation completion rules, we call all the ABox completion rules the AR rules.
The AR rules deserve some explanations: There are clear correspondences between the R rules and AR rules. For example, AR⊑ is an ABox counterpart of R⊑ except that the context is explicitly a nominal, and TBox results are used as side conditions. Note that directly applying the R rules together with the AR rules could introduce unnecessary performance overheads such as axiom scheduling, processing and maintenance as we discussed in Sect. 3. In our approach, we separate TBox reasoning, ABox relation computation and ABox type computation. This helps reduce memory usage and computation time.
AR⊑ {{aa}} ⊑⊑ DE : D ⊑ E ∈ SR ∪ A AR∗H {a{}a}⊑⊑∃rE:D : ∃s:D → E ∈ SR; r ⊑∗O s AR∗T ∃{t:}{a⊑} ∃→r:DE : ∃s:D → E ∈ SR; r ⊑∗O t ⊑∗O s; T rans(t) ∈ O a AR− ⊓ a { } ⊑ D1; {a} ⊑ D2
{a} ⊑ D1 ⊓ D2 AR+ {a} ⊑ D1; {a} ⊑ D2 : D1 ⊓ D2 occurs in O
⊓ {a} ⊑ D1 ⊓ D2 AR+ {a} ⊑ D : r ⊑∗O s; ∃r:D occurs in O ∃ ∃s:{a} → ∃s:D
a AR⊥ {{b}} ⊑⊑ ⊥⊥ : {b} ⊑ ∃r:{a} ∈ SR AR∗⊥ {a{}a}⊑⊑∃r⊥:D : D ⊑ ⊥ ∈ SR ARH ∃s{:{b}a}⊑→EE : r ⊑∗O s; {b} ⊑ ∃r:{a} ∈ SR
∃s:{a} → E ART ∃t:{b} → E
: r ⊑∗O t ⊑∗O s; T rans(t) ∈ O; {b} ⊑ ∃r:{a} ∈ SR;
Now we defined the closure of applying all the rules: Definition 3. (Ontology Completion Closure) Let O = (T ; A) be an E LH⊥;R+ ontology, its ontology completion closure, denoted by S, is the smallest set of axioms closed under the AR rule set, with O axioms as side conditions, such thatSR ⊆ S; A ⊆ S (axioms mapped as elaborated at the beginning of this section); and for all a ∈ IN O, {a} ⊑ {a} ∈ XO, and {a} ⊑ ⊤ if ⊤ occurs in O.
Together the AR rules are also complete, sound and tractable. The soundness and tractability of rules are quite obvious. The completeness on ABox materialisation can be shown by the following Theorem: Theorem 1. For any E LH⊥;R+ ontology O = (T ; A), we have either there is some {x} ⊑ ⊥ ∈ S, or 1. O |= D(a) only if {a} ⊑ D ∈ S for D occurs in O; 2. O |= r(a; b) only if {a} ⊑ ∃s:{b}; s ⊑∗O r ∈ S for r ∈ RN O.
The result regarding roles is quite obvious due to Lemma 3 and item 1 in Def. 3. The type part can be proved by contrapositive. Assuming there is no {x} ⊑ ⊥ ∈ S, it’s obvious that the TBox T has a model. We can construct such a model based on ST and shows that it can be extended to a model of O based on S, such that this model entails a said class assertion only if it is in S. Full proof can be found in our technical report.
As we can see, the AR rules also preserve the feature that all premises of each rule have a same common part as the context. Therefore, they still enjoy the lock-free feature in reasoning. In later sections, we will further elaborate this point. 4.4
In this section, we present the parallel algorithm corresponding to the E LH⊥;R+
completion rules. We reuse some notions such as context, activeContexts queue, scheduled
queue and processed set from the original TBox algorithm for E LHR+ [
The revised saturation algorithm (Algorithm 1) is presented as follows. The saturation of an ontology is realised by first performing saturation of the non-class assertion axioms, the output of which (i.e., SR) is then used in the saturation of the class assertions. This yields S, which satisfies Theorem 1. This result contains all entailed class assertions, and all role assertions can be easily retrieved. All necessary tautology axioms must be added to the input prior to saturation. For TBox, we add axioms of the form C ⊑ C for all concepts C such that C ∈ CN O ∪ {⊥}. Similarly, for type computation we add {a} ⊑ {a} for all individuals a ∈ IN O.
Algorithm 1: saturate(input): saturation of axioms under inference rules Input: input (the set of input axioms)
Result: the saturation of input is computed in context:processed 1 activeContexts ← ∅; 2 axiomQueue:addAll(input); 3 loop 4 axiom ← axiomQueue:pop(); 5 if axiom = null then break; 6 for context ∈ getContexts(axiom) do 7 context:scheduled:add(axiom); 8 activeContexts:activate(context); 9 loop 10 11 12 13 14 15 context ← activeContexts:pop(); if context = null then break; loop axiom ← context:scheduled:pop(); if axiom = null then break; process (axiom); context:isActive ← false; if context:scheduled ̸= ∅ then activeContexts:activate(context);
In the saturation (Algorithm 1), the activeContexts queue is initialised with an empty set (line 1), and then all input axioms are added into an axiomQueue (line 2). After that, two main loops (lines 3-8 and lines 9-17) are sequentially parallelised. In the first main loop, multiple workers independently retrieve axioms from the axiomQueue (line 4), then get the contexts of the axioms (line 6), add the axioms into corresponding scheduled queues (line 7) and activate the contexts. In the second main loop, multiple workers independently retrieve contexts from the activeContexts queue (line 10) and process its scheduled axioms (line 15). Once context:scheduled is empty, context:isActive is set to f alse (line 16). A re-activation checking is performed (line 17) in case other workers have added new axioms into context:scheduled while the last axiom is being processed (between line 14 and line 16). This procedure will continue until the activeContexts queue is empty.
The getContext() method returns the context of an axiom, depending on the form of the axiom. In the following list, the concept C or {a} is the context.
C ⊑ D | D ⊑ ∃r:C | ∃s:C → E | D ⊑ ∃r:{a} | {a} ⊑ D
To activate a context, an atomic boolean value isActive is associated with each context to indicate whether the context is already active. A context is added into the activeContexts queue only if this value is f alse, which will be changed to true at the time of activation. The process() method covers items 2.(a), 2.(b), 2.(c) shown at the end of Sect. 2.2. We match the form of input axiom and check whether it has been processed before; if not it will be added into the processed set of the context. Based on the form of axiom, applicable completion rules can be determined. Meanwhile, checking if the conclusion is already in corresponding context’s processed set can be performed. Once a completion rule has been applied, the conclusion axioms and their forms are determined. Once a conclusion is derived, its contexts and whether they are definitely the same as the current context are determined. The conclusion axioms can directly be added into corresponding scheduled queues. 5
We implemented our algorithms in our PEL reasoner (written in JAVA). To evaluate
its performance we use the Amazon Elastic Computer Cloud (EC2) High-Memory
Quadruple Extra Large Instance. It has 8 virtual cores with 3.25 EC2 units each, where
each EC2 unit “provides the equivalent CPU capacity of a 1.0-1.2 GHz 2007 Opteron
or 2007 Xeon processor”. The instance has 60 GB memory allocated to JVM. Our
test cases include a real world TBox NotGalen with generated ABox. NotGalen− is
extracted from an earlier version of Galen (http://www.opengalen.org/) by removing
functional role assertions. It contains a moderate-size TBox with 2748 classes, 413
roles and no ABox. To populate the ontology we use the SyGENiA system [
For each ontology, we perform ABox materialisation. Note that not all the relations have to be computed in reasoning, but only the necessary ones as indicated in Theorem 1. Nevertheless all relations can be retrieved very easily if needed. Results of our implementation PEL are presented in Table 2. The time shown in our evaluation is the overall computation time. Time unit is second.
From the comparison between different numbers of workers in Table 2 we can see that multiple parallel workers can indeed improve the reasoning performance, even when the ontology contains complex TBox and very large number of individuals. In general, the performance improves when more and more workers are used. With more than 4 workers, the performance may decrease on very large ABoxes. We believe one of the potential reasons is that although the CPU cores can work in parallel, the RAM bandwidth is limited and RAM access is still sequential. In relatively “light-weight” ABox reasoning with large ABox, the RAM access will be enormous and very often so that multiple workers will have to compete for RAM access. This makes memory I/O a potential bottleneck of parallelisation and wastes CPU cycles. Another potential reasoner is that with such a large Jave heapsize, the memory management of the JVM will take quite some time. A better management of memory will be an important direction of our future work. 6
In this paper we extended early related work to present a parallel ABox reasoning approach to E LH⊥;R+ ontologies. We proposed new completion rules to improve efficiency and scalability of parallel ABox reasoning, and showed that they are complete and sound for ABox reasoning. Our evaluation shows that ABox reasoning can benefit from parallelisation, even for very large ABoxes. In future, We would like to continue the work in two directions. One is to develop distributed algorithms so that the memory cost can also be distributed. The other is to develop target-driven materialisation instead of full materialisation to reduce memory cost.
Yuan Ren and Jeff Z. Pan are partially funded by the EU FP7 K-Drive project.