Embracing Change by Abstraction Materialization Maintenance for Large ABoxes

1 Introduction

Most ontology reasoners support the task of materialization (i.e., they compute and explicitly store all entailed atomic concept and role assertions for the individuals in the ontology), which allows for directly evaluating conjunctive instance queries. Computing the materialization is computationally expensive and approaches such as summarization [Dolby et al., 2009], ABox modularization [Wandelt and M¨oller, 2012], or Abstraction Refinement [Glimm et al., 2014; 2017] attempt to "compress" the size of the dataset over which the materialization is computed to be able to materialize large ABoxes. Even using efficient materialization techniques, recomputing all consequences whenever input data changes can cause a significant delay before user queries can be answered again, which might be prohibitive for some application scenarios. Incremental maintenance algorithms originating from the database and Datalog communities (see, e.g., [Volz et al., 2003; Motik et al., 2015]) have been applied to description logics and the semantic web for incremental classification [Kazakov and Klinov, 2013], incremental materialization via Datalog [Volz et al., 2005] and RDF stream reasoning [Barbieri et al., 2010]. Apart from the technique used in the RDFox system [Motik et al., 2014], the mentioned materialization algorithms focus on and are optimized for ontologies that can be expressed in the form of (Datalog) rules, i.e., proper existentials are not supported. Furthermore, how incremental maintenance algorithms can be combined with data compression techniques is an open problem, only addressed in a sketchy way by Steigmiller et al. [Steigmiller et al., 2015] in the form of a representative cache maintaining individuals in an incremental fashion.

We address this problem by extending the Abstraction Refinement method s.t. abstractions capture information beyond the simple presence of assertions. This ultimately allows us to deal with changes of the underlying ABox. To show the correctness of the obtained theoretical framework, we devise novel proof techniques. Our empirical evaluation with synthetic and real-world ontologies shows up to four times improved materialization times compared to the approach without Abstraction Refinement in different change scenarios.

2 Preliminaries

The syntax of ALCHI is defined using a vocabulary consisting of countably infinite disjoint sets NC of atomic concepts, NR of atomic roles, and NI of individuals. A role is either an atomic role or an inverse role r- with r ∈ NR. We denote atomic roles with lower case and (possibly non-atomic) roles with upper case letters. We define R- := r- if R = r and R-:=r if R = r-. An ALCHI concept is defined as

where A ∈ NC and R is a role. Let C,D be concepts, R, S roles and a, b individuals. A TBox is a set of concept and role inclusion axioms of the form C ⊑ D and R ⊑ S, respectively. An ABox is a set of (concept and role) assertions of the form C(a) and R(a, b), respectively. An ontology O = A∪T consists of an ABox and a TBox. To simplify the presentation, we do not distinguish between R(a, b) and R-(b, a) as well as R ⊑ S and R- ⊑S-. We use con(O), rol(O), and ind(O) for the sets of atomic concepts, atomic roles, and individuals occurring in O, respectively.

An interpretation I = (∆I , ·I ) consists of a non-empty set ∆I , the domain of I, and an interpretation function ·I , that assigns to each A ∈ NC a subset AI ⊆ ∆I , to each R ∈ NR a binary relation RI ⊆ ∆I × ∆I , and to each a ∈ NI an element aI ∈ ∆I . This assignment is extended to roles by (r-)I = {〈e, d〉 | 〈d, e〉 ∈ rI } and, inductively, to complex concepts as ⊤I = ∆I , ⊥I = ∅, (¬C)I = ∆I \C I , (C ⊓D)I = C I ∩DI , (C ⊔D)I = C I ∪DI , and

An interpretation I satisfies an axiom α, written I |= α, if

α = C ⊑ D and C I ⊆ DI , α = R ⊑ S and RI ⊆ SI , α = C(a) and aI ∈ C I , or α = R(a, b) and 〈aI , bI 〉 ∈ RI ; I is a model of an ontology O, written I |= O, if I |= α for each α ∈ O; O entails an axiom α, written O |= α, if every model of O satisfies α.

An ALCHI ontology O is Horn [Kr¨otzsch et al., 2013] and in normalized form if, for every C(a) ∈ O, C ∈ NC and, every C ⊑ D ∈ O, is in one of the forms ⊤ ⊑ A, A ⊑ B,A ⊑ ∃R.B,A ⊑ ⊥,A ⊓ B ⊑ C,A ⊑ ∀R.B where A,B,C ∈ NC and R is a role. W.l.o.g., we assume in the remainder every ontology as normalized by applying a structural transformation; see e.g. [Kazakov, 2009].

For ALCHI ontologies, determining entailed role assertions can easily be done using a precomputed role hierarchy. Hence, we focus on the task of computing entailed concept assertions: For an ontology O = A∪T , we say that A is materialized w.r.t. T , if O |= A(a) implies A(a) ∈ A for each A ∈ con(O) and a ∈ ind(O). The materialization of A w.r.t. T is the smallest super-set of A that is materialized w.r.t. T .

2.1 Abstraction Refinement

The main idea of the Abstraction Refinement method [Glimm et al., 2014; 2017] is to materialize an ontology O = A ∪ T with a potentially large ABox A by constructing a smaller ABox B s.t. the materialization of B ∪T can be computed by a general-purpose reasoner, and transferring the new entailments back to O. The ABox B is usually called the abstraction of the original ABox A. Homomorphisms are used for transferring back entailments:

Definition 1. For A and B ABoxes, a mapping h: ind(B) → ind(A) is called a homomorphism (from B to A) if h(B) = ∪α∈Bh(α) ⊆ A, where h(C(a)) := C(h(a)) and h(R(a, b)) := R(h(a), h(b)). An individual b ∈ ind(B) is a representative of an individual a ∈ ind(A) if there exists a homomorphism h: ind(B) → ind(A) s.t. h(b) = a.

The following property enables the transfer of entailments:

Lemma 1. Let h: ind(B) → ind(A) be a homomorphism between the ABoxes B and A. Then, for every TBox T and every axiom β, B ∪ T |= β implies A∪ T |= h(β).

Abstractions are based on asserted roles and concepts for single individuals using types:

Definition 2 (Type). Let A be an ABox and a an individual. The concept type of a w.r.t. A is a set of concepts τC(a) = {C | C(a) ∈ A}. The role type of a w.r.t. A is a set of roles τR(a) = {R | ∃b : R(a, b) ∈ A}. The (combined) type of a w.r.t. A is a pair (τC(a), τR(a)), where τC(a) and τR(a) are the concept and role type of a w.r.t. A, respectively.

The abstract ABox is then constructed by introducing one representative for each type with the respective assertions.

Definition 3 (Abstraction). Let τ = 〈τC, τR〉 be a type. The abstraction for τ is an ABox

Function update(∆B, A)

In: ∆B: abstract assertions, A: ABox

Out: ∆A: update using ∆B

1 ∆A← ∅

2

for C(vτ(a)) ∈ ∆B do

3

∆A ← ∆A ∪ C(a)

4

5

for R(a, b) ∈ A and C(wR

∆A ← ∆A ∪ C(b)

6

return ∆A

τ(a) ) ∈ ∆B do

Algorithm 1: materializeAR(O) In: O = A ∪ T : ontology Out: A∞: materialization of A w.r.t. T 1 A∞ ←A, ∆A← ∅ 2 repeat 3 A∞ ←A∞ ∪∆A // not needed in loop round 1 4 Let B be the abstraction of A (Definition 3) 5 Let B∞ be the materialization of B w.r.t. T 6 ∆B ←B∞ \ B, ∆A←update(∆B, A) 7 until ∆A ⊆ A∞ 8 return A∞

where vτ and wR τ are distinguished abstract individuals for the type τ . The abstraction of an ABox A is ⋃a∈ind(A) Bτ(a), where τ(a) is the type for a w.r.t. A.

Example 2. The abstraction for A in Example 1 is B = Bτ(a) ∪ Bτ(b), where Bτ(a) = Bτ1 = {A(vτ1 ), r(vτ1 , wr τ1 )}, Bτ (b) = Bτ2 = {A(vτ2 ), r-(vτ2 , wrτ2 )}.

Intuitively, the abstraction is a disjoint union of ABoxes simulating combined types. Note that each mapping h: ind(B) → ind(A) s.t. h(vτ) ∈ {a ∈ ind(A) | τ(a) = τ}, and h(wR τ ) ∈ {b ∈ ind(A) | R(h(vτ), b) ∈ A} is a homomorphism from B to A, which allows for transferring entailments from the abstraction back to the original ABox (Lemma 1). For B∞ the materialization of B ∪ T and ∆B = B∞ \ B, the function update(∆B, A) uses the above defined homomorphism to generate an update using ∆B.

Algorithm 1 then defines the Abstraction Refinement method for materializing a Horn ALCHI ontology. The loop is repeated until a fix-point is reached and the update contains no assertions not already present in the materialization. The method is sound, complete, and terminating for Horn ALCHI [Glimm et al., 2014] and, with some extensions, even for Horn SHOIF [Glimm et al., 2017].

3 Incremental Materialization

For computing the materialization, we compute the closure of the ABox assertions using a modified version of the materialization rules given by Glimm et al. (2017) for Horn SHOIF restricted to Horn ALCHI as shown in Figure 1. Premises are given above the horizontal line and the conclusions below. Side conditions are given after the colon and restrict the expressions to which the rules are applicable. For example, rule

Figure 1: Materialization rules (A, B ∈ NC, R, S roles, a, b ∈ NI)

R⊑ produces one inference for each individual a and concepts A1, . . . ,An,B s.t. T |= A0 ⊓ . . . ⊓ An ⊑ B with the premise {A1(a), . . . , An(a)} and the conclusion B(a). Note that TBox axioms are only used in side conditions and never as premises of the rules, which allows us to focus on ABox reasoning and leave TBox reasoning to a suitable reasoner. Theorem 1 can be shown in a very similar (but simpler) way to the proof used by Glimm et al. (2017).

Theorem 1. The rules in Figure 1 are sound and complete for the materialization of a normalized Horn ALCHI ontology.

3.1 The Delete/Rederive Algorithm

For the changes, we adopt the database view, in which only known ABox facts can be added or deleted. This already provides enough expressivity for many use cases, e.g. stream reasoning [Barbieri et al., 2010]. Due to the monotonicity of DL reasoning, additions can be handled by simply 'continuing' materialization. Hence, we only focus on deletions and assume: Given a Horn ALCHI ontology O = A ∪ T , the materialization A∞ of A w.r.t. T , and a set A- ⊆ A of deletions, we want to determine the materialization of A \ Aw.r.t. T using A∞. This is non-trivial and requires the identification and removal of assertions in A∞ no longer derivable from A \ A-. The Delete/Rederive (DRed) algorithm [Gupta et al., 1993; Staudt and Jarke, 1996] initially overestimates the necessary deletions and then determines facts still derivable from A \ A-. The overestimation is obtained by continuously (over-)deleting facts, which can be derived using already deleted facts. We formalize this using restricted rule applications.

Definition 4 (Restricted Derivation). Given a set of deduction rules R, an ontology O = A∪ T , and an ABox A′ , an axiom α can directly be derived from O under restriction A′ , written O ⊢RA′ α, if α can be derived from O by a rule in R s.t. at least one of the premises is in A′ .

In the remainder, we simply write A∪ T ⊢A′ α and assume R to consist of the rules from Figure 1.

For the presentation of the DRed algorithm, we follow the presentation style of Motik et al. (2015), but we adapt it to a consequence-based calculus, to avoid complications with ensuring termination of a Datalog program in the presence of function symbols, which are required to handle existential quantifiers. DRed, formalized in Algorithm 2, consists of three consecutive phases: (1) compute the overdeletion, (2) rederive deletions with an alternative derivation in one step, (3) reinsert facts with alternative derivations. Phase (1) and (3) can directly be used to extend the Abstraction Refinement method for incremental materialization maintenance.

Function reinsert(T , A∞new , Dnew) In: T : TBox, A∞new : overdeletion, Dnew: rederivation Out: A∞new : materialization of A \ A- w.r.t. T 1 Dprev ←Dnew \A∞new 2 while Dprev ̸= ∅ do 3 A∞new ← A∞new ∪ Dprev, Dnew ← {α | A∞new ∪ T ⊢Dprev α}, Dprev ← Dnew \ A∞new 4 return A∞new

Hence, we define the according functions overdelete and reinsert, which are then used in Algorithm 2. The computed set of deletions Dall in the function overdelete can be seen as a sort of closure for A∞ ∪ T ⊢Dall α. The search for facts with an alternative derivation in the reinsertion phase is restricted to assertions in the overdeletion set Dall using an additional premise for the derivation rules. The computed set Dnew is then used in Phase (3) by the function reinsert to restore the correct materialization. Rule applicability is restricted to avoid unnecessary rule applications. Although Dall does not appear in the reinsertion phase, due to the way the overdeletion is generated, Phase (3) determines A∞new as a closure for A∞new ∪ T ⊢A∞new∩Dall α.

3.2 DRed and Abstraction Refinement

We adopt DRed in the general Abstraction Refinement way: We construct, for each of the different phases, suitable abstractions of the ABox on which we perform the respective operations. Interleaved refinement steps (for overdeletion and reinsertion repeatedly until the fix-point) transfer results back to the original ABox and yield an adapted abstraction. Since DRed operations on abstractions additionally require knowledge about the set of deletions, we extend the original definitions to bi-types and bi-abstractions.

Definition 5 (Bi-Type). Given ABoxes A1, A2, the bi-type of an individual a ∈ ind(A1 ∪A2) w.r.t. (A1,A2) is a quadruple (τ 1C (a), τ 1R(a), τ 2C (a), τ 2R(a)), where (τ 1C (a), τ 1R(a)) is the combined type of a w.r.t. A1 and (τ 2C (a), τ 2R(a)) is the combined type of a w.r.t. A2.

Definition 6 (Bi-Abstraction). Given two ABoxes A1, A2 and a bi-type τ = (τ 1C , τ 1R, τ 2C , τ 2R) w.r.t. (A1,A2), the bi-abstraction for τ is an ABox B1 τ ∪B2 τ , where B1 τ = {C(vτ) | C ∈ τ 1C } ∪ {R(vτ ,wR τ ) | R ∈ τ 1R}, B2 τ = {C(vτ) | C ∈ τ 2C } ∪ {R(vτ ,wR τ ) | R ∈ τ 2R}, and vτ and wR τ are distinguished abstract individuals for the bi-type τ. The

Algorithm 2: DRed(O, A∞, A-)

• In: O = A ∪ T : ontology, A∞: materialization, A-: deletions

Out: A∞new : materialization of A \ A- w.r.t. T

▷ overdeletion phase

◁

• 2 A∞new ← A∞ \ Dall, Dnew ← Dall ∩ (A \ A-)
• 3 Apply the rules (Fig. 1) to A∞new w.r.t. T s.t. the conclusion is added to Dnew and with the additional side condition that the conclusion occurs in Dall

▷ reinsertion phase

◁

• 4 A∞new ← reinsert(O, A∞new , Dnew)
• 5 return A∞new

bi-abstraction of (A1, A2) is B = B1 ∪ B2 with

where τ(a) is the bi-type for a w.r.t. (A1,A2) and B1

B2

τ(a) is the bi-abstraction for τ(a).

The following example highlights how bi-abstractions also differentiate types based on their (over-)deleted assertions, while still aggregating 'similar' cases.

Example 3. Let A = {A(a1),A(a2),A(a3),r(a1,b),r(a2,b), r(a3, b)} and A- = {A(a1),A(a3)}, the combined type of a1, a2, and a3 w.r.t. A is ({A}, {r}). To distinguish a1 and a3 from a2, we consider the bi-types w.r.t. (A \ A-,A-): τ (a1) = τ (a3) = (∅, {r}, {A}, ∅), τ (a2) = ({A}, {r}, ∅, ∅), τ (b) = (∅, {r-}, ∅, ∅).

Similar to the DRed algorithm, the Abstraction Refinement Delete and Rederive algorithm (ARDRed) consists of three consecutive phases: (1) compute the overdeletion using the function overdelete on abstractions followed by the refinement step until a fix-point is reached, (2) rederive deletions in the abstraction with an alternative derivation in one step, (3) reinsert facts with alternative derivations using Abstraction Refinement. For the reinsertion phase, we again restrict the derivation rules using the second part of bi-types, which represents the deleted assertions, as opposed to using the overdeletion set Dall in DRed.

We note two things about the overdeletion phase of Algorithm 3: First, the input ABox B1 ∪ B2 for overdelete is not necessarily fully materialized, which can delay some derivations until the next loop round. Second, the function update uses the initial role assertions in A∞, i.e. deletions are also propagated over deleted roles. The rederivation phase does not share parts with DRed (Algorithm 2), as we cannot restrict rederivations in a similar way, due to missing information about the concept deletions for role successors.

3.3 Correctness

It can easily be verified that the Abstraction Refinement aspects of the rederivation and reinsertion phases operate like the original Abstraction Refinement procedure and that the used rules are sound. Hence, soundness follows from the completeness of the overdeletion phase, i.e. we need to show

τ(a) ∪

Algorithm 3: ARDRed(O, A∞, A-)

In: O = A ∪ T : ontology, A∞: materialization,

7 A∞new ← A∞ \ Dall, Dnew ← Dall ∩ (A \ A-), Enew ← ∅

• 8 Let B1 ∪ B2 be the bi-abstraction w.r.t. (A∞new, Dall)
• 9 Apply the rules (Fig. 1) to B1 w.r.t. T s.t. the conclusion is added to Enew and with the additional side condition for R⊑ that the conclusion occurs in B2

11 while Dnew \ A∞new ̸= ∅ do

12 A∞new ←A∞new ∪Dnew

13 Let B1 ∪B2 be the bi-abstraction w.r.t. (A∞new,Dall)

• 14 Enew ←reinsert(T , B1 , B1 ∩B2)
• 15 Dnew ←update(Enew \ B1 , A∞new )

16 return A∞new

that assertions no longer derivable from A \ A- are not present when starting the rederivation phase. We make the notion of overdeletion precise using ABox justifications:

Definition 7 (ABox Justification, Overdeletion). Let O = A ∪ T be an ontology. For an axiom α s.t. O |= α, an ABox justification w.r.t. T is any set J ⊆ A s.t. J ∪ T |= α; J is minimal, if ∀J ′ ⊂ J : J ′ ∪ T ̸|= α.

Let A∞ be the materialization of A w.r.t. T and A- ⊆ A deletions. Any superset of the set {α ∈ A∞ | J ∩ A- ̸= ∅ for J ⊆ A a minimal ABox justification for α w.r.t. T } is an overdeletion of A∞ w.r.t. A-.

For the overdeletion and reinsertion phases, we execute functions overdelete and reinsert over biabstractions and use homomorphisms to transfer the obtained results. Both functions construct closures via restricted derivations. For our argumentation, we consider two important properties induced by restricted derivations:

Lemma 2 (Restricted Derivation Properties). Let O = A ∪ T be an ontology and A1,A2 ABoxes with A1 ⊆ A2, ind(A1) ⊆ ind(A) and B an ABox, s.t. there is a homomorphism h : ind(A) → ind(B) from A to B. Then the following properties hold for any assertion α:

The overdeletion/reinsertion phases terminate after reaching the fix-point, where no further information can be transferred using homomorphisms. We show that, in the fixpoint, the closures constructed over bi-abstractions can be lifted up to closures over the original ABoxes. For the inner overdeletion (line 5), we have B1 ∪ B2 as the bi-abstraction w.r.t. (A∞ \ Dall,Dall) (line 4). The inner overdeletion (line 5) extends B2 with assertions α to determine a closure over B1 ∪B2 ∪ T ⊢B2 α. For the inner reinsertion, we have B1 ∪ B2 as the bi-abstraction w.r.t. (A∞new,Dall) (line 13). The inner reinsertion (line 14) constructs a closure for B1 ∪ T ⊢B1∩B2 α. Note that, compared to the closure constructed by reinsert in the DRed algorithm, this is actually a restriction since (bi-)abstractions only contain concept assertions for individuals of the form vτ . Still, this restriction does not affect the final result. We can lift these closures up to A∞ ∪ T ⊢Dall α for the overdeletion and A∞new ∪ T ⊢A∞new∩Dall α for the reinsertion. Lemma 3 provides the proof for the overdeletion phase. The proof for the reinsertion phase is analogous.

Lemma 3 (Overdeletion Fix-Point). Let O = A ∪ T be a normalized Horn ALCHI ontology with materialization A∞ and deletions A- ⊆ A. Further, let Dall be s.t. A- ⊆ Dall ⊆ A∞ and B = B1 ∪ B2 the bi-abstraction w.r.t. (A∞ \ Dall , Dall).

For each individual a ∈ ind(A) with bi-type τ = (τ 1C , τ 1R, τ 2C , τ 2R), each atomic concept A ∈ con(O), and each role R ∈ rol(O), if

1. B1 ∪ B2 ∪ T ⊢B2 A(vτ ) implies A(a) ∈ Dall and
2. B1 ∪B2 ∪ T ⊢B2 A(wR τ ) and R(a, b) ∈ A implies A(b) ∈ Dall,

then, for each assertion α s.t. A∞ ∪ T ⊢Dall α, α ∈ Dall.

Sketch. Extend B =B1 ∪B2 to B′ = B1′ ∪ B2′ as follows: If r(a, b) ∈ A∞ \ Dall, extend B1 with r(vτ(a), vτ(b)); if r(a, b) ∈ A-, extend B2 with r(vτ(a), vτ(b)). Note that there is a homomorphism h from A∞ to B′ , thus, by Lemma 2 (2), if A∞ ∪ T ⊢Dall α, then B′ ∪ T ⊢h(Dall) h(α). We can then show that h(Dall) ⊆ B2′ , hence, by B′ ∪ T ⊢B2′ h(α).

We next sketch why B′ has the same atomic concept assertions as direct derivations under restriction B2′ as B under restriction B2 . Let r(a, b) ∈ A∞. By considering the construction of B′ from B, the rules in Figure 1 and the conditions of restricted derivations, we can show that introducing the new role assertion r(vτ(a), vτ(b)) does not result in new restricted entailments. Hence, according to condition 1, A(a) ∈ Dall.

Lemma 4 (Soundness). Let O=A∪ T be a Horn ALCHI ontology, A∞ the materialization of A w.r.t. T , A- ⊆ A a set of deletions, and A∞new the result of ARDRed(O, A∞, A-). If α ∈ A∞new , then (A\A-) ∪ T |= α.

Sketch. We mainly need to show that the set Dall obtained as a closure according to Lemma 3 is complete and contains all assertions that are to be removed in the sense of Definition 7. To the contrary of what is to be shown, assume there is some α /∈ Dall s.t. a minimal ABox justification J for α contains an assertion from A-. By Theorem 1, α can be derived via a number of rule applications from J and, thus, there is a number of premises, of which at least one also has a minimal ABox justification J ′ ⊆ J with J ′ ∩ A- ̸= ∅. By doing so repeatedly, we eventually determine some assertion β s.t. A∞ ∪ T ⊢Dall β, which is a contradiction. The ARDred algorithm removes Dall from A∞ and, as shown earlier, only sound assertions are reinserted.

We now show completeness using the previous results.

Lemma 5 (Completeness). Let O = A ∪ T be a Horn ALCHI ontology, A∞ the materialization of A w.r.t. T , A- ⊆ A a set of deletions, and A∞new the result of ARDRed(O, A∞, A-). If (A \ A-) ∪ T |= α, then α ∈ A∞new .

Sketch. First, we consider the inputs A∞new and Dnew as they are used in the closure construction of the reinsertion phase. By Lemma 4, Dall contains the overdeletion of A∞ w.r.t. A-. For A∞new , we can then confirm that A \ A- ⊆ A∞new using the definition of the algorithm. For Dnew, we need to consider the effects of the rederivation phase. Using the rules in Figure 1 and the construction of the bi-abstraction B1 ∪ B2, we can show that Dnew is determined s.t. it contains at least all assertions, which can directly be rederived from A∞ \ Dall. It remains to show that under these conditions, constructing A∞new as a closure over A∞new ∪ T ⊢A∞new∩Dall α results in A∞new s.t. (A\A-)∪T |= α implies α ∈ A∞new . Assuming the contrary, let α be some concept assertion, s.t. (A\A-)∪T |= α and α /∈ A∞new . Due to the initial construction of A∞new , there must be some 'initial culprit' β /∈ A∞new , which can directly be derived from A∞new using a rule from Figure 1. We can then show that the conditions of the construction of A∞new are violated.

Theorem2 (Correctness). Let O=A∪T be aHornALCHI ontology, A∞ the materialization of A w.r.t. T , A- ⊆ A a set of deletions. ARDRed(O, A∞, A-) terminates and the returned A∞new is s.t. α ∈ A∞new iff (A\A-) ∪ T |= α.

Sketch. The overdeletion and reinsertion loops of the algorithm terminate and, once an iteration cannot determine new assertions, we obtain the termination of the algorithm as a direct consequence of the already shown soundness (Lemma 4) and completeness (Lemma 5) results. In particular, termination occurs in the worst case, when Dall = A∞ (overdeletion) and A∞new = A∞ (reinsertion).

4 Implementation and Evaluation

For the evaluation, we focus on directly comparing the algorithms, i.e. classical DRed and ARDRed. To do so, we have implemented both from scratch in Java including support for additions. The code and the experimental data are publicly available [Glimm and Brenner, 2018]. As basis for the test cases, we used the UOBM benchmark [Ma et al., 2006], for which we generated instances of 10, 50 and 100 universities (denoted UOBM10, UOBM50, and UOBM100, respectively) and the well-known NPD and Reactome ontologies. All ontologies were preprocessed by dropping non-Horn ALCHI axioms and by normalizing the remaining axioms. Table 1 shows the number of TBox and ABox axioms of the preprocessed ontologies.

An incremental test consists of a TBox T and a base ABox A from which we obtain an initial ABox A0 and 100 change ABoxes containing assertions to be either added or deleted, depending on the test scenario. Each change ABox contains all assertions for 1% of the individuals from A. 1 We evaluate three scenarios: (1) add-only starts with an almost empty A0 and step by step adds the change ABoxes; (2) remove-only starts with A0 = A and then removes the change ABoxes; (3) add-remove alternates between additions and removals, starting with two initial addition steps to avoid adding/removing the same individuals over and over again. All tests were executed on a server with two Intel hexa core processors at 2.60GHz (without using parallelization) and each test execution was assigned 200 GB of the overall 500 GB RAM to allow for keeping all test data in memory to avoid I/O impact. The number of 100 change ABoxes is large enough to even out JVM behavior (e.g. code optimization at runtime).

Results are shown in Table 1 and visualized in Figure 2. It can be seen that our approach outperforms the classical DRed implementation in almost all cases. We can also observe the typical Abstraction Refinement behavior, in that the advantage of ARDRed over DRed increases with the ABox size: For UOBM10, DRed still outperforms ARDRed in the addonly and remove-only cases. Figure 2c shows initial reasoning times stacked under the streaming times to display accumulated results. When running an incremental reasoning system for a longer time period, initial reasoning times eventually become irrelevant. Considering this argument, ARDRed behaves slightly worse than DRed for NPD and Reactome in the remove-only case. Our analysis shows that this is due to the unoptimized bi-types, which currently require individuals to start with the same materialization and to receive the same deletions, to be classified into the same type and we presume that this restriction is too strong for practical ontologies. This does not seem to be a problem for the UOBM ontologies, which we attribute to the synthetic data generation. The improvement achieved by ARDRed over DRed is less noticeable than that for non-incremental materialization by Abstraction Refinement. We attribute this to a generally increased overhead of the abstraction construction and refinement aspects in the incremental setting, which is confirmed by the fact that the initial materialization times for A0 in the remove-only setting are comparable to those of the original Abstraction Refinement approach. The runtimes of the add-remove case are generally lower than the runtimes of the add-only case, which in return are lower than those of the remove-only case. The first can be explained by the general number of assertions, which is lower in the add-remove case (as we keep adding and removing the same number of individuals). The second result is also to be expected, as deletion of assertions is far more expensive than adding assertions.

1 We exclude individuals which are used like nominals (implicitly belonging to the terminological part), e.g. the individual realizing the SwimmingClass concept in UOBM. Such individuals make up far less than 1% of the total individuals.

5 Conclusion and FutureWork

The introduced novel materialization maintenance algorithm for Horn ALCHI ontologies combines DRed and Abstraction Refinement. Benefits of this approach lie in the summarization of similar deletion and reasoning tasks, paving the road for efficient maintenance of materializations of large ABoxes.

For the implementation, further optimizations for the Abstraction Refinement part (e.g. caching of types, further summarization of types in the overdeletion) and the DRed part (e.g. integrating the Backward/Forward optimization [Motik et al., 2015]) are paths to be explored.

Acknowledgements

This work was done within the project "Reasoning over Large Amounts of Data in Ontologies via Abstraction and Refinement" (GL 779/3-2) and the Transregional Collaborative Research Centre SFB/TRR 62 "Companion-Technology for Cognitive Technical Systems" funded by the German Research Foundation (DFG).