=Paper=
{{Paper
|id=Vol-2211/paper-11
|storemode=property
|title=Complete Approximations of Horn DL Ontologies
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-11.pdf
|volume=Vol-2211
|authors=Anneke Bötcher,Carsten Lutz,Frank Wolter
|dblpUrl=https://dblp.org/rec/conf/dlog/BotcherLW18
}}
==Complete Approximations of Horn DL Ontologies==
https://ceur-ws.org/Vol-2211/paper-11.pdf
Complete Approximation of Horn DL Ontologies
Anneke Bötcher1 , Carsten Lutz1 , and Frank Wolter2
1
University of Bremen, Germany
anneke@uni-bremen.de clu@uni-bremen.de
2
University of Liverpool, United Kingdom
wolter@liverpool.ac.uk
Abstract. We study the approximation of expressive Horn DL ontolo-
gies in less expressive Horn DLs, with completeness guarantees. Cases of
interest include Horn-SRIF -to-ELR⊥ , Horn-SHIF -to-ELH⊥ , and oth-
ers. Since finite approximations almost never exist, we carefully map out
the structure of infinite approximations. This provides a solid theoret-
ical foundation for constructing incomplete approximations in practice
in a controlled way. Technically, we exibit a connection to the axiomati-
zation of quasi-equations valid in classes of semilattices with operators
and additionally develop a direct proof strategy based on the chase and
on homomorphisms that allows us to also deal with approximations of
bounded role depth.
1 Introduction
There is a large number of description logics that vary considerably regarding
their expressive power and computational properties [2] and despite prominent
standardization efforts, many different DLs continue to be used in ontologies
from practical applications.3 As a result, it is often necessary to convert an
ontology formulated in some DL L into another DL L0 , a particularly important
case being that L0 is a fragment of L—if it is not, then one could use the fragment
L ∩ L0 of L in place of L0 . For example, this happens in ontology import when
an engineer who designs an ontology formulated in L0 wants to reuse content
from an existing ontology formulated in L. The problem that emerges from this
is ontology approximation, a form of knowledge compilation [27, 11].
In this paper, we are interested in approximating an ontology OE formulated
in an expressive description logic L by an ontology OL formulated in a fragment
L0 of L. We aim to construct OL so that it preserves all information from OE
expressible in L0 , called a greatest lower bound in knowledge compilation [27].
Formally, for every L0 concept inclusion C v D that is formulated in the signa-
ture Σ of OE , we require that OE |= C v D if and only if OL |= C v D, and
likewise for role inclusions and any other type of ontology statement supported
by L0 . We say that OL is sound as an approximation if it satisfies the “if” part
of this property and complete if it satisfies the “only if” part. It is equivalent to
3
See, for example, the BioPortal repository at https://bioportal.bioontology.
org/.
demand that OE |= OL and for every L ontology O in signature Σ, OE |= O
implies OL |= O. We consider both the case where OL is formulated in Σ (non-
projective approximation) and the case where additional symbols are admitted
(projective approximation).
In practice, approximations are often constructed in an ad hoc way that
is sound but not complete. For example, it is common to simply replace all
subconcepts of OE that use a constructor which is not available in L0 with top
or with bottom. In fact, full completeness is typically not attainable as it brings
about infinite ontologies even in simple cases. For example, consider the ELI
ontology OE = {∃hasSupervisor− .> v Manager} which contains only a single
range restriction. There is no finite EL approximation OL since for all n ≥ 1,
OE entails the EL concept inclusion
∃hasSupervisorn .> v ∃hasSupervisor.(Manager u ∃hasSupervisorn−1 .>).
Also for the ELF ontology OE = {func(hasSupervisor), func(reportsTo)},
there is no finite EL approximation OL since for all n, m ≥ 1, OE entails the EL
concept inclusion4
∃reportsTo.∃hasSupervisorn .> u ∃reportsTom .> v
∃reportsTo.(∃hasSupervisorn .> u ∃reportsTom−1 .>).
Nevertheless, ad hoc ways to construct approximations can be a problematic
choice since it is often only poorly understood which information has been given
up. This is particularly worrying in ontology import where one would like to
construct an as meaningful approximation as possible, rather than just some
approximation. Our aim is to address this problem by carefully studying the
structure of infinite approximations. As the expressive DL L, we consider Horn-
SRIF and fragments thereof. As the fragment L0 , we consider ELR⊥ and corre-
sponding fragments thereof, where ELR⊥ denotes the extension of ELH⊥ with
role inclusions of the form r1 ◦· · ·◦rn v r. For example, we study Horn-SRIF-to-
ELR⊥ approximation, Horn-SHIF-to-ELH⊥ , ELI-to-EL, ELF-to-EL, and so
on. Subsumption is ExpTime-complete in all mentioned source DLs and PTime-
complete in all mentioned target DLs [1, 20]. We thus support ontology designers
who build an ontology in a tractable DL and want to import in a well-understood
way from an existing ontology formulated in a more costly DL, without compro-
mising tractability.
We provide the following results. In Section 3, we present non-projective
approximations for the ELRI F⊥ -to-ELR⊥ case and several subcases such as
ELHI⊥ -to-ELH⊥ . Here, superscript I means that inverse roles are admitted only
in role hierarchies of the form r v s− but not in concept inclusions and more com-
plex role inclusions, which is actually a very common way to use inverse roles in
practice. The presented approximation requires that OE is inverse closed, mean-
ing that for every role name r in OE , there is a role name r̂ that is defined via
4
A single functionality assertion would also do, but it is convenient for the example
to have two role names in the signature of OE .
role hierarchies to be the inverse of r. This also yields projective approximations
for the case where inverse closedness is not assumed and for the Horn-SRIF-to-
ELR⊥ case through a well-known normalization procedure. The completeness
proof is based on a novel connection between ontology approximation and the
axiomatizations of quasi-equations valid in classes of semilattices with opera-
tors (SLOs); note that SLOs have been used before to obtain algorithms for
subsumption in extensions of EL [28, 29].
In Section 4, we construct non-projective ELHI F⊥ -to-ELH⊥ approxima-
tions under the mild assumption that whenever OE |= r v s− , then neither
func(s) ∈ OE nor func(s− ) ∈ OE . This again encompasses relevant subcases
such as ELHF-to-ELH, without any syntactic assumptions. The main difference
to Section 3 is how completeness is established. Here, we find a chase procedure
for L ontologies that is inspired by and closely linked to the proposed approx-
imation scheme, prove that it is complete for consequences formulated in L0 ,
and then show that consequences computed by the chase can also be derived
using OL . In contrast to the approach based on SLOs, this enables us to also
prove that finite approxmations always exist if we restrict the role depth of con-
cepts in consequences to be bounded by a constant; we speak of depth bounded
approximations.
We then proceed to study ELI⊥ -to-EL⊥ approximations in Section 5. In
contrast to the cases considered before, where both L and L0 are based on the
concept language EL⊥ , here the concept language of L (which is ELI ⊥ ) different
from the one of L0 (which is EL⊥ ). We present non-projective approximations for
unrestricted ontologies OE and for ontologies OE which are in the well-known
normal form for ELI⊥ ontologies that avoids syntactic nesting of concepts. The
two approximation schemes are remarkably different, the latter arguably being
more informative than the former.
In Section 6, we complement the proposed infinite approximations by showing
that finite approximations do not exist even in simple cases and that depth
bounded approximations are non-elementary in size even in simple cases.
Proof details are available in the appendix of the long version, available at
http://www.informatik.uni-bremen.de/tdki/research/papers.html
Related Work. Approximation in a DL context was first studied in [27]
where FL concepts are approximated by FL− concepts and in [9] where ALC
concepts are approximated by ALE concepts. In both cases, the approximation
always exists, but ontologies are not considered. An incomplete approach to
approximating SHOIN ontologies in DL-LiteF is presented in [24] and com-
plete (projective) approximations of SROIQ ontologies in DL-LiteA are given
in [7]. Such approximations are guaranteed to exist due to the limited expressive
power of DL-LiteA . Approximation of Horn-ALCHIQ ontologies by DL-LiteR
ontologies in an OBDA context was considered in [8], exploiting the mapping
formalism available in OBDA. In [22], approximation of ELU ontologies in terms
of EL ontologies is studied, the main result being that it is ExpTime-hard and
in 2ExpTime to decide a finite complete approximation exists. An incomplete
approach to approximating SROIQ ontologies in EL++ is in [25]. There are also
approaches towards efficient DL reasoning that involve computing approxima-
tions, which may be greatest lower bounds and/or least upper bounds. Such ap-
proximations are intentionally incomplete in order to not compromise efficiency,
see for example [26, 14, 10]. Related to approximation is the problem whether a
given L ontology can be equivalently rewritten into the fragment L0 of L, either
non-projectively [21] or projectively [19]; note that this asks whether we have to
approximate at all. There are also various approaches to OBDA with expressive
DLs that involve forms of approximation such as [30, 31, 12, 15].
2 Preliminaries
Let NC and NR be disjoint and countably infinite sets of concept and role names.
A role is a role name r or an inverse role r− , with r a role name. A Horn-SRIF
concept inclusion (CI) is of the form L v R, where L and R are concepts defined
by the syntax rules
R, R0 ::= > | ⊥ | A | ¬A | R u R0 | ¬L t R | ∃ρ.R | ∀ρ.R
L, L0 ::= > | ⊥ | A | L u L0 | L t L0 | ∃ρ.L
with A ranging over concept names and ρ over roles. The depth of a concept
R or L is the nesting depth of existential and universal restrictions in it. For
example, the depth of ∃r.B u ∃r.∃s.A is two. A Horn-SRIF ontology O is a
set of Horn-SRIF CIs, functionality assertions func(ρ), transitivity assertions
trans(ρ), and role inclusions (RIs) ρ1 ◦ · · · ◦ ρn v ρ. A role inclusion of the special
form ρ1 v ρ2 is a role hierarchy (RH). We adopt the standard assumption that
for any RI ρ1 ◦ · · · ◦ ρn v ρ with n ≥ 2, we neither have O |= func(ρ) nor
O |= func(ρ− ). Ontologies used in practice of course have to be finite. In this
paper, though, we shall frequently consider also infinite ontologies.
An ELRIF ⊥ ontology is a Horn-SRIF ontology in which both the left- and
right-hand sides of CIs are ELI ⊥ concepts, defined as usual, and that does not
contain transitivity assertions. If O uses neither inverse roles nor functionality
assertions, then it is an ELR⊥ ontology. We assume w.l.o.g. that, in ELRIF ⊥
and below, the ⊥ concept occurs only in the form C v ⊥. We assume that
other standard DL names such as Horn-SHIF are understood. It should also
be clear what we mean by saying that an ontology language is based on a con-
cept language. For example, the ontology language ELHIF ⊥ is based on the
concept language ELI ⊥ . We also use a non-standard naming scheme, namely
that HI indicates the presence of role hierarchies and of inverse roles in role
hierarchies, but not in concept inclusions. RI is similar, but additionally admits
role inclusions while still restricting the use of inverse roles to role hierarchies.
For the semantics and more details on the relevant DLs, we refer to [2].
A signature Σ is a set of concept and role names. When speaking of EL(Σ)
concepts, we mean EL concepts that only use concept and role names from Σ,
and likewise for other concept languages. We use sig(O) to denote the set of
concept and role names used in ontology O.
Definition 1. Let OE be a Horn-SRIF ontology with sig(OE ) = Σ and let L
be a fragment of Horn-SRIF based on the concept language C. A (potentially
infinite) L ontology OL is an L approximation of OE if the following conditions
are satisfied:
1. OE |= C v D iff OL |= C v D for all C(Σ) concepts C, D;
2. if α is a role inclusion, role hierarchy, or functionality assertion that falls
within L and uses only symbols from Σ, then OE |= α iff OL |= α.
We call OL a non-projective EL approximation if sig(OL ) ⊆ Σ and projective
otherwise.
N
For ` ∈ ∪{ω}, (non-projective and projective) `-bounded L approximations
are defined analogously, except that only concepts C, D of depth bounded by ` are
considered in Point 1.
The term ω-bounded approximation, which is in fact the same as an unbounded
approximation, is used only for uniformity. In Definition 1 and throughout the
paper, we use OE to denote ontologies formulated in an E xpressive DL and OL
to denote ontologies formulated in a Lightweight (in the sense of ‘inexpressive’)
DL. Note that, trivially, infinite (non-projective and projective) approximations
always exist: simply take as OL the set of all relevant inclusions and assertions
that are entailed by OE . Definition 1 speaks about Horn-SRIF ontologies OE
because this is the most expressive DL considered in this paper. In general, we
speak about LS -to-LT approximation, LS a DL and LT a fragment thereof, to
denote the task of approximating an LS ontology in LT . We call LS the source
DL and LT the target DL. One can show that there are ELI ontologies OE
that have a finite projective EL approximation, but no finite non-projective EL
approximation. Details are in the appendix. An alternative definition of approx-
imations is obained by considering in Point 1 any C concept for C and D rather
than only concepts in signature Σ. We choose not to do that because then even
in the 1-bounded case, finite approximations do not necessarily exist.
Example 1. Consider the ELI ontology OE = {∃r− .A v B}. We have as a
consequence Au∃r.X v ∃r.(B uX) for each of the infinitely many concept names
X ∈ NC . Thus, every (projective or non-projective) 1-bounded EL approximation
of OE must be infinite under the alternative definition of approximation.
We now make some basic observations regarding approximations. The proof is
straightforward.
Lemma 1. Let OE be a Horn-SRIF ontology with sig(OE ) = Σ and L a frag-
ment of Horn-SRIF. Then
1. an L ontology OL is an L approximation of OE iff OE |= OL and for every
L
S ontology O with OE |= O and sig(O) ⊆ Σ, OL |= O;
2. i≥0 O` is an L approximation of OE if for all ` ≥ 0, O` is an `-bounded
L approximation of OE ; the same is true for projective L approximations
provided that sig(O` ) ∩ sig(O`0 ) ⊆ Σ when ` 6= `0 .
Point 1 may be viewed as an alternative definition of (non-projective) approx-
imations. Point 2 is important because it allows us to concentrate on bounded
approximations in proofs and to then obtain results for unbounded approxima-
tions as a byproduct. The following is well-known, see for example [5].
Lemma 2. Given a Horn-SRIF ontology OE with sig(O) = Σ, one can con-
0 0
struct in polynomial time an ELRIF ⊥ ontology OE with sig(OE ) ⊇ Σ that
entails the same Horn-SRIF(Σ) concept inclusions, role inclusions, and func-
tionality assertions.
0
Note that the construction of the ontology OE from Lemma 2 requires the
introduction of fresh concept names. Still, every `-bounded L approximation of
O0 is a projective `-bounded L approximation of O. From now on, we work with
ELRIF ⊥ ontologies rather than with Horn-SRIF and thus obtain projective
approximations also for the latter. Studying non-projective approximations of
Horn-SRIF ontologies is outside the scope of this paper.
3 Unbounded ELRIF⊥ -to-ELR⊥ Approximation
We provide (unbounded) approximations of ELRIF⊥ ontologies in ELR⊥ . We
assume throughout this section that ELRIF⊥ ontologies OE are inverse closed,
that is, for every role name r used in OE , there is a role name, which we denote
r̂, such that r v r̂− and r̂ v r− are in OE . Thus, r̂ is an explicit name for
the inverse of r. We can clearly additionally assume w.l.o.g. that there are no
other occurrences of inverse roles in OE , which we shall always do. In other
words, it suffices to consider inverse closed ELRI F⊥ ontologies in place of inverse
closed ELRIF⊥ ontologies. We obtain non-projective approximations under this
assumption, which clearly also yields projective approximations in the general
case. The following theorem summarizes the results from this section.
Theorem 1. Let OE be an inverse closed ELRI F⊥ ontology and Σ = sig(OE ).
Define OL to be the ELR⊥ ontology that contains for all EL(Σ) concepts C, D
and role names r, s ∈ Σ:
1. all CIs in OE ;
2. r v s if OE |= r v s;
3. r1 ◦ · · · ◦ rn v r, r̂n ◦ · · · ◦ r̂1 v r̂ if r1 ◦ · · · ◦ rn v r ∈ OE with n ≥ 2;
4. C u ∃r.D v ∃r.(D u ∃r̂.C);
5. ∃r.C u ∃r.D v ∃r.(C u D) if func(r) ∈ OE ;
6. ∃r.∃r̂.C v C if func(r̂) ∈ OE .
Then OL is an ELR⊥ approximation of OE .
Note that Points 1 to 3 essentially take over the part of OE that is expressible
in ELR⊥ , Point 4 aims at capturing the consequences of inverse roles, Point 5 at
functional roles, and Point 6 at the interaction between functional roles and in-
verse roles. Points 4 to 6 all introduce infinitely many CIs. The following example
shows that Point 6 cannot be omitted.
Example 2. Consider OE = {func(r̂), r v r̂− , r̂ v r− , A v A} Then OE |=
0 0
∃r.∃r̂.A v A but OL 6|= ∃r.∃r̂.A v A for the ontology OL obtained from OL
by omitting the CIs of Point 6. To show this, consider the interpretation I with
domain {0, 1, . . .} and
rI = {(2n, 2n + 1) | n ≥ 0}, r̂I = {(2n + 1, 2n + 2) | n ≥ 0}, AI = {2n | n ≥ 1}
0
Then I is a model of OL but 0 ∈ (∃r.∃r̂.A)I \ AI .
It should be obvious how Point 5 captures the ELF-to-EL example from the
introduction. Point 4 captures the natural variation of the ELI-to-EL example
from the introduction obtained by converting the ELI ontology OE used there
into an inverse closed ELHI ontology, as follows.
Example 3. Let OE = {∃supervises.> v Manager, hasSuper v supervises− ,
supervises− v hasSuper}. Point 4 yields
∃hasSupern .> v ∃hasSuper.(∃supervises.> u ∃hasSupern−1 .>)
which together with ∃supervises.> v Manager ∈ OL yields the desired
∃hasSupern .> v ∃hasSuper.(Manager u ∃hasSupern−1 .>).
Theorem 1 also settles several natural subcases of (projective) ELRI F⊥ -to-
ELR⊥ approximation such as ELHI -to-ELH. For subcases where the source
DL does not contain inverse roles such as ELF-to-EL, the concept inclusions in
Point 4 are still present in the approximation as we still assume inverse closed-
ness. This could also be avoided, as in the results presented in the subsequent
section. We find it remarkable that the construction of OL is based almost en-
tirely on a purely syntactic analysis of OE , rather than involving reasoning.
Reasoning is only required to derive the role hierarchies to be included in OL , in
Point 2 of Theorem 1. Although we do not consider this aspect very important,
we mention that this problem is ExpTime-complete when OE is formulated in
ELRI F⊥ and in PTime for many of the captures subcases such as when OE is
formulated in ELRI .
It is straightforward to show that the ontology OL from Theorem 1 is sound
as an approximation. To prove completeness, we establish a novel connection be-
tween EL⊥ approximations and axiomatizations of the quasi-equations that are
valid in classes of semilattices with operators (SLOs) [16, 29, 17]. Roughly speak-
ing, an approximation is obtained from such an axiomatization by instantiating
its equations, which correspond (in the sense of modal correspondence theory)
to the role inclusions and hierarchies in the original ontology, with arbitrary EL
concepts. A detailed presentation is provided in the appendix.
4 Depth-Bounded ELHI F⊥ -to-ELH⊥ Approximation
We pursue an alternative approach to proving that an approximation is com-
plete, based on a suitable version of the chase. This allows us to also treat the
case of depth bounded approximations. Moreover, approximations obtained in
this section are non-projective and the assumption of ontologies being inverse
closed is not needed. We consider ELHI F⊥ -to-ELH⊥ approximation and sub-
cases thereof. An extension to role inclusions should be possible, but is left as
future work.
We assume w.l.o.g. that role hierarchies only take the two forms r v s and
r v s− . We further assume the following syntactic restriction:
(♥) OE |= r v s− implies that neither func(s) ∈ OE nor func(s− ) ∈ OE .
This assumption is not without loss of generality, it serves to eliminate a subtle
interaction between inverse roles, functional roles, and role hierarchies. While
this interaction is captured implicitly and gracefully by the unbounded approxi-
mation scheme given in the previous section, it causes complications in the depth
bounded case. We briefly comment on this at the end of the section.
Let C be an EL⊥ concept and k ≥ 0. By decorating C with subconcepts from
OE at leaves, we mean to replace any number of occurrences of a quantifier-free
subconcept D by a concept D u D1 u · · · u Dk , D1 , . . . , Dk subconcepts of OE .
The following is the main result of this section.
Theorem 2. Let OE be an ELF HI⊥ ontology, Σ = sig(OE ), and ` ∈ ∪{ω} a N
depth bound. Define OL to be the ELH⊥ ontology that consists of the following,
where `0 = max{0, ` − 1} and r, r1 , r2 , s are role names from Σ:
1. all concept inclusions from OE ;
2. r v s if OE |= r v s;
3. C1 u ∃r.C2 v ∃r.(C2 u ∃s.C1 ) if OE |= r v s− , ∃s.C1 is a subconcept of OE
or an EL(Σ) concept of depth bounded by `, and C2 is an EL(Σ) concept of
depth bounded by `0 decorated with subconcepts of OE at leaves;
4. ∃r1 .C1 u ∃r2 .C2 v ∃r1 .(C1 u C2 ) if there is a role name s with OE |= r1 v s,
OE |= r2 v s, and OE 3 func(s), and C1 , C2 are EL(Σ) concepts of depth
bounded by `0 decorated with subconcepts of OE at leaves.
Then OL is an `-bounded approximation of OE .
We tried to be as economic as possible regarding the classes of concepts that
have to be considered in Points 3 and 4, which has led to the subtle depth
bounds stated there. Note that Theorem 2 also settles the cases of ELF H⊥ -
to-ELH⊥ approximation and of ELHI⊥ -to-ELH⊥ approximation (both without
any syntactic restrictions), as well as the variation of all these cases without H
and/or ⊥ in both the source and target DL.
Due to Points 3 and 4, the approximation OL is of (single) exponential
size even when ` = 0. This must necessarily be the case because otherwise
we would obtain a subexponential algorithm for the ExpTime-complete sub-
sumption problem between concept names in ELI. Note that Theorem 2 also
reproves the upper bound for this problem: compute the 0-bounded approxima-
tion of single exponential size in exponential time and then decide subsumption
in EL in PTime.
It is again straightforward to verify that the ontology OL constructed in
Theorem 2 is sound as an approximation, that is, OE |= OL . Completeness
is established in two steps. First, we introduce a suitable version of the chase
and show that it is sound and complete regarding the consequences relevant for
approximation, and second we show that the CIs in OL can simulate derivations
of this chase.
Let us now drop assumption (♥). One can prove that we then need to extend
Points 1 to 4 of Theorem 2 with the following:
5. ∃r.∃s.C v C if OE |= r v s− , func(s) ∈ OE , and C is a subconcept of OE
or an EL(Σ) concept of depth bounded by `;
6. ∃s.∃r.C v C if OE |= r v s− , func(s− ) ∈ OE , and C is a subconcept of OE
or an EL(Σ) concept of depth bounded by `.
However, this is still not sufficient to obtain a complete approximation. Consider
the ELHI ontology
OE = {A v ∃r1 .∃r2 .(B u ∃s.>), s v r1 , s v r2− , func(r1− ), func(r2− )}.
It can be verified that OE |= A v B. However, it can also be proved that even
when OL is the set of all statements from Points 1 to 6 with ` = 0, OL 6|= A v B.
5 ELI⊥ -to-EL⊥ Approximation
The previous sections concentrated on cases of L-to-L0 approximations where
both L and L0 were based on the same concept language EL⊥ . In this section,
we take a look at ELI⊥ -to-EL⊥ approximation, thus aiming to approximate
away inverse roles in concepts inclusions. We consider bounded and unbounded,
projective and non-projective approximations. The proof techniques is based on
the chase, as in the previous section.
Constructing informative non-projective approximations appears to be diffi-
cult in the ELI⊥ -to-EL⊥ case. Informally, concepts of the form ∃r− .C can be
used as a marker invisible to EL⊥ that is propagated along role edges, resulting
in rather complex EL concept inclusions to be entailed by OE .
Example 4. Let OE = {A v ∃s− .>, ∃r− .∃s− .> v ∃s− .>, ∃s− .> v B}. Then
OE |= C v C 0 for all EL concepts C, C 0 where C 0 is obtained from C by dec-
orating with B any node that is reachable in C from a node decorated with A
along an r-path (we view an EL concept as a tree in the standard way, see for
example [18]).
We now give a non-projective approximation that captures the effects demon-
strated in Example 4. For an ELI⊥ ontology OE , we use clEL (OE ) to denote
the set of all EL concepts that can be obtained by starting with a subconcept
of a concept from OE and then replacing every subconcept of the form ∃r− .D
with >. Let C be an EL concept. An EL concept C 0 is a clEL (OE ) decoration of
C if it can be obtained from C by conjunctively adding concepts from clEL (OE )
to a single occurrence of a subconcept in C.
Theorem 3. Let OE be an ELI⊥ ontology and Σ = sig(OE ). Define an EL⊥
ontology OL that consists of the following:
1. C v C 0 if OE |= C v C 0 , C an EL(Σ) concept and C 0 a clEL (OE ) decoration
of C;
2. C v ⊥ if OE |= C v ⊥, C an EL(Σ) concept;
Then OL is an approximation of OE .
We prove completeness by using the standard chase for ELI⊥ that is complete
also for ELI consequences and then work with homomorphisms that are in a
certain sense ‘forwards directed’. Details are given in the appendix.
Arguably, the approximation provided by Theorem 3 is less informative than
the ones obtained in the previous sections. We next demonstrate that in the
projective case, more informative approximations can be constructed. One way
of doing this is to first convert the ELI ⊥ ontology into an inverse closed ELHI⊥
ontology as in Section 3. Here, we pursue a natural alternative that consists of
first converting the ELI ⊥ ontology into a widely known normal form for such
ontologies [2] and then providing non-projective approximations for ontologies
in normal form. Note that, in practice, ontologies are sometimes already con-
structed in this normal form or at least in a form very close to it.
An ELI ⊥ ontology O is in normal form if all CIs in O have one of the
forms > v A1 , A1 v ⊥, A1 v ∃ρ.A2 , ∃ρ.A1 v B, and A1 u · · · u An v B
where A1 , . . . , An , B range over concept names and ρ ranges over roles. It is well
known that every ELI ⊥ ontology O can be converted in an ELI ⊥ ontology O0
in linear time such that O0 is in normal form and a conservative extension of O.
Clearly, any (projective or non-projective) approximation of O0 is a projective
approximation of O.
Theorem 4. Let OE be an ELI⊥ ontology in normal form, Σ = sig(OE ), and
` ∈ N ∪ {ω} a depth bound. Define an EL⊥ ontology OL that consists of the
following:
1. all concept inclusions from OE that are of the form > v A, A v ⊥, ∃r.A v
B, or A v ∃r.B,;
2. A1 u · · · u An v B if OE |= A1 u · · · u An v B, A1 , . . . , An , B ∈ NC in OE ;
3. A u ∃r.C v ∃r.(C u B) if ∃r− .A v B ∈ OE and C is an EL(Σ) concept of
depth bounded by ` − 1.
Then OL is an appoximation of OE .
It is straightforward to verify that OL is sound. To prove completeness, we
use the same strategy as for Theorem 2.
6 Size of Approximations
We prove that finite approximations do not necessarily exist and that depth
bounded approximations can be non-elementary in size. These results hold both
for projective and non-projective approximations and for all combinations of
source and target DL considered in this paper. The ontologies used to prove
these results are simple and show that for the vast majority of ontologies that
occur in practical applications, neither finite approximations nor depth bounded
approximations of elementary size can be expected. We focus on the cases ELIH-
to-ELH, ELHF-to-ELH, and ELHI -to-ELH, starting with the non-existence of
finite approximations.
Theorem 5. None of the ontologies
{∃r− .A v B}, {func(r), A v A}, {r v s− , A v A}
has finite projective ELH approximations.
We next show that bounded depth approximations can be non-elementary
in size. The function tower : ×N N → N
is defined as tower(0, n) := n and
tower(k + 1, n) := 2tower(k,n) . The size of a (finite) ontology is the number
of symbols needed to write it, with concept and role names counting as one.
We use Γn to denote a fixed finite tautological set of EL concept inclusions
that contains the symbols Σn = {r1 , r2 , A1 , Â1 , . . . , An , Ân }. One could take, for
example, ∃r1 .> v >, ∃r2 .> v >, and all A v A with A ∈ {A1 , Â1 , . . . , An , Ân }.
Theorem 6. Let n ≥ 0 and let On be the union of Γn with any of the following
sets:
{∃r− .A v B}, {func(r), A v A}, {r v s− , A v A}
For every ` ≥ 1, any `-bounded projective ELH approximation OL of On must
be of size at least tower(`, n).
7 Conclusion
There are several questions that emerge from our work. For example, it remains
an open problem to develop a convincing approximation for ELHI F⊥ -to-ELH⊥
in the non-projective case, or even for Horn-SRIF-to-ELR⊥ . It would also be
useful to consider more expressive target DLs such as the extension of ELH⊥ or
ELR⊥ with range restrictions, and to add nominals to the picture. Of course,
it would also be very interesting to approximate non-Horn DLs such as ALC,
SHIQ, and SROIQ in (tractable and intractable) Horn DLs.
From a conceptual perspective, it would be of great interest to understand
how approximations can be tailored towards intended applications. In this con-
text, observe that all our bounded depth approximation schemes still work when
the set of concepts of depth ` is replaced with any set Γ of concepts closed un-
der subconcepts. For example, if one wants to decide subsumption between EL
concepts C and D relative to an ELI ontology OE , one can approximate OE in
EL relative to the set Γ of subconcepts of C and D; the resulting EL ontology
OL will entail C v D iff OE does. In a similar spirit, it would be interesting to
develop approximations that aim at query answering applications.
Acknowledgments. Supported by the DFG Collaborative Research Center
1320 EASE - Everyday Activity Science and Engineering.
References
1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. of IJCAI.
Morgan Kaufmann (2005)
2. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description
Logic. Cambridge University Press (2017)
3. Beklemishev, L.D.: Positive provability logic for uniform reflection principles. Ann.
Pure Appl. Logic 165(1), 82–105 (2014)
4. van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.)
Handbook of Philosophical Logic, vol. 2, pp. 167–247. Reidel, Dordrecht (1984)
5. Bienvenu, M., Hansen, P., Lutz, C., Wolter, F.: First order-rewritability and con-
tainment of conjunctive queries in horn description logics. In: Proceedings of IJCAI.
pp. 965–971 (2016)
6. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press
(2001)
7. Botoeva, E., Calvanese, D., Rodriguez-Muro, M.: Expressive approximations in
DL-Lite ontologies. In: AIMSA. pp. 21–31 (2010)
8. Botoeva, E., Calvanese, D., Santarelli, V., Savo, D.F., Solimando, A., Xiao, G.:
Beyond OWL 2 QL in OBDA: rewritings and approximations. In: Proc. of AAAI.
pp. 921–928. AAAI Press (2016)
9. Brandt, S., Küsters, R., Turhan, A.Y.: Approximation and difference in description
logics. In: KR. pp. 203–214 (2002)
10. Carral, D., Feier, C., Grau, B.C., Hitzler, P., Horrocks, I.: EL-ifying ontologies. In:
Proc. of IJCAR. pp. 464–479 (2014)
11. Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17,
229–264 (2002)
12. Feier, C., Lutz, C., Kuusisto, A.: Rewritability in monadic disjunctive datalog,
MMSNP, and expressive description logics. In: Proceedings of the 20th Interna-
tional Conference on Database Theory (ICDT17) (2017)
13. Goldblatt, R.: Varieties of complex algebras. Annals of Pure and Applied Logic
44, 173–242 (1989)
14. Groot, P., Stuckenschmidt, H., Wache, H.: Approximating description logic classi-
fication for semantic web reasoning. In: Proc. of ESWC. pp. 318–332 (2005)
15. Hernich, A., Lutz, C., Papacchini, F., Wolter, F.: Horn-rewritability vs PTime
query evaluation in ontology-mediated querying. In: Proceedings of IJCAI-ECAI.
AAAI Press (2018)
16. Jackson, M.: Semilattices with closure. Algebra Universalis 52, 1–37 (2004)
17. Kikot, S., Kurucz, Á., Tanaka, Y., Wolter, F., Zakharyaschev, M.: Kripke com-
pleteness of strictly positive modal logics over meet-semilattices with operators.
CoRR abs/1708.03403 (2017), http://arxiv.org/abs/1708.03403
18. Konev, B., Lutz, C., Ozaki, A., Wolter, F.: Exact learning of lightweight description
logic ontologies. Journal of Machine Learning Research 18(201), 1–63 (2018)
19. Konev, B., Lutz, C., Wolter, F., Zakharyaschev, M.: Conservative rewritability of
description logic TBoxes. In: Proc. of IJCAI. pp. 1153–1159 (2016)
20. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of horn description logics.
ACM Trans. Comput. Log. 14(1), 2:1–2:36 (2013)
21. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: Model-theoretic charac-
terizations and rewritability. In: IJCAI. pp. 983–988 (2011)
22. Lutz, C., Seylan, I., Wolter, F.: An automata-theoretic approach to uniform inter-
polation and approximation in the description logic EL. In: Proc. of KR. AAAI
Press (2012)
23. Lutz, C., Wolter, F.: Deciding inseparability and conservative extensions in the
description logic EL. J. Symb. Comput. 45(2), 194–228 (2010)
24. Pan, J.Z., Thomas, E.: Approximating OWL-DL ontologies. In: AAAI. pp. 1434–
1439 (2007)
25. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for TBox rea-
soning. In: AAAI (2010)
26. Schaerf, M., Cadoli, M.: Tractable reasoning via approximation. Artificial Intelli-
gence 74(2), 249 – 310 (1995)
27. Selman, B., Kautz, H.A.: Knowledge compilation and theory approximation. J.
ACM 43(2), 193–224 (1996)
28. Sofronie-Stokkermans, V.: Locality and subsumption testing in EL and some of its
extensions. In: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic, vol. 7.
pp. 315–339. College Publications (2008)
29. Sofronie-Stokkermans, V.: Representation theorems and locality for subsumption
testing and interpolation in the description logics EL and EL+ and their exten-
sions with n-ary roles and numerical domains. Fundam. Inform. 156(3-4), 361–411
(2017)
30. Tserendorj, T., Rudolph, S., Krötzsch, M., Hitzler, P.: Approximate owl-reasoning
with screech. In: Proc. of RR. LNCS, vol. 5341, pp. 165–180. Springer (2008)
31. Zhou, Y., Grau, B.C., Nenov, Y., Kaminski, M., Horrocks, I.: Pagoda: Pay-as-you-
go ontology query answering using a datalog reasoner. J. Artif. Intell. Res. 54,
309–367 (2015)