Incremental Materialization Update via Abstraction Re nement

Abstract

ions instead of operating on a large ABox. We also show that the obtained procedure is sound and complete for Horn ALCHI ontologies.

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 the evaluation of conjunctive instance queries directly over the stored facts. Computing the materialisation is computationally expensive and approaches such as summarization [ 3 ], ABox modularization [ 16 ], or abstraction re nement [ 5 ] attempt to \compress" the size of the dataset over which the materialization is computed, thereby enabling processing of large ABoxes and reducing the number of recurring reasoning steps. Even using e cient materialization techniques, recomputing all consequences whenever input data changes can cause a signi cant 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., [ 14, 10 ]) have been applied to description logics and the semantic web for incremental classi cation [ 6, 13 ], incremental materialization via Datalog [ 15 ] and RDF stream reasoning [ 2 ]. While the basic idea of incremental maintenance algorithms is generally applicable, the presented algorithms so far 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. [ 12 ] in the form of a representative cache maintaining individuals in an incremental fashion.

In this paper we address this problem by combining the abstraction re nement technique for materialization of Horn ALCHI ontologies with the wellknown Delete/Rederive (DRed) algorithm for materialization management. 2

Preliminaries

The syntax of ALCHI is de ned using a vocabulary consisting of countably in nite 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 2 NR. We de ne R := r if R = r and R := r if R = r . For general semantics and complex concepts and axioms, we conform to the standard de nitions and refer the reader to e.g. Baader et al. [ 1 ]. An ontology O is a nite set of axioms, written as O = A [ T , where A is an ABox consisting of the concept and role assertions in O and T a TBox consisting of the concept and role inclusion axioms in O. We also refer to concept and role assertions simply as assertions. To simplify the presentation, we do not distinguish between axioms R(a; b), R v S and, respectively, R (b; a), R v S . We use con(O), rol(O), and ind(O) for the sets of atomic concepts, atomic roles, and individuals occurring in O, respectively. Given an ontology O = A [ T , an ABox justi cation w.r.t. T for an axiom with O j= is any set J A s.t. J [ T j= . An ABox justi cation J is minimal, if 8J 0 J : J 0 [ T 6j= . An ALCHI ontology O is Horn [ 9 ] and in normalized form if, for every C(a) 2 O, C is an atomic concept and every concept inclusion C v D 2 O, is in one of the following forms > v A; A v B; A v 9R:B; A v ?; A u B v C; A v 8R:B where A; B, and C are atomic concepts 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. [ 8 ].

For an ontology O = A [ T , we say that A is concept-materialized w.r.t. T , if O j= A(a) implies A(a) 2 A for each A 2 con(O) and a 2 ind(O); A is role-materialized w.r.t. T if O j= r(a; b) implies r(a; b) 2 A for each r 2 rol(O) and a; b 2 ind(O); A is (fully) materialized w.r.t. T if it is concept-, and role-materialized. Given an ontology O = A [ T , the concept-, role-, and/or (full) materialization of A w.r.t. T of is the smallest super-set of A that is concept-, role-, and/or fully materialized w.r.t. T , respectively. Note that the full materialization of A w.r.t. T is always nite since the sets con(O), rol(O) and ind(O) are nite. Since the role materialization of an ALCHI ontology can be determined quickly using a precomputed role hierarchy, we focus on concept materialization in the remainder. 2.1 The main idea of the abstraction re nement method [ 4, 5 ] is to materialize an ontology O = A [ T with a potentially large ABox A by constructing a smaller ABox B such that the materialization of B [ T can be computed by a generalpurpose reasoner, and transferring the new entailments back to O. The ABox B is usually called the abstraction of the original ABox A. For transferring back entailments, we use homomorphisms: De nition 1. Let A and B be ABoxes. A mapping h : ind(B) ! ind(A) is called a homomorphism (from B to A) if, for every assertion 2 B, we have h( ) 2 A, where h(C(a)) := C(h(a)) and h(R(a; b)) := R(h(a); h(b)). We say an individual b 2 ind(B) is a representative of an individual a 2 ind(A) if there exists a homomorphism h : ind(B) ! ind(A) such that h(b) = a. We further extend h to ABoxes as h(B) = [ 2Bh( ).

Entailments can be transferred due to the following property.

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 j= implies A [ T j= h( ).

Suitable abstractions for ALCHI can be constructed by considering asserted roles and concepts for single individuals using types: De nition 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) = fC j C(a) 2 Ag. The role type of a w.r.t. A is a set of roles R(a) = fR j 9b : R(a; b) 2 Ag. The (combined) type of a w.r.t. A is a pair ( C ; R), where C (a) and R(a) are the concept and role type of a w.r.t. A, respectively.

Example 1. Let A = fA(a); A(b); R(a; b)g. Then C (a) = C (b) = fAg, R(a) = fRg, R(b) = fR g, (a) = 1 = hfAg; fRgi, and (b) = 2 = hfAg; fR gi.

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

De nition 3 (Abstraction). Let A be an ABox and = h C ; Ri a type. The abstraction for is an ABox B = fC(v ) j C 2 C g [ fR(v ; wR) j R 2 Rg, where v and wR are distinguished abstract individuals for the type . The abstraction of A is B = Sa2ind(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 = fA(v 1 ); R(v 1 ; wR1 )g, B (b) = B 2 = fA(v 2 ); R (v 2 ; wR2 )g. Intuitively, the abstraction is a disjoint union of ABoxes simulating combined types. Note that each mapping h : ind(B) ! ind(A) such that: h(v ) 2 fa 2 ind(A) j (a) = g; h(wR) 2 fb 2 ind(A) j R(h(v ); b) 2 Ag; is a homomorphism from B to A, which allows us to transfer entailments from the abstraction back to the original ABox (Lemma 1). We formalize these transferred entailments using De nition 4.

De nition 4. Let B be the abstraction of an ABox A (according to De nition 3), B1 be the (concept-)materialization of B [ T , and B = B1 n B. The update of A using B is the smallest set of assertions A such that:

C(v (a)) 2 R(a; b) 2 A; C(wR(a)) 2

B B;

C(a) 2 C(b) 2

A; A: (1) (2) (3) (4)

A1(a)

An(a) R(a; b) B(b)

: T j= A0 u : : : u An v 8S:B and T j= R v S

Using the de nitions above, the Abstraction Re nement method for reasoning over a Horn ALCHI ontology O = A [ T can be summarized as follows: AR1 Build the abstraction B of A using De nition 3 AR2 Determine the update A of A according to De nition 4, using a reasoner on B [ T and extend A with A.

AR3 Repeat from Step AR1 until no new entailments can be added to A.

Steps AR1 and AR2 are repeated until the procedure reaches a x-point. The method is sound, complete, and terminating for Horn ALCHI and, with some extensions, even for Horn SHOIF [ 5 ]. 3

Combining Abstraction Re nement with DRed

For computing the materialization of a Horn ALCHI ontology O = A [ T , we compute the closure of the ABox assertions using a slightly modi ed version of the materialization rules given by Glimm et al. [ 5 ] 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 Rv produces one inference for each individual a and concepts A1; : : : ; An; B such that T j= A0 u : : : u An v B with the premise fA1(a); : : : ; An(a)g and the conclusion B(a). Note that the axioms in the TBox T are only used in side conditions and never as premises of the rules, which allows us to focus on ABox reasoning and to leave TBox reasoning to a suitable reasoner. Lemma 2 can be shown very similarly (although in a much simpler way) to the proof used by Glimm et al. [ 5 ].

Lemma 2. The rules in Figure 1 are sound and complete for the conceptmaterialization of a normalized Horn ALCHI ontology. 3.1

The Delete/Rederive Algorithm While one can examine a variety of di erent knowledge base changes in the DL setting, we choose to adapt the database-based view, in which only known ABox facts can be added or deleted. This view already provides enough expressivity for a variety of use cases, e.g. stream reasoning [ 2 ]. Additionally, as additions of ABox facts can be handled by simply 'continuing' materialization using the new facts due to the monotonicity of DL reasoning, we also focus on deletions in the remainder. More precisely, we assume the following setting and notation in the remainder of the paper: Given a normalized ALCHI ontology O = A [ T , the materialization A1 of A w.r.t. T , and a set of assertions A A to be deleted, we want to determine the materialization of A n A w.r.t. T using A1. Doing so requires the identi cation and removal of assertions in A1 no longer derivable from A n A , which is a rather di cult task. The Delete/Rederive (DRed) algorithm [ 7, 11 ] therefore initially overestimates the necessary deletions and then determines facts still derivable from A n A . This overestimation is obtained by continuously overdeleting facts, which could be derived from already overdeleted facts. We formalize this behavior by de ning a form of restricted rule applications.

De nition 5 (Restricted Derivations). Given an ontology O = A [ T and an ABox A0, an axiom directly follows from A [ T under restriction A0, if either 2 A0 or if a rule from Figure 1 can be applied to A w.r.t T to derive and at least one of the premises is in A \ A0. If directly follows from A [ T under restriction A0, we write A [ T `A0 .

For the presentation of the DRed algorithm, we follow the presentation style of Motik et al. [ 10 ], but we adapt it to a consequence-based calculus. This avoids complications with ensuring termination of a Datalog program in the presence of function symbols, which are required to translate existential quanti ers. The algorithm further uses several auxiliary sets: the set Dall accumulates facts that might need to be removed from A1 due to the removal of A , the set Dnew gathers facts derived in the current iteration of rule application, and the set Dprev contains facts derived in the previous iteration of rule application. The DRed algorithm determines An1ew as the (concept-)materialization of (A n A ) w.r.t. T as follows: DR1 Set A = A n A , set Dnew = A , and set Dall = ;.

DR2 Set Dprev = Dnew n Dall. If Dprev = ;, then go to step DR4; DR3 Set Dall = Dall [ Dprev, set Dnew to the set of all assertions with A1 `Dprev . Repeat step DR2.

After this step, Dall contains all facts that might need to be deleted, so steps DR2{DR3 are called overdeletion.

DR4 Set An1ew = A1 n Dall, and set Dnew = Dall \ A.

DR5 Evaluate an extension of the rules in Figure 1 over An1ew w.r.t. T such that each premise additionally contains its conclusion, but restricted to match assertions in Dall and such that the conclusion is added to Dnew. This rederivation step adds to Dnew facts with an alternate derivation in the updated An1ew. The additional premise restricted to matches in Dall restricts rederivation only to facts from steps DR2{DR3.

DR6 Set Dprev = Dnew n An1ew. If Dprev = ;, then terminate; DR7 Set An1ew = An1ew [ Dprev, set Dnew to the set of all assertions with . Repeat step DR6. Steps DR6{DR7 are called (re)insertion.

An1ew `Dprev 3.2

Incremental Materialization via Abstraction Re nement We adopt DRed in the general abstraction re nement way: We construct, for each of the di erent phases, suitable abstractions of the ABox, on which we perform the overdeletion, rederivation and the reinsertion phase. Interleaved renement steps (in case of overdeletion and reinsertion repeatedly, until a xpoint is reached) transfer results back to the original ABox and yield an adapted abstraction.

While reasoning using standard abstraction re nement requires only knowledge about asserted concepts and roles, overdeleting and rederiving on abstractions additionally requires knowledge about the set of assertions that are to be deleted. To keep track of such assertions, we extend the de nitions of types and abstractions to bi-types ans bi-abstractions.

De nition 6 (Bi-Type). Given ABoxes A1; A2, the bi-type of an individual a 2 ind(A1 [ A2) w.r.t. (A1; A2) is a quadruple ( C1 (a); R1 (a); C2 (a); R2 (a)), where ( C1 (a); R1 (a)) is the combined type of a w.r.t. A1 and ( C2 (a); R2 (a)) is the combined type of a w.r.t. A2.

De nition 7 (Bi-Abstraction). Given two ABoxes A1, A2 and a bi-type = (whC1e;reR1B1 = fC(v ) j C 2 C1 g [ fR(v ; wR) j R 2 R1 g, B2 = fC(v ) j C 2 C2 g [ ; C2 ; R2 ) w.r.t. (A1; A2), the bi-abstraction for is an ABox B1 [ B2, fR(v ; wR) j R 2 R2 g, and v and wR are distinguished abstract individuals for the bi-type . The bi-abstraction of (A1; A2) is B = B1 [ B2; B1 = Sa2ind(A) B1(a); B2 = Sa2ind(A) B2(a); where (a) is the bi-type for a w.r.t. (A1; A2) and B1(a) [ B2(a) is the biabstraction for (a).

The following example highlights, how bi-abstractions also di erentiate types based on their (over-)deleted assertions, while still aggregating `similar' cases. Example 3. For A = fA(a1); R(a1; b); A(a2); R(a2; b); A(a3); R(a3; b)g and A = fA(a1); A(a3)g, the combined type of a1, a2, and a3 w.r.t. A is (fAg; fRg). To distinguish a1 and a3 from a2, we consider the bi-types w.r.t. (A n A ; A ) and obtain (a1) = (a3) = 1 = (;; fRg; fAg; ;) and (a2) = 2 = (fAg; fRg; ;; ;); furthermore, (b) = 3 = (;; fR g; ;; ;).

In our procedure, we use (similar to the DRed algorithm), auxiliary sets Dall, Eall, Dnew, Enew, and Eprev, where Eall, Enew and Eprev represent sets used within abstractions. The Abstraction Re nement Delete and Rederive algorithm (ARDred) determines An1ew as the (concept-)materialization of A n A w.r.t. T as follows: ARD1 Set Dnew = A and set Dall = ;.

ARD2 If Dnew n Dall = ;, then go to step ARD4.

ARD3 Set Dall = Dall[Dnew, set Dnew = ;. Build the bi-abstraction B = B1[B2 w.r.t. (A1 n Dall; Dall).

OD1 Set Enew = B2 and set Eall = ;. OD2 Set Eprev = Enew n Eall. If Eprev = ;, go to step OD4.

OD3 Set Eall = Eall [ Eprev, set Enew to the set of all assertions with

B1 [ B2 [ T `Eprev . Go to step OD2.

OD4 Determine Dnew as the update of Dall according to De nition 4, using Eall as B and the role assertions of A1 in line 4 of the de nition.

Continue with step ARD2.

This concludes the overdeletion phase of the algorithm.

ARD4 Set An1ew = A1 n Dall, set Dnew = Dall \ (A n A ).

ARD5 Let B = B1 [ B2 be the bi-abstraction w.r.t. (An1ew; Dall). Set Enew = ; and evaluate the rules in Figure 1 w.r.t. T over B1, s.t. conclusions are added to Enew and Rv additionally contains its conclusion as a premise restricted to match assertions in B2. Extend the assertions present in Dnew with the update to Dnew w.r.t. De nition 4, using Enew as B and the role assertions of A n A in line 4 of the De nition. Set Dnew = Dnew \ Dall.

This step is also referred to as the rederivation phase.

ARD6 Set Dprev = Dnew n An1ew. If Dprev = ; terminate.

ARD7 Set An1ew = An1ew [ Dnew. Construct the bi-abstraction B = B1 [ B2 w.r.t. (An1ew; Dall).

RD1 Set Enew = B1 \ B2, Eall = ;.

RD2 Set Eprev = Enew n Eall. If Eprev = ;, go to step RD4.

RD3 Set Eall = Eall [ Enew, set Enew to the set of all assertions with

B1 [ Eall [ T `Eprev . Continue with step RD2.

RD4 Determine Dnew as the update of An1ew according to De nition 4, using Eall as B and the role assertions of An1ew in line 4 of the De nition.

Continue with step ARD6.

Steps ARD6{RD4 form the (re-)insertion phase of the algorithm. Steps RD1{RD3 form the inner (re-)insertion phase.

Similar to DRed, we have an overdeletion (steps ARD1{OD4), a rederivation (steps ARD4{ARD5) and a reinsertion phase (steps ARD6{RD4). Similar to abstraction re nement, instead of determining the overdeleted, rederived and reinserted assertions on the original ABox, we determine assertions on suitable bi-abstractions and transfer the obtained results back, in case of overdeletion and reinsertion repeatedly, until a xpoint is reached.

The use of bi-types and bi-abstractions allows us to transfer the deletion set into B as B2. In the overdeletion phase, we (indirectly) extend B2 to ultimately extend the overdeletion Dall and construct the bi-abstraction over (A1 n Dall; Dall), such that B is still the abstraction of the complete materialization (as otherwise, not all assertions could be derived). The rederivation phase uses B2 to restrict possible derivations of rule Rv. Finally, the reinsertion phases determines rederived assertions using the `overlap' between B1 (created from An1ew) and B2, which allows us to reduce the number of possible derivations.

Note that there is a slight conceptual di erence in the overdeletion part of DRed (which always operates on a complete (concept-)materialization of an ABox) and the inner overdeletion (steps OD1{OD4), as the latter operates on B and not the (concept-)materialization of B. Thus, the inner overdeletion of ARDred also extends Eall with derivable assertions not in B.

Sound- and completeness of the algorithm strongly depends on the overdeletion phase (steps ARD1{OD4) for soundness (i.e. removing all axioms, which are no longer derivable) and the reinsertion phase (steps ARD6{RD4) for completeness (i.e. rederiving all axioms that are still derivable).

First, we want to x the notion of overdeletion for the following discussions. De nition 8 (Overdeletion). Let O = A [ T be an ontology, A A a set of assertions to be deleted and A1 the (concept-)materialization of A w.r.t. T . A set Dall A1 is an overdeletion of A1 w.r.t. A , if, for all 2 Dall, there is a minimal ABox justi cation J A for w.r.t. T , s.t. J \ A 6= ;.

As soundness of the algorithm is related to completeness of the overdeletion phase of the algorithm, we can in the following focus on two completeness proofs. To do so, we rst consider some properties of the restricted derivation relation of De nition 5. We can then show that determining a complete closure for restricted derivations in an abstraction re nement way ensures a similar closure over the original ABoxes. Finally, we use the obtained results to show completeness w.r.t. the base task, which is, respectively, overdeletion and rederivation. Lemma 3 (Properties of Direct Restricted Derivations). Let O = A [ T be an ontology and A1; A2 ABoxes with A1 A2, ind(A1) ind(A2) 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 :

A [ T `A1 A [ T `A1 implies A [ T `A2

: implies B [ T `h(A1\A) h( ): (Monotonicity) (5) (6) Proof (Sketch). Both properties can easily be veri ed using the assumptions, De nitions 1 and 5 and the rules in Figure 1. tu

Using De nition 5, we can describe the xpoint constructed by the overdeletion and reinsertion phases as follows: For B the bi-abstraction w.r.t. (A1 n Dall; Dall) (Step ARD3), the inner overdeletion phase extends B2 with assertions to determine a closure over B1 [ B2 [ T `B2 . Similarly, in the inner reinsertBio1nispehxatseen, dfoedr Bwi=thBa1s[seBrt2iotnhse bit-oabcsotnrastcrtuiocnt wa.crl.ot.su(rAen1oewve;rDBal1l)[(STte`pBA1\RB2D7.),

In both cases, the results of constructing the closure are transferred back to the original ABoxes using homomorphisms and updates. We proceed to show (roughly similar to the completeness proof of the original abstraction re nement approach [ 4 ]), that if no new assertions are transferred back to the original ABoxes, a corresponding xpoint on those original ABoxes (Dall in case of the overdeletion phase, An1ew in case of the reinsertion phase) has been reached. Theorem 1 (Overdeletion Fixpoint Theorem). Let O = A [ T be a normalized Horn ALCHI ontology, A1 the (concept-)materialization of A w.r.t. T and A A a set of axioms to be deleted. Let further Dall be an ABox with A Dall A1 and let B = B1[B2 be the bi-abstraction w.r.t. (A1nDall; Dall). Then it holds for all with A1 [ T `Dall , that 2 Dall, if for every bitype = ( C1 ; R1 ; C2 ; R2 ) of an individual a 2 ind(A), every atomic concept A 2 con(O) and every role R 2 rol(O), we have 1. B1 [ B2 [ T `B2 A(v ) implies A(a) 2 Dall. 2. B1 [ B2 [ T `B2 A(wR) and R(a; b) 2 A implies A(b) 2 Dall. Proof (Sketch). Extend B = B1 [ B2 with new role assertions to B0 = B10 [ B20 as follows: If R(a; b) 2 A1 n Dall, extend B1 with R(v (a); v (b)). If R(a; b) 2 A , extend B2 with R(v (a); v (b)). Note that there is a homomorphism from A1 to B0 and thus, according to Property 6 of Lemma 3, B0 [ T `h(Dall) , if A [ T `Dall . We then show that h(Dall) B20 and, therefore, B0 [ T `B20 . Thus, we are left to show, that the new role assertions provide no new derivations, as then the assumed properties assure the desired xpoint. tu

We brie y sketch the idea behind the proof, that B0 has the same atomic concept assertions as direct derivations under restriction B20 as B under restriction B2. It su ces to consider four individuals v1; v2; w1; w2 of the bi-abstraction, s.t. v1 = v (a); w1 = wR(a); v2 = v (b); w2 = wR(b) and R(a; b) 2 A1. By considering the construction of B0 and B and the rules in Figure 1 together with the conditions of restricted derivations, we can easily show that introducing the new role assertion R(v1; v2) does not result in new restricted entailments.

We can argue similar to the above, that An1ew is determined as the closure w.r.t. An1ew [ T `An1ew\Dall by the reinsertion phase, which concludes the completeness proofs of the overdeletion and rederivation phases w.r.t. restricted derivations. It is left to show, that rst of all, the results above are related to the task at hand (removing all axioms no longer entailed by AnA and rederiving all axioms still entailed by A n A ) and second, that the full algorithm is complete and sound w.r.t. the base task, which is, incrementally determining the changed materialization. We proceed to rst examine the overdeletion phase based on the previous results and extend this examination into the soundness proof for ARDred. We then examine the reinsertion phase and its preceding operations to ultimately deliver the completeness proof for ARDred.

For the overdeletion phase, we use the bi-abstraction w.r.t. (A1 n Dall; Dall) and construct Dall, such that A1 [ T `Dall implies 2 Dall. In particular, initially Dall = A . Consider the following Lemma.

Lemma 4. Given an ontology O = A [ T , the (concept-)materialization A1 of A w.r.t. T and a set of axioms to be deleted A A. Let Dall be a set s.t. A Dall and, if, for any concept or role assertion , A1 [ T `Dall , then 2 Dall. Then Dall is an overdeletion of A1 w.r.t. A according to De nition 8.

, s.t. A1 [ T `Dall Proof (Sketch). Assuming the contrary (i.e. 2= Dall), we argue by sound- and completeness of the rules in Figure 1, that can be derived via a number of rule applications from a minimal ABox justi cation J (as in Def. 8) and thus there is a number of premises, of which at least one also has a minimal ABox justi cation J 0 J with J 0 \ A 6= ;. By doing so repeatedly, we ultimately determine some assertion holds, which is a contradiction. tu

Thus, the overdeletion phase of the ARDred algorithm in steps ARD1{OD4 produces a correct overdeletion Dall of A1 w.r.t. A . Additionally, we remove this overdeletion from the materialization in step ARD4. Thus, it remains to be shown that no unsound assertions are reinserted afterwards.

Lemma 5. Given an ontology O = A [ T , a set of assertions to be deleted A A and the set An1ew of the ARDred algorithm after step ARD4. If, during the execution of the ARDred algorithm, an axiom is added to An1ew after step ARD4, then (A n A ) [ T j= .

Proof (Sketch). We argue that all newly added assertions are derived using sound rules on sound abstractions, but with additional restrictions. As the restrictions only remove derivations, all added assertions are sound. tu tu

Soundness follows from the previous considerations concerning overdeletion. Corollary 1 (Soundness of ARDred). Given an ontology O = A [ T , the (concept-)materialization A1 of A w.r.t. T and a set of axioms to be deleted A A. Let An1ew be the materialization obtained by executing the ARDred algorithm for O, A1 and A . Then 2 An1ew implies (A n A ) [ T j= .

For the completeness of the reinsertion part of the algorithm, we need to additionally consider the initial contents of the sets An1ew and Dall, as they are used in the closure construction. As shown before, Dall contains the overdeletion of A1 w.r.t. A . For An1ew, from step ARD4 and step ARD7, we see that A n A An1ew. Further, we show, that step ARD5 extends An1ew with at least all assertions, which can be directly rederived from A1 n Dall.

Lemma 6. Given an ontology O = A [ T , the (concept-)materialization A1 of A w.r.t. T and a set of axioms to be deleted A A. Let further Dall be the overdeletion of A1 w.r.t. A and An1ew = A1 n Dall. Then Dnew is extended by step ARD5 with all axioms 2= An1ew obtained by applying one rule from Figure 1 to A1 n An1ew.

Proof (Sketch). We obtain the desired result by examining all ways, in which a rule from Figure 1 can derive an assertion in one step and use the necessary preconditions to determine which assertions must be part of B1 and B2 as constructed by the algorithm in step ARD5. We then use this examination to show that all necessary assertions will also be derived on the abstraction (and be part of the generated update).

Using these preconditions together with the established closure properties of the reinsertion phase of the algorithm, we can now formulate the following theorem, which rather directly entails the completeness of the ARDred algorithm. Theorem 2. Given an ontology O = A [ T , the (concept-)materialization A1 of A w.r.t. T , a set of axioms to be deleted A A and the overdeletion Dall of A1 w.r.t. A . Let further An1ew be the smallest set, s.t. A1 n Dall An1ew, 2 An1ew.

A n A An1ew and, if any concept assertion can be derived from A1 n Dall by directly applying one of the rules from Figure 1 w.r.t. T , then 2 An1ew. Further extend An1ew to the smallest set, s.t. if An1ew [ T `An1ew\Dall for any concept assertion , then 2 An1ew. Then, for any concept assertion , (AnA )[T j= implies Proof. As 2= An1ew and due to the initial construction of An1ew, there must be some , s.t. is, so to speak, the initial culprit, i.e. 2= An1ew and can be derived directly from An1ew using a rule from Figure 1. We show that if there is any such , then the conditions of the construction of An1ew are violated. Corollary 2 (Completeness of ARDred). Given an ontology O = A [ T , the (concept-)materialization A1 of A w.r.t. T and a set of axioms to be deleted A A. Let An1ew be the materialization obtained by executing the ARDred algorithm for O, A1 and A . Then (A n A ) [ T j= implies 2 An1ew.

As both the overdeletion and reinsertion loop of the algorithm terminate after no new assertions could be determined in the previous iteration, we obtain the termination of the algorithm as a direct consequence of the sound- and completeness results. In particular, we terminate in the worst case, when Dall = A1 (overdeletion) and An1ew = A1 (reinsertion). 4

Conclusion and Future Work

We have introduced a way to incrementally maintain the (concept-)materialization of an ALCHI ontology by combining DRed and abstraction re nement and using a consequence-based reasoning procedure. We have further shown that the presented procedure is sound and complete. Bene ts of this approach lie in the summarization of similar deletion and reasoning tasks, paving the road for e cient maintenance of materializations of large ABoxes.

While the choosen presentation is appropriate for theoretical examinations, we will in the future focus on optimizations needed for a practical implementation and evaluation of the approach, to verify its practicality. For example, retaining results from previously materialized abstractions can reduce reasoning e orts, as results for unchanged types can be reused. Other optimizations will focus on better handling role deletions to avoid the currently large amount of unnecessary overdeletions (this can be done by either extending abstractions with a new role successor for deleted roles or by reducing role deletion to concept deletions using knowledge about propagated concepts) and on general ways to reduce the number of generated types while retaining sound- and completeness (one could, for example, only use the deletions of the previous abstraction-re nement round to generate bi-abstractions in the overdeletion phase), as a reduction in the number of types automatically entails a reduction in the overall computations. Finally, we want to incorporate approaches which tackle the general de ciencies of DRed, such as the Backward/Forward algorithm [ 10 ], which avoids unnecessary overdeletions by considering knowledge still asserted in A n A .

References

1. Baader , F. : The description logic handbook: Theory, implementation and applications . Cambridge university press ( 2003 )

2. Barbieri , D.F. , Braga , D. , Ceri , S. , Della Valle , E. , Grossniklaus , M. : Incremental reasoning on streams and rich background knowledge . In: Extended Semantic Web Conference . pp. 1 { 15 . Springer ( 2010 )

3. Dolby , J. , Fokoue , A. , Kalyanpur , A. , Schonberg , E. , Srinivas , K. : Scalable Highly Expressive Reasoner (SHER) . J. of Web Semantics 7 ( 4 ), 357 { 361 ( 2009 )

4. Glimm , B. , Kazakov , Y. , Liebig , T. , Tran , T. , Vialard , V. : Abstraction re nement for ontology materialization . In: Proc. of the 13th Int. Semantic Web Conference , ISWC 2014 . pp. 180 { 195 ( 2014 )

5. Glimm , B. , Kazakov , Y. , Tran , T. : Ontology materialization by abstraction re nement in horn SHOIF . In: Proceedings of the 31st AAAI Conference on Arti cial Intelligence . pp. 1114 { 1120 . AAAI Press ( 2017 )

6. Grau , B.C. , Halaschek-Wiener , C. , Kazakov , Y. , Suntisrivaraporn , B. : Incremental classi cation of description logics ontologies . Journal of Automated Reasoning 44 ( 4 ), 337 { 369 ( 2010 )

7. Gupta , A. , Mumick , I.S. , Subrahmanian , V.S.: Maintaining views incrementally . In: Proceedings of the 1993 ACM SIGMOD International Conference on Management of Data . pp. 157 { 166 . SIGMOD '93, ACM ( 1993 )

8. Kazakov , Y. : Consequence-Driven Reasoning for Horn SHIQ Ontologies . In: Proc. of the 21st Int. Joint Conf. on Arti cial Intelligence , IJCAI 2009 . pp. 2040 { 2045 ( 2009 )

9. Krotzsch, M. , Rudolph , S. , Hitzler , P. : Complexities of Horn Description Logics . ACM Trans. Comput. Log . 14 ( 1 ) ( 2013 )

10. Motik , B. , Nenov , Y. , Piro , R.E.F. , Horrocks , I. : Incremental update of datalog materialisation: the backward/forward algorithm . In: Proceedings of the 29th AAAI Conference on Arti cial Intelligence . pp. 1560 { 1568 . AAAI Press ( 2015 )

11. Staudt , M. , Jarke , M. : Incremental maintenance of externally materialized views . In: Proceedings of the 22th International Conference on Very Large Data Bases . pp. 75 { 86 . VLDB ' 96 , Morgan Kaufmann Publishers Inc. ( 1996 )

12. Steigmiller , A. , Glimm , B. , Liebig , T. : Completion graph caching for expressive description logics . In: Proceedings of the 28th International Workshop on Description Logics. CEUR Workshop Proceedings , vol. 1350 . CEUR-WS.org ( 2015 ), http://ceur-ws. org/ Vol- 1350 /paper-35.pdf

13. Suntisrivaraporn , B. : Module extraction and incremental classi cation: A pragmatic approach for el+ el^+ ontologies . The Semantic Web: Research and Applications pp. 230 { 244 ( 2008 )

14. Volz , R. , Staab , S. , Motik , B. : Incremental maintenance of materialized ontologies . In: On The Move to Meaningful Internet Systems 2003 : CoopIS, DOA, and ODBASE - OTM Confederated International Conferences , CoopIS, DOA, and ODBASE. Lecture Notes in Computer Science , vol. 2888 , pp. 707 { 724 . Springer ( 2003 )

15. Volz , R. , Staab , S. , Motik , B. : Incrementally maintaining materializations of ontologies stored in logic databases . Journal on Data Semantics II pp. 1 { 34 ( 2005 )

16. Wandelt , S. , Moller, R.: Towards ABox Modularization of Semi-Expressive Description Logics . J. of Applied Ontology 7 ( 2 ), 133 { 167 ( 2012 )