=Paper=
{{Paper
|id=Vol-1577/invited_paper_1
|storemode=property
|title=Ontology Materialization by Abstraction Refinement in Horn SHOIF
|pdfUrl=https://ceur-ws.org/Vol-1577/invited_paper_1.pdf
|volume=Vol-1577
|authors=Birte Glimm,Yevgeny Kazakov,Trung-Kien Tran
|dblpUrl=https://dblp.org/rec/conf/dlog/GlimmKT16
}}
==Ontology Materialization by Abstraction Refinement in Horn SHOIF==
https://ceur-ws.org/Vol-1577/invited_paper_1.pdf
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)