Abstraction refinement is a recently introduced technique which allows for reducing materialization of an ontology with a large ABox to materialization of a smaller (compressed) 'abstraction' of this ontology. Although this approach 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 ontologies. Supporting functional roles, in particular, is nontrivial due to the sophisticated interaction with nominals and inverse roles. Additionally, we show how to compute not only the concept-materialization but also the role- and equalitymaterialization. To show completeness we use a tailored set of materialization rules that loosely decouple the ABox from the TBox, which is intrinsically interesting as reasoning with nominals in general requires both ABox and TBox.
Description Logics (DLs) are popular languages for knowledge representation and
reasoning. They are the underlying formalism for the standardized Web Ontology
Language (OWL) and its profiles, which are widely used in many application areas.
Recent 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
materialization 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 [
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 [
The syntax and semantics of the Description Logic (DL) SHOIF is briefly presented
in Table 1. A SHOIF ontology O is Horn [
C(i) ::=> j ? j A j o j C1 u C2 j C1 t C2 j 9R:C D(i) ::=> j ? j A j o j D1 u D2 j 9R:D j 8R:D j :C (1) (2) Given an ontology O, a role R is functional (in O) if func(R) 2 O and transitive (in O) if tran(R) 2 O. (Horn) ALCHOI is the fragment of (Horn) SHOIF in which functionality and transitivity are disallowed. For an ontology O, let vH be the reflexive transitive closure of the role hierarchy H = fR v S 2 Og. If R vH 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) 2 O then R must be simple.
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) 2 A, we assume that R (b; a) 2 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 j= A(a) implies A(a) 2 O for each A 2 con(O) and a 2 ind(O); O is role-materialized if O j= r(a; b) implies r(a; b) 2 O for each r 2 rol(O) and a; b 2 ind(O); O is equality-materialized if O j= a b implies a b 2 O for each a; b 2 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
The main idea of the abstraction refinement method [
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 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.
Example 1. Consider the ABoxes A = fA(a); A(b)g and B = fA(u)g. Then the individual u of B is a representative for both individuals a and b since the mappings h1 = fu 7! ag and h2 = fu 7! bg are homomorphisms from B to A.
The following property of homomorphisms allows transferring entailments from the abstraction to the original ABox.
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.
defined by h = fa 7! u; b 7! ug. Then by Lemma 1, for every TBox T and concept C if A [ T j= C(a) or A [ T j= C(b) then B [ T j= C(u).
In practice, computing a sufficiently small abstraction B of A such that there are
homomorphisms in both directions is rarely possible, so the set of concept assertions
transferred 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 [
It is easy to show using model-theoretic arguments that an ALCHOI ontology O without 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 j= R(a; b) then either (i) there exists an assertion R0(a0; b0) 2 O such that O j= a a0, O j= b b0, and R0 vH R, or (ii) a is an instance of 9R: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 9R :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 concept materialization by simple syntactic transformations. The following examples illustrate that for Horn SHOIF ontologies such reductions do not work.
Example 3. Consider the ontology O = A [ T with A = fA(a); A(b)g and T = fA v 9F :o; func(F )g. Then O j= 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 nominals 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 = fA(a); R(a; b)g and T = fA v 9S:>; R v F; S v F; func(F )g. Then O j= S(a; b) but O 6j= R v S.
As can be seen from Examples 3 and 4, the computation of equality- and rolematerialization becomes a non-trivial problem for Horn SHOIF ontologies. Fortunately, using the following corollary of Lemma 1, one can extend the main idea behind concept materialization described in the previous section to equality- and rolematerialization.
and A, u; v 2 ind(B), a = h(u); b = h(v) 2 ind(A), and T a SROIQ TBox. Then B [T j= u v implies A[T j= a b, and B [T j= R(u; v) implies A[T j= 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 = fA v og. Then A [ T j= 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 j= R(a; b) for some role R, but we are not able to derive this assertion using Corollary 2, for example, for T = fA v 9T:o; A v 9T :o; tran(T ); T v Rg.
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 individuals based on their assertions.
of concepts C (a) = fC j C(a) 2 Ag. The role type of a is a set of roles R(a) = fR j 9b : R(a; b) 2 Ag. 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 ontology and, therefore, > occurs in every (concept) type. To simplify the presentation, however, we usually omit > in the remainder.
Example 6. Let A = fA(a); A(b); R(a; b)g. Then C (a) = C (b) = R(a) = fRg, R(b) = fR g, (a) = 2 = hfAg; fRgi, and (b) = fR gi. 1 = fAg, 3 = hfAg;
The abstract ABox is then constructed by introducing one representative for each type with the respective assertions.
Definition 3. The abstraction of an ABox A is an ABox B = Sa2ind(A)(B C(a)[B (a)), where: – for each concept type C , B C = fC(u C ) j C 2 C g, – for each combined type = h C ; Ri, B = fC(v ) j C 2 C g [ fR(v ; wR) j
R 2 Rg, where u C , v , and wR 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 = fA(u 1 )g, B (a) = B 2 = fA(v 2 ); R(v 2 ; wR2 )g, B (b) = B 3 = fA(v 3 ); R (v 3 ; wR3 )g.
h(u C ) 2 fa 2 ind(A) j C (a) = C g; 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. This allows us to transfer entailments from the abstraction 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 = fA(a); A(b)g and TBox T = fA v og mentioned in Example 5. We have C (a) = C (b) = 1 = fAg, and (a) = (b) = 2 = hfAg; ;i. The abstraction of A is defined as B = B 1 [ B 2 with B 1 = fA(u 1 )g, B 2 = fA(v 2 )g. Since B [ T j= u 1 v 2 , and h = fu 1 7! a; v 2 7! bg is a homomorphism from B to A, using Corollary 2 we obtain A [ T j= 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.
Intuitively, the abstraction is a disjoint union of ABoxes simulating concept and combined types. Note that each mapping h : ind(B) ! ind(A) such that: (3) (4) (5) (6) (7) (8) (9) (10) (11)
C(v (a)) 2
R(a; b) 2 A; C(wR(a)) 2 R(a; b) 2 A; S(v (a); wR(a)) 2
S(v (a); v (a)) 2 u C(a)
v (b) 2 R(u C(a); v (b)) 2
B B; B B B B ) ) ) ) ) )
C(a) 2
C(b) 2 S(a; b) 2 S(a; a) 2 a
b 2 R(a; b) 2
A; A; A; A A; A:
B [ T j= B implies A [ T j= A.
Proof. It is easy to see that for each 2 A and 2 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 j= implies A [ T j= h( ) = . tu Let B0 be the materialization of B [ T , then we transfer assertions from B = B0 n 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. (12) (13) (14) (15) (16) (17) Definition 5. We say that an ABox A is equality-closed if: fa fa fa b; b cg b; A(a)g b; R(a; c)g a 2 ind(A) implies a
a 2 A
A is closed under the axiom tran(T ) if: A is closed under the axiom func(F ) if: fT (a; b); T (b; c)g
fF (a; b); F (a; c)g
c 2 A: 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 ) 2 T and/or each func(F ) 2 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. In the
previous method [
Since Steps 2 and 3 can only extend the original ABox with entailed atomic assertions, 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
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 [
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 jCj n or jCj = n with C a concept and n 2 N. An interpretation I satisfies jCj n (jCj = n), written I j= jCj n (I j= jCj = n), iff jCI j n (jCI j = n).
We also use role conjunctions R u S, interpreted by (R u S)I = RI \ SI . 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 2 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) 2 A if C(a) 2 A for every C 2 N . Note that if N (a) 2 A then A j= jN j 1.
Definition 7. Let A be an ABox. Then N(A) = fjN j cardinality axioms induced by A. 1 j N (a) 2 Ag is the set of R1 a
a : a 2 ind(A) 1 T (a; b) T (b; c) Rt T (a; c)
R9 Rt Rjj 3 N (a) M (b)
T (a; b) N (a) N (b)
a b N (a) M (b)
R(a; b)
R2 a b b a c c
R3 a b R(a; c) R(b; c)
R4 a b A(a) A(b) : tran(T ) 2 T
2 N (a)
Rt T (a; a) : T 0 j= N v 9(T u T ):>; tran(T ) 2 T R 1 F (a; b) F (a; c) b c
: func(F ) 2 T : T 0 j= fN v 9T:N 0; M v 9T :N 0; jN 0j = 1g; tran(T ) 2 T : T 0 j= jN j = 1
R8
N (a) R(a; b)
B(b)
: T 0 j= N v 8R:B : T 0 j= fN v 9R:M; jM j = 1g
R1v RS((aa;; bb)) : R v S 2 T
R2v NB((aa)) : T 0 j= N v B R 2 M (a) F (a; b)
H(a; b) N (b) : T 0 j= M v 9(F u H):N; func(F ) 2 T
the following grammar:
C(i) ::=> j ? j A j o j C1 u C2 j C1 t C2 D(i) ::=> j ? j A j o j 9R:A j 8R:A j :C and (3) for every C v 8R:A 2 O and every transitive sub-role T of R, there exists an atomic concept B that occurs only in fC v 8T :B; B v 8T :B; B v Ag O and not in C or A.
Theorem 1. Let O = A [ T be a normalized Horn SHOIF ontology and T 0 = T [
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 inconsistent then we can derive all assertions using rules R2v, R9, and Rjj. 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 j= implies 2 A, for every atomic assertion . Then, O j= implies J j= , which implies 2 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 j= implies 2 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 [
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 superroles if (di 1;di) 2 T I ; 1 i n. This extension makes J satisfy transitivity axioms and the rules Rt1–Rt3 ensure that J j= R(a; b) implies R(a; b) 2 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 j= O, and J j= implies 2 A for every atomic assertion , i.e., we obtain J as required. tu 7
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.
Proof. Since N(B0) = N(A), the side condition of each rule holds for B0 [ 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 ; Rt1. 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 B0 consequently. Since B0 is closed under R, the conclusion 0 of 0 w.r.t. R is already in B0. 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: Rt3; the remaining cases are analogous. Let fN (a); M (b)g A, and the corresponding side condition holds. We have fN (v (a)); M (v (b))g B B0. Since B0 is closed under Rt3, we have T (v (a); v (b)) 2 B0. 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 fN (u C ); M (v )g B B0 and B0 is closed under Rt3, we have T (u C ; v ) 2 B0, and consequently T (u C ; v ) 2 B0 n B. By Definition 4, we have T (a; b) 2 A A. Therefore, A is closed under Rt3. tu 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, B0 [ T the materialization of B [ T , B = B0 n B, and A the update of A using B. For every A(a) 2 A, we have A(v (a)) 2 B B0, which implies N(A) N(B0)(?). 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)) 2 B0, we have A(v (a)) 2 B0. Since the procedure has terminated, i.e. A A, for every A(v (a)) 2 B0 or A(wR(a)) 2 B0 we have A(a) 2 A for some a 2 ind(A). Hence, we obtain N(B0) N(A)(y). From (?) and (y) we have N(A) = N(B0), which allows us to apply Lemma 3.
By Theorem 1, B0 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. tu 8
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
[