Ontology Materialization by Abstraction Refinement in Horn SHOIF Birte Glimm, Yevgeny Kazakov, and Trung-Kien Tran University of Ulm, Germany, .@uni-ulm.de Abstract. Abstraction refinement is a recently introduced technique which al- lows for reducing materialization of an ontology with a large ABox to material- ization of a smaller (compressed) ‘abstraction’ of this ontology. Although this ap- proach is sound for the very expressive language SROIQ, so far it was proved to be complete only for Horn ALCHOI ontologies. In this paper we propose an extension of this method that is now complete for Horn SHOIF ontolo- gies. Supporting functional roles, in particular, is nontrivial due to the sophis- ticated interaction with nominals and inverse roles. Additionally, we show how to compute not only the concept-materialization but also the role- and equality- materialization. To show completeness we use a tailored set of materialization rules that loosely decouple the ABox from the TBox, which is intrinsically inter- esting as reasoning with nominals in general requires both ABox and TBox. 1 Introduction Description Logics (DLs) are popular languages for knowledge representation and rea- soning. They are the underlying formalism for the standardized Web Ontology Lan- guage (OWL) and its profiles, which are widely used in many application areas. Re- cent years have also seen an increasing interest in ontology-based data access (OBDA), where a TBox with background knowledge, often expressed in a DL language, is used to enrich datasets (ABoxes), which are then accessible via queries. Ontology materi- alization is a reasoning task that computes logical consequences of the dataset w.r.t. the TBox and it is the most important task in some languages, e.g., OWL 2 RL [10]. In other languages, e.g., those that allow existential quantification, materialization is a stepping stone for query answering via rewriting [8]. To make ontology materialization useful in practice, especially for large datasets, scalable materialization is of great importance. Several approaches have been proposed to achieve this goal. The RDFox [11] and WebPIE [13] systems operate on the en- tire dataset and utilize parallel computing to perform a rule-based materialization for OWL 2 RL. Other approaches try to reduce the size of the dataset. Modules or so- called ‘individual islands’ [14] are used for reducing the set of ABox assertions to those that are sufficient for computing the entailed assertions for a given individual. The SHER system [4, 2] improves consistency checking of a large ABox by computing a so-called ‘summary ABox’ in which several original individuals are merged into one. If the resulting ABox is found consistent, then so is the original ABox. If not, then ex- planations [7] are used to pinpoint the contradictory axioms or relax the summary to avoid inconsistency. Similar to SHER, in the abstraction refinement method [5] several individuals of the original ABox can be represented by one individual in a correspond- ing ‘abstract ABox’. In contrast to the summary ABox, the abstract ABox provides an under-approximation rather than the over-approximation of entailments (e.g., if the ab- straction is inconsistent then so is the original ABox but not necessarily vice versa). To ensure completeness of the method, the so-called refinement step is used that re- computes the abstraction based on new (sound) entailments obtained from a previous abstraction. This has the added benefit that not only consistency but also the full mate- rialization of the ABox can be computed at once without (rather expensive) explanation computations or repeated consistency checks. This paper builds upon the abstraction refinement method and presents the following improvements: 1. We extend the approach to guarantee completeness in the presence of transitive and functional roles, thus fully supporting Horn SHOIF ontologies. Reasoning with nominals, inverse roles, and functionality is known to be difficult due to the loss of the tree-model property. 2. We materialize not only concept assertions, but also role and equality assertions. In ALCHOI, role and equality assertions can be computed simply by expanding the role hierarchy and analyzing assertions of nominals. In SHOIF, this is no longer the case. Apart from transitivity, role assertions could result from the consequence that some roles are functional; and interactions of nominals, inverse roles, and func- tionality could lead to a new kind of nominals. In Section 4, we discuss this issue in more detail and provide a solution in Section 5. 3. We present a new set of materialization rules (Section 6), which loosely decouple the ABox from the TBox. Although we use them only for proving completeness of the method (Section 7), these rules can be of interest on its own, e.g., as a basis of an efficient implementation for ABox reasoning. This provides a fresh view of the approach as the completeness proofs are principally different from the previous proofs [5], and the method can potentially be extended to other languages having similar rules. 2 Preliminaries The syntax and semantics of the Description Logic (DL) SHOIF is briefly presented in Table 1. A SHOIF ontology O is Horn [9], if, for every D(a) ∈ O and C v D ∈ O, the concepts C and D satisfy the following grammar definitions: C(i) ::=> | ⊥ | A | o | C1 u C2 | C1 t C2 | ∃R.C (1) D(i) ::=> | ⊥ | A | o | D1 u D2 | ∃R.D | ∀R.D | ¬C (2) Given an ontology O, a role R is functional (in O) if func(R) ∈ O and transitive (in O) if tran(R) ∈ O. (Horn) ALCHOI is the fragment of (Horn) SHOIF in which functionality and transitivity are disallowed. For an ontology O, let v∗H be the reflexive transitive closure of the role hierarchy H = {R v S ∈ O}. If R v∗H S, then we say that R is a sub-role of S and S is a super-role of R; A role R is simple (in O) if it has no transitive sub-roles; if func(R) ∈ O then R must be simple. Table 1. The syntax and semantics of the DL SHOIF Syntax Semantics Concepts: atomic concept A AI ⊆ ∆I nominal o o ⊆ ∆I , ||oI || = 1 I top > ∆I bottom ⊥ ∅ negation ¬C ∆I \ C I conjunction C uD C I ∩ DI disjunction C tD C I ∪ DI existential restriction ∃R.C {d | ∃e ∈ C I : hd, ei ∈ RI } universal restriction ∀R.C {d | hd, ei ∈ RI → e ∈ C I } Axioms: concept inclusion CvD C I ⊆ DI role inclusion RvS RI ⊆ S I role transitivity tran(R) RI ◦ RI ⊆ RI role functionality func(R) hd, ei, hd, e0 i ∈ RI → e = e0 concept assertion C(a) aI ∈ C I role assertion R(a, b) ha , b i ∈ RI I I equality assertion a≈b aI = bI To simplify the presentation, we do not distinguish between axioms R(a, b) and R− (b, a), a ≈ b and b ≈ a, R v S and R− v S − , and tran(R) and tran(R− ). For example, if R(a, b) ∈ A, we assume that R− (b, a) ∈ A. We use con(O), rol(O), ind(O), nom(O) for the sets of atomic concepts, atomic roles, individuals, and nominals occurring in O, respectively. For an ontology O, we say that O is concept-materialized if O |= A(a) implies A(a) ∈ O for each A ∈ con(O) and a ∈ ind(O); O is role-materialized if O |= r(a, b) implies r(a, b) ∈ O for each r ∈ rol(O) and a, b ∈ ind(O); O is equality-materialized if O |= a ≈ b implies a ≈ b ∈ O for each a, b ∈ ind(O); O is (fully) materialized if it is concept-, role-, and equality-materialized. Given an ontology O, the concept-, role-, equality-, and/or (full) materialization of O is the smallest super-set of O that is concept-, role-, equality-, and/or fully materialized respectively. 3 Computing Materialization by Abstraction The main idea of the abstraction refinement method [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 general-purpose reasoner, and transfer the new entailments back to O. The ABox B is usually called the abstraction of the original ABox A (or just the abstract ABox if A is clear from the context), and the individuals in B are called representatives of the original individuals in A. All results in this section apply to any DL with (classical) set-theoretic semantics, e.g., SROIQ [6]. Definition 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 α ∈ B, we have h(α) ∈ A, where h(C(a)) := C(h(a)), h(R(a, b)) := R(h(a), h(b)), and h(a ≈ b) := h(a) ≈ h(b). We say an individual b ∈ ind(B) is a representative of an individual a ∈ ind(A) if there exists a homomorphism h : ind(B) → ind(A) such that h(b) = a. Example 1. Consider the ABoxes A = {A(a), A(b)} and B = {A(u)}. Then the individual u of B is a representative for both individuals a and b since the mappings h1 = {u 7→ a} and h2 = {u 7→ b} are homomorphisms from B to A. The following property of homomorphisms allows transferring entailments from the abstraction to the original ABox. 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(β). Corollary 1. If an individual u ∈ ind(B) is a representative for an individual a ∈ ind(A), then, for every TBox T and concept C, if B ∪ T |= C(u), then A ∪ T |= C(a). According to Corollary 1, in Example 1 one can transfer any newly entailed concept assertion for u to the corresponding assertions for a and b. In fact, in this particular case, all entailed concept assertions for A can be computed this way because there is also a homomorphism from A to B. Example 2 (Example 1 continued). Consider the homomorphism h : ind(A) → ind(B) defined by h = {a 7→ u, b 7→ u}. Then by Lemma 1, for every TBox T and concept C if A ∪ T |= C(a) or A ∪ T |= C(b) then B ∪ T |= C(u). In practice, computing a sufficiently small abstraction B of A such that there are homo- morphisms in both directions is rarely possible, so the set of concept assertions trans- ferred using Corollary 1 is usually incomplete. To ensure completeness, one can employ further refinement steps that recompute the abstraction based on the new information derived. This method was shown to be complete for concept materialization of Horn ALCHOI ontologies [5]. The aim of this paper is to extend this approach to Horn SHOIF. Before we go into further details explaining our extension, we first describe challenges that the new functionality and transitivity axioms pose for ontology materi- alization. 4 Full Materialization for Horn SHOIF It is easy to show using model-theoretic arguments that an ALCHOI ontology O with- out equality assertions entails an equality between individuals a ≈ b iff either a = b or both a and b are instances of some nominal concept o occurring in O. To compute such entailed equality assertions, it is sufficient to compute instances of nominals, which can be accomplished by introducing an axiom o v Ao with a fresh concept Ao for each nominal o and computing instances of Ao by concept materialization. If O contains equality assertions, one needs to additionally perform the transitive symmetric closure of the resulting equality assertions. For role materialization, similarly, one can show that if O |= R(a, b) then either (i) there exists an assertion R0 (a0 , b0 ) ∈ O such that O |= a ≈ a0 , O |= b ≈ b0 , and R0 v∗H R, or (ii) a is an instance of ∃R.o and b is an instance of o for some nominal o, or (iii) a is an instance of o and b is an instance of ∃R− .o for some nominal o. All these conditions can again be checked by introducing fresh concepts and computing the concept materialization. That is, (full) materialization of Horn ALCHOI ontologies can be reduced to con- cept materialization by simple syntactic transformations. The following examples illus- trate that for Horn SHOIF ontologies such reductions do not work. Example 3. Consider the ontology O = A ∪ T with A = {A(a), A(b)} and T = {A v ∃F − .o, func(F )}. Then O |= a ≈ b but neither a nor b are instances of the nominal o. As Example 3 illustrates, equality testing in (Horn) SHOIF becomes less trivial; the main reason is that using a combination of functional roles, inverse roles, and nom- inals one can express entailed nominal concepts such as A in Example 3, which can be interpreted by at most one element. In the following example, we demonstrate how functional roles can also result in some non-trivial entailments of role assertions, even if no equality or nominals are used. Example 4. Consider the ontology O = A ∪ T with A = {A(a), R(a, b)} and T = {A v ∃S.>, R v F, S v F, func(F )}. Then O |= S(a, b) but O 6|= R v S. As can be seen from Examples 3 and 4, the computation of equality- and role- materialization becomes a non-trivial problem for Horn SHOIF ontologies. Fortu- nately, using the following corollary of Lemma 1, one can extend the main idea be- hind concept materialization described in the previous section to equality- and role- materialization. Corollary 2. Let h : ind(B) → ind(A) be a homomorphism between the ABoxes B and A, u, v ∈ ind(B), a = h(u), b = h(v) ∈ ind(A), and T a SROIQ TBox. Then B ∪T |= u ≈ v implies A∪T |= a ≈ b, and B ∪T |= R(u, v) implies A∪T |= R(a, b) for every role R. Unfortunately, the abstract ABoxes that are sufficient to guarantee completeness of concept-materialization are not sufficient to guarantee completeness of equality- and role-materialization as demonstrated in the following example. Example 5. Consider the ABox A and its abstraction B in Example 1. As stated in Example 2, for any TBox T all entailed concept assertions of T ∪ A can be obtained using Corollary 1 for the abstraction B. However, the abstraction B may be insufficient for computing all entailed role or equality assertions using Corollary 2. Indeed, consider T = {A v o}. Then A ∪ T |= a ≈ b, but, clearly, there is no homomorphism h : ind(B) → ind(A) such that h(u) = a and h(u) = b required to derive this assertion using Corollary 2. Similarly, it is possible that A ∪ T |= R(a, b) for some role R, but we are not able to derive this assertion using Corollary 2, for example, for T = {A v ∃T.o, A v ∃T − .o, tran(T ), T v R}. 5 Abstraction Refinement for Horn SHOIF The general algorithm for ontology reasoning using the abstraction refinement method can be summarized as follows: 1. Build a suitable abstraction of the original ontology; 2. Compute the entailments from the abstraction using a reasoner and transfer them to the original ontology using homomorphisms (Lemma 1); 3. Compute the deductive closure of the original ontology using some (light-weight) rules; 4. Repeat from Step 1 until no new entailments can be added to the original ontology. The efficiency and theoretical properties of this method depend on the choices of how the abstraction is computed in Step 1, which entailments are transferred in Step 2, and which rules are used to compute the deductive closure in Step 3. In the following we detail these choices for Horn SHOIF. To compute the abstraction of the original ABox (Step 1), we define types of indi- viduals based on their assertions. Definition 2. Let A be an ABox and a an individual. The concept type of a is a set of concepts τC (a) = {C | C(a) ∈ A}. The role type of a is a set of roles τR (a) = {R | ∃b : R(a, b) ∈ A}. The (combined) type of a is a pair τ (a) = hτC (a), τR (a)i where τC (a) is the concept type of a and τR (a) is the role type of a. Note that we assume w.l.o.g. that, for every individual a, >(a) is included in the on- tology and, therefore, > occurs in every (concept) type. To simplify the presentation, however, we usually omit > in the remainder. Example 6. Let A = {A(a), A(b), R(a, b)}. Then τC (a) = τC (b) = τ1 = {A}, τR (a) = {R}, τR (b) = {R− }, τ (a) = τ2 = h{A}, {R}i, and τ (b) = τ3 = h{A}, {R− }i. The abstract ABox is then constructed by introducing one representative for each type with the respective assertions. S Definition 3. The abstraction of an ABox A is an ABox B = a∈ind(A) (BτC (a) ∪Bτ (a) ), where: – for each concept type τC , BτC = {C(uτC ) | C ∈ τC }, – for each combined type τ = hτC , τR i, Bτ = {C(vτ ) | C ∈ τC } ∪ {R(vτ , wτR ) | R ∈ τR }, where uτC , vτ , and wτR are distinguished abstract individuals for each concept type τC and each combined type τ . Example 7. The abstraction for A in Example 6 is the ABox B = BτC (a) ∪ BτC (b) ∪ Bτ (a) ∪ Bτ (b) , where BτC (a) = BτC (b) = Bτ1 = {A(uτ1 )}, Bτ (a) = Bτ2 = {A(vτ2 ), − R(vτ2 , wτR2 )}, Bτ (b) = Bτ3 = {A(vτ3 ), R− (vτ3 , wτR3 )}. Intuitively, the abstraction is a disjoint union of ABoxes simulating concept and com- bined types. Note that each mapping h : ind(B) → ind(A) such that: h(uτC ) ∈ {a ∈ ind(A) | τC (a) = τC }, (3) h(vτ ) ∈ {a ∈ ind(A) | τ (a) = τ }, (4) h(wτR ) ∈ {b ∈ ind(A) | R(h(vτ ), b) ∈ A}, (5) is a homomorphism from B to A. This allows us to transfer entailments from the ab- straction back to the original ABox using Corollaries 1 and 2. Note that each original individual a in A has at least two representatives in B: uτC (a) that has exactly the same concept assertions as a and vτ (a) which additionally has assertions with the same roles. Two representatives are necessary to solve the problem mentioned in Example 5 for transferring role and equality assertions. Example 8. Consider the ABox A = {A(a), A(b)} and TBox T = {A v o} men- tioned in Example 5. We have τC (a) = τC (b) = τ1 = {A}, and τ (a) = τ (b) = τ2 = h{A}, ∅i. The abstraction of A is defined as B = Bτ1 ∪ Bτ2 with Bτ1 = {A(uτ1 )}, Bτ2 = {A(vτ2 )}. Since B ∪ T |= uτ1 ≈ vτ2 , and h = {uτ1 7→ a, vτ2 7→ b} is a homomorphism from B to A, using Corollary 2 we obtain A ∪ T |= a ≈ b. Next, we detail how entailed assertions are transferred from B to A in Step 2 of the algorithm. To achieve completeness it is not necessary to transfer all of them and we detail which assertions are to be transferred after the definition. Definition 4. Let B be the abstraction of an ABox A (according to Definition 3), and ∆B a set of assertions. The update of A (using ∆B) is the smallest set of assertions ∆A such that: C(vτ (a) ) ∈ ∆B ⇒ C(a) ∈ ∆A, (6) R(a, b) ∈ A, C(wτR(a) ) ∈ ∆B, ⇒ C(b) ∈ ∆A, (7) R(a, b) ∈ A, S(vτ (a) , wτR(a) ) ∈ ∆B ⇒ S(a, b) ∈ ∆A, (8) S(vτ (a) , vτ (a) ) ∈ ∆B ⇒ S(a, a) ∈ ∆A (9) uτC (a) ≈ vτ (b) ∈ ∆B ⇒ a ≈ b ∈ ∆A, (10) R(uτC (a) , vτ (b) ) ∈ ∆B ⇒ R(a, b) ∈ ∆A. (11) Lemma 2. Let B be the abstraction of A, ∆A an update for ∆B, and T a TBox. Then B ∪ T |= ∆B implies A ∪ T |= ∆A. Proof. It is easy to see that for each α ∈ ∆A and β ∈ ∆B in cases (6)–(11), there is a homomorphism h from B to A satisfying conditions (3)–(5) such that h(β) = α. Hence, by Lemma 1, B ∪ T |= β implies A ∪ T |= h(β) = α. t u Let B 0 be the materialization of B ∪ T , then we transfer assertions from ∆B = B 0 \ B according to Definition 4 in Step 2. Next, we compute the (deductive) closure of the ABox A under equality, transitivity, and functionality in Step 3. Definition 5. We say that an ABox A is equality-closed if: a ∈ ind(A) implies a ≈ a ∈ A (12) {a ≈ b, b ≈ c} ⊆ A implies a ≈ c ∈ A, (13) {a ≈ b, A(a)} ⊆ A implies A(b) ∈ A, (14) {a ≈ b, R(a, c)} ⊆ A implies R(b, c) ∈ A, (15) A is closed under the axiom tran(T ) if: {T (a, b), T (b, c)} ⊆ A implies T (a, c) ∈ A. (16) A is closed under the axiom func(F ) if: {F (a, b), F (a, c)} ⊆ A implies b ≈ c ∈ A. (17) The closure of A (w.r.t. a TBox T ) under equality, transitivity, and/or functionality is the smallest super-set of A that is closed under equality, for each tran(T ) ∈ T and/or each func(F ) ∈ T , respectively. Computing the closure of an ABox under equality, functionality, and transitivity is a relatively lightweight operation that does not require using a reasoner. Note that all these assertions must be derived in order to compute the full materialization. S In the previous method [5], the abstraction of an ABox A is defined as B = a∈ind(A) Bτ (a) , and there is no computation of the closure as in Step 3. One can easily check that the previous method is incomplete not only for role and equality materializations but also for concept materialization of Horn SHOIF ontologies, even with the computation of the closure in Step 3. Since Steps 2 and 3 can only extend the original ABox with entailed atomic as- sertions, the procedure is sound, and since the number of such assertions is bounded, the procedure eventually terminates. We next show that the procedure is complete for Horn SHOIF ontologies, that is, the resulting ontology is (fully) materialized when the procedure terminates. 6 A Criterion for Ontology Materialization To prove completeness of the abstraction refinement procedure in the case of Horn SHOIF, we characterize when such ontologies are fully materialized by means of closure of the ABox assertions under certain rules. The rules are similar to the rules for reasoning in Horn SHIQ and Horn SHOIQ [12, 3] in the sense that they derive logical consequences of axioms. Since we are only interested in ABox consequences and not going to use these rules for computing the materialization (but merely for prov- ing completeness of our abstraction refinement algorithm), however, we will not derive TBox axioms explicitly but use their entailments in side conditions of the rules. Recall from the discussion after Example 3, that in SHOIF one can express some non-trivial nominal concepts. To be able to reason about such concepts, we need to extend the language with new axiom types. Definition 6. A concept cardinality restriction is an axiom of the form |C| ≥ n or N |C| = n with C a concept and n ∈ . An interpretation I satisfies |C| ≥ n (|C| = n), written I |= |C| ≥ n (I |= |C| = n), iff |C I | ≥ n (|C I | = n). We also use role conjunctions R u S, interpreted by (R u S)I = RI ∩ S I . The new constructors and axioms are used only in the conditions of rules and not in the ontology. In the following, we denote by N and M conjunctions of atomic concepts and/or nominals and by H conjunctions of roles (possibly with indexes and superscripts). If we write C ∈ N , N ⊆ N 0 , N ( N 0 , we treat N and N 0 as the corresponding sets of conjuncts, where N = > denotes the empty conjunction. Similarly for conjunctions of roles. For a role conjunction H we denote by H − the conjunction of inverses of roles in H. We write N (a) ∈ A if C(a) ∈ A for every C ∈ N . Note that if N (a) ∈ A then A |= |N | ≥ 1. Definition 7. Let A be an ABox. Then N(A) = {|N | ≥ 1 | N (a) ∈ A} is the set of cardinality axioms induced by A. a≈b b≈c a ≈ b R(a, c) a ≈ b A(a) R1≈ : a ∈ ind(A) R2≈ R3≈ R4≈ a≈a a≈c R(b, c) A(b) T (a, b) T (b, c) N (a) R1t : tran(T ) ∈ T R2t : T 0 |= N v ∃(T u T − ).>, tran(T ) ∈ T T (a, c) T (a, a) N (a) M (b) R3t : T 0 |= {N v ∃T.N 0 , M v ∃T − .N 0 , |N 0 | = 1}, tran(T ) ∈ T T (a, b) N (a) N (b) N (a) R(a, b) R|| : T 0 |= |N | = 1 R∀ : T 0 |= N v ∀R.B a≈b B(b) N (a) M (b) R(a, b) R∃ : T 0 |= {N v ∃R.M, |M | = 1} R1v :RvS∈T R(a, b) S(a, b) F (a, b) F (a, c) N (a) R1≤ : func(F ) ∈ T R2v : T 0 |= N v B b≈c B(a) M (a) F (a, b) R2≤ : T 0 |= M v ∃(F u H).N, func(F ) ∈ T H(a, b) N (b) Fig. 1. Materialization rules with T 0 = T ∪ N(A) The materialization rules are presented in Figure 1. These rules are complete for ontology materialization provided the input ontology is in normal form. Definition 8. A Horn SHOIF ontology O is in normal form if (1) for every D(a) ∈ O, D is an atomic concept; (2) for every C v D ∈ O, the concepts C and D satisfy the following grammar: C(i) ::=> | ⊥ | A | o | C1 u C2 | C1 t C2 (18) D(i) ::=> | ⊥ | A | o | ∃R.A | ∀R.A | ¬C (19) and (3) for every C v ∀R.A ∈ O and every transitive sub-role T of R, there exists an atomic concept B that occurs only in {C v ∀T.B, B v ∀T.B, B v A} ⊆ O and not in C or A. Theorem 1. Let O = A ∪ T be a normalized Horn SHOIF ontology and T 0 = T ∪ N(A). Then A is closed under the rules in Figure 1 w.r.t. T iff O is fully materialized. Proof (sketch). The if direction is trivial since all rules derive logical consequences of the axioms in premises and side conditions. For the only if direction, if T 0 is incon- sistent then we can derive all assertions using rules R2v , R∃ , and R|| . If ind(O) = ∅, then Theorem 1 trivially holds. We assume ind(O) 6= ∅ and T 0 is consistent. We then construct a model J of O such that J |= α implies α ∈ A, for every atomic asser- tion α. Then, O |= α implies J |= α, which implies α ∈ A, i.e., O is materialized. Such model J is obtained in two steps: 1) construct an interpretation I satisfying all but transitivity axioms in O such that I |= α implies α ∈ A for every atomic assertion α; 2) obtain J from I by extending the interpretation of non-simple roles to satisfy transitivity axioms. Intuitively, I has a forest-like structure consisting of a graph part and tree parts. The graph part contains domain elements for individuals and concepts that have exactly one instance. The tree parts grow from the graph part to satisfy entailed existential axioms. To construct I, we use a chase-like technique [1] in which new domain elements are introduced to satisfy axioms of the form M v ∃H.N entailed by O such that H and N are maximal (w.r.t M ), i.e., there is no M v ∃H 0 .N 0 entailed by O and H ∪ N ( H 0 ∪N 0 . This guarantees that new domain elements (and their respective assertions) also satisfy universal restrictions and role inclusions. Additionally, a new domain element is introduced only when an axiom cannot be satisfied by the existing domain elements. This ensures all the existential axioms are satisfied while the functionality axioms are not violated. To obtain the model J from I that also satisfies the transitivity axioms in O, we extend the interpretation of non-simple roles to include the transitive closure, i.e., for every transitive role T , (d0 , dn ) is added to T J and to the interpretations of its super- roles if (di−1, di ) ∈ T I , 1 ≤ i ≤ n. This extension makes J satisfy transitivity axioms and the rules R1t –R3t ensure that J |= R(a, b) implies R(a, b) ∈ A for every role R and individuals a, b. Moreover, since only the interpretation of non-simple roles has been extended, it is also possible to show J entails the other axioms in O, i.e. J |= O, and J |= α implies α ∈ A for every atomic assertion α, i.e., we obtain J as required. t u 7 Completeness Once the abstraction refinement procedure terminates, we claim that the input ontology is fully materialized by showing that it is closed under the rules in Figure 1. Lemma 3. Let A ∪ T be an ontology s.t. A is equality-, transitivity-, and functionality- closed, B the abstraction of A, B 0 an ABox s.t. B ⊆ B 0 , N(B 0 ) = N(A) and ∆A ⊆ A with ∆A the update of A using B 0 \ B. Then, B 0 is closed under the rules in Figure 1 w.r.t. T implies that A is also closed under the rules w.r.t. T . Proof. Since N(B 0 ) = N(A), the side condition of each rule holds for B 0 ∪ T iff it holds for A ∪ T . We examine each rule in Figure 1 and show that A is closed under that rule. Clearly, A is closed under R1≈ –R4≈ , R1≤ , R1t . For the other rules, the intuition is: if the premises of a rule R hold for some assertions γ in A, then the premises of R also hold for the corresponding abstract assertions γ 0 in B, and in B 0 consequently. Since B 0 is closed under R, the conclusion κ0 of γ 0 w.r.t. R is already in B 0 . Then, the condition ∆A ⊆ A guarantees that the conclusion κ of γ w.r.t. R is already in A, which implies that A is closed under R. We present one interesting case: R3t ; the remaining cases are analogous. Let {N (a), M (b)} ⊆ A, and the corresponding side condition holds. We have {N (vτ (a) ), M (vτ (b) )} ⊆ B ⊆ B 0 . Since B 0 is closed under R3t , we have T (vτ (a) , vτ (b) ) ∈ B 0 . If vτ (a) = vτ (b) = vτ , i.e. a and b have the same type τ , we are not able to obtain T (a, b) to add to A. That explains why concept types are required. In this case, since {N (uτC ), M (vτ )} ⊆ B ⊆ B0 and B 0 is closed under R3t , we have T (uτC , vτ ) ∈ B 0 , and consequently T (uτC , vτ ) ∈ B 0 \ B. By Definition 4, we have T (a, b) ∈ ∆A ⊆ A. Therefore, A is closed under R3t . t u Using Lemma 3, we show that the procedure is complete. Theorem 2. Let O = A ∪ T be the ontology obtained from the abstraction refinement procedure in Section 5. Then, O is fully materialized. Proof. Let B be the abstraction of A, B 0 ∪ T the materialization of B ∪ T , ∆B = B 0 \ B, and ∆A the update of A using ∆B. For every A(a) ∈ A, we have A(vτ (a) ) ∈ B ⊆ B 0 , which implies N(A) ⊆ N(B 0 )(?). There always exists a homomorphism h from B to B s.t. h(uτC (a) ) = vτ (a) . Therefore, for every A(uτC (a) ) ∈ B 0 , we have A(vτ (a) ) ∈ B 0 . Since the procedure has terminated, i.e. ∆A ⊆ A, for every A(vτ (a) ) ∈ B 0 or A(wτR(a) ) ∈ B 0 we have A(a) ∈ A for some a ∈ ind(A). Hence, we obtain N(B 0 ) ⊆ N(A)(†). From (?) and (†) we have N(A) = N(B 0 ), which allows us to apply Lemma 3. By Theorem 1, B 0 is closed under the rules in Figure 1. Therefore, by Lemma 3, A is closed under those rules. Consequently, by Theorem 1, O is materialized. t u 8 Discussion and Future Work Our next step is to evaluate the procedure in practice. We believe that it is particularly efficient for ontologies with large ABoxes. We have demonstrated in our previous work [5] that for such ontologies, the abstractions are often significantly smaller than the original ones. Given the (intentionally) close similarity with the previous procedure, it is reasonable to assume that the proposed extension would yield similar reductions. We also plan to extend the approach to allow more constructors in the Horn fragments. A possibility to handle qualified number restrictions is to extend the combined type of individuals by considering also concept assertions of their predecessors/successors. Materialization of concept assertions in the presence of role chains could be done us- ing well-known encoding techniques but computing role assertions, especially for non- simple roles, might be more involved. Handing non-Horn ontologies requires major changes in the current approach as the abstraction can communicate only deterministic entailments; this will be the subject of future work. References 1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995) 2. Dolby, J., Fokoue, A., Kalyanpur, A., Schonberg, E., Srinivas, K.: Scalable highly expressive reasoner (SHER). J. of Web Semantics 7(4), 357–361 (2009) 3. Eiter, T., Ortiz, M., Simkus, M., Tran, T.K., Xiao, G.: Query rewriting for Horn-SHIQ plus rules. In: Proc. of the 26th National Conf. on Artificial Intelligence (AAAI 2012). AAAI Press (2012) 4. Fokoue, A., Kershenbaum, A., Ma, L., Schonberg, E., Srinivas, K.: The summary ABox: Cutting ontologies down to size. In: Proc. of the 5th Int. Semantic Web Conference (ISWC 2006). LNCS, vol. 4273, pp. 343–356. Springer (2006) 5. Glimm, B., Kazakov, Y., Liebig, T., Tran, T., Vialard, V.: Abstraction refinement for ontology materialization. In: Proc. of the 13th Int. Semantic Web Conference (ISWC 2014). pp. 180– 195. Springer (2014) 6. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc. of 10th Inter- national Conference on Principles of Knowledge Representation and Reasoning (KR 2006). pp. 57–67 (2006) 7. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Proc. of the 6th Int. Semantic Web Conf. (ISWC 2007). LNCS, vol. 4825, pp. 267–280. Springer (2007) 8. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The combined approach to ontology-based data access. In: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011. pp. 2656–2661 (2011) 9. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of horn description logics. ACM Trans. Comput. Log. 14(1), 2 (2013) 10. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C. (eds.): OWL 2 Web Ontology Language: Profiles (Second Edition). W3C Recommendation (2012), available at http://www.w3.org/TR/owl2-profiles/ 11. Motik, B., Nenov, Y., Piro, R., Horrocks, I., Olteanu, D.: Parallel materialisation of datalog programs in centralised, main-memory RDF systems. In: Proc. of the Twenty-Eighth AAAI Conference on Artificial Intelligence. pp. 129–137 (2014) 12. Ortiz, M., Rudolph, S., Simkus, M.: Worst-case optimal reasoning for the horn-dl fragments of OWL 1 and 2. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010 (2010) 13. Urbani, J., Kotoulas, S., Maassen, J., van Harmelen, F., Bal, H.E.: WebPIE: A web-scale parallel inference engine using MapReduce. J. Web Semantics 10, 59–75 (2012) 14. Wandelt, S., Möller, R.: Towards ABox modularization of semi-expressive description log- ics. J. of Applied Ontology 7(2), 133–167 (2012)