We study the approximation of expressive Horn DL ontologies in less expressive Horn DLs, with completeness guarantees. Cases of interest include Horn-SRIF -to-ELR?, Horn-SHIF -to-ELH?, and others. Since nite approximations almost never exist, we carefully map out the structure of in nite approximations. This provides a solid theoretical foundation for constructing incomplete approximations in practice in a controlled way. Technically, we exibit a connection to the axiomatization 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.
demand that OE j= OL and for every L ontology O in signature , OE j= O implies OL j= O. We consider both the case where OL is formulated in (nonprojective 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 in nite ontologies even in simple cases. For example, consider the ELI ontology OE = f9hasSupervisor :> v Managerg which contains only a single range restriction. There is no nite EL approximation OL since for all n 1, OE entails the EL concept inclusion
Also for the ELF ontology OE = ffunc(hasSupervisor); func(reportsTo)g, there is no nite EL approximation OL since for all n; m 1, OE entails the EL concept inclusion4
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 in nite approximations. As the expressive DL L, we consider
HornSRIF and fragments thereof. As the fragment L0, we consider ELR? and
corresponding 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
-toELR? approximation, Horn-SHIF -to-ELH?, ELI-to-EL, ELF -to-EL, and so
on. Subsumption is ExpTime-complete in all mentioned source DLs and
PTimecomplete in all mentioned target DLs [
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 complex role inclusions, which is actually a very common way to use inverse roles in practice. The presented approximation requires that OE is inverse closed, meaning that for every role name r in OE, there is a role name r^ that is de ned 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 -toE LR? 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 operators (SLOs); note that SLOs have been used before to obtain algorithms for subsumption in extensions of E L [28, 29].
In Section 4, we construct non-projective E LHI F?-to-E LH? approximations under the mild assumption that whenever OE j= r v s , then neither func(s) 2 OE nor func(s ) 2 OE . This again encompasses relevant subcases such as E LHF -to-E LH, without any syntactic assumptions. The main di erence to Section 3 is how completeness is established. Here, we nd a chase procedure for L ontologies that is inspired by and closely linked to the proposed approximation 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 nite approxmations always exist if we restrict the role depth of concepts in consequences to be bounded by a constant; we speak of depth bounded approximations.
We then proceed to study E LI?-to-E L? approximations in Section 5. In contrast to the cases considered before, where both L and L0 are based on the concept language E L?, here the concept language of L (which is E LI?) di erent from the one of L0 (which is E L?). We present non-projective approximations for unrestricted ontologies OE and for ontologies OE which are in the well-known normal form for E LI? ontologies that avoids syntactic nesting of concepts. The two approximation schemes are remarkably di erent, the latter arguably being more informative than the former.
In Section 6, we complement the proposed in nite approximations by showing that nite 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 rst studied in [27]
where F L concepts are approximated by F L concepts and in [
Let NC and NR be disjoint and countably in nite 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 de ned by the syntax rules
R; R0 ::= > j ? j A j :A j R u R0 j :L t R j 9 :R j 8 :R
L; L0 ::= > j ? j A j L u L0 j L t L0 j 9 :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 9r:B u 9r:9s: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 j= func( ) nor O j= func( ). Ontologies used in practice of course have to be nite. In this paper, though, we shall frequently consider also in nite ontologies.
An E LRIF ? ontology is a Horn-SRIF ontology in which both the left- and right-hand sides of CIs are E LI? concepts, de ned as usual, and that does not contain transitivity assertions. If O uses neither inverse roles nor functionality assertions, then it is an E LR? ontology. We assume w.l.o.g. that, in E LRIF ? 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 concept language. For example, the ontology language E LHIF ? is based on the concept language E LI?. 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 [
De nition 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 in nite) L ontology OL is an L approximation of OE if the following conditions are satis ed: 1. OE j= C v D i OL j= 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 j= i OL j= . We call OL a non-projective E L approximation if sig(OL) and projective otherwise.
are de ned 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 De nition 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, in nite (non-projective and projective) approximations always exist: simply take as OL the set of all relevant inclusions and assertions that are entailed by OE . De nition 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 E LI ontologies OE that have a nite projective E L approximation, but no nite non-projective E L approximation. Details are in the appendix. An alternative de nition of approximations 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, nite approximations do not necessarily exist. Example 1. Consider the E LI ontology OE = f9r :A v Bg. We have as a consequence Au9r:X v 9r:(B uX) for each of the in nitely many concept names X 2 NC. Thus, every (projective or non-projective) 1-bounded E L approximation of OE must be in nite under the alternative de nition 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 ) = ment of Horn-SRIF . Then and L a frag1. an L ontology OL is an L approximation of OE i OE j= OL and for every
L ontology O with OE j= O and sig(O) , OL j= O; 2. Si 0 O` is an L approximation of OE if for all ` 0, O` is an `-bounded
Point 1 may be viewed as an alternative de nition of (non-projective)
approximations. Point 2 is important because it allows us to concentrate on bounded
approximations in proofs and to then obtain results for unbounded
approximations as a byproduct. The following is well-known, see for example [
Note that the construction of the ontology OE0 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 E LRIF ? 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 E LRI F?-to-E LR? Approximation We provide (unbounded) approximations of E LRIF? ontologies in E LR?. We assume throughout this section that E LRIF? 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 su ces to consider inverse closed E LRI F? ontologies in place of inverse closed E LRIF? 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 E LRI F? ontology and = sig(OE ). De ne OL to be the E LR? ontology that contains for all E L( ) concepts C; D and role names r; s 2 : 1. all CIs in OE ; 2. r v s if OE j= r v s; 3. r1 rn v r; r^n r^1 v r^ if r1 4. C u 9r:D v 9r:(D u 9r^:C); 5. 9r:C u 9r:D v 9r:(C u D) if func(r) 2 OE ; 6. 9r:9r^:C v C if func(r^) 2 OE .
rn v r 2 OE with n 2;
Note that Points 1 to 3 essentially take over the part of OE that is expressible in E LR?, 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 inverse roles. Points 4 to 6 all introduce in nitely many CIs. The following example shows that Point 6 cannot be omitted.
Example 2. Consider OE = ffunc(r^); r v r^ ; r^ v r ; A v Ag Then OE j= 9r:9r^:A v A but OL0 6j= 9r:9r^:A v A for the ontology OL0 obtained from OL by omitting the CIs of Point 6. To show this, consider the interpretation I with domain f0; 1; : : :g and rI = f(2n; 2n + 1) j n 0g; r^I = f(2n + 1; 2n + 2) j n 0g; AI = f2n j n 1g Then I is a model of OL0 but 0 2 (9r:9r^:A)I n 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 = f9supervises:> v Manager; hasSuper v supervises ; supervises v hasSuperg. Point 4 yields
which together with 9supervises:> v Manager 2 OL yields the desired
Theorem 1 also settles several natural subcases of (projective) ELRI F?-toELR? 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 closedness. This could also be avoided, as in the results presented in the subsequent section. We nd it remarkable that the construction of OL is based almost entirely 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
between EL? approximations and axiomatizations of the quasi-equations that are
valid in classes of semilattices with operators (SLOs) [
Depth-Bounded E LHI F?-to-E LH? Approximation We pursue an alternative approach to proving that an approximation is complete, 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 E LHI F?-to-E LH? approximation and subcases 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 j= r v s implies that neither func(s) 2 OE nor func(s ) 2 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 approximation scheme given in the previous section, it causes complications in the depth bounded case. We brie y comment on this at the end of the section.
OE at leaves, we mean to replace any number of occurrences of a quanti er-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 E LF HI? ontology, = sig(OE ), and ` 2 N [ f!g a depth bound. De ne OL to be the E LH? ontology that consists of the following, where `0 = maxf0; ` 1g and r; r1; r2; s are role names from :
2. r v s if OE j= r v s; 3. C1 u 9r:C2 v 9r:(C2 u 9s:C1) if OE j= r v s , 9s:C1 is a subconcept of OE or an E L( ) concept of depth bounded by `, and C2 is an E L( ) concept of depth bounded by `0 decorated with subconcepts of OE at leaves; 4. 9r1:C1 u 9r2:C2 v 9r1:(C1 u C2) if there is a role name s with OE j= r1 v s, OE j= r2 v s, and OE 3 func(s), and C1; C2 are E L( ) concepts of depth bounded by `0 decorated with subconcepts of OE at leaves.
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 E LF H?
I -to-E LH? approximation (both without to-E LH? approximation and of E LH? 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 subsumption problem between concept names in E LI. Note that Theorem 2 also reproves the upper bound for this problem: compute the 0-bounded approximation of single exponential size in exponential time and then decide subsumption in E L in PTime.
It is again straightforward to verify that the ontology OL constructed in Theorem 2 is sound as an approximation, that is, OE j= 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. 9r:9s:C v C if OE j= r v s , func(s) 2 OE, and C is a subconcept of OE or an EL( ) concept of depth bounded by `; 6. 9s:9r:C v C if OE j= r v s , func(s ) 2 OE, and C is a subconcept of OE or an EL( ) concept of depth bounded by `.
However, this is still not su cient to obtain a complete approximation. Consider the ELHI ontology OE = fA v 9r1:9r2:(B u 9s:>); s v r1; s v r2 ; func(r1 ); func(r2 )g: It can be veri ed that OE j= 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 6j= A v B. 5
E LI?-to-E L? 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 di cult in the ELI?-to-EL? case. Informally, concepts of the form 9r :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 = fA v 9s :>; 9r :9s :> v 9s :>; 9s :> v Bg: Then
OE j= C v C0 for all EL concepts C; C0 where C0 is obtained from C by
decorating 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 [
We now give a non-projective approximation that captures the e ects demonstrated 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 9r :D with >. Let C be an EL concept. An EL concept C0 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.
ontology OL that consists of the following: = sig(OE ). De ne an E L? 1. C v C0 if OE j= C v C0, C an E L( ) concept and C0 a clEL(OE ) decoration of C; 2. C v ? if OE j= C v ?, C an E L( ) concept;
We prove completeness by using the standard chase for E LI? that is complete also for E LI 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 rst convert the E LI? ontology into an inverse closed E LHI?
ontology as in Section 3. Here, we pursue a natural alternative that consists of
rst converting the E LI? ontology into a widely known normal form for such
ontologies [
An E LI? ontology O is in normal form if all CIs in O have one of the forms > v A1, A1 v ?, A1 v 9 :A2, 9 :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 E LI? ontology O can be converted in an E LI? 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 E LI? ontology in normal form, = sig(OE ), and ` 2 N [ f!g a depth bound. De ne an E L? ontology OL that consists of the following:
B, or A v 9r:B,; 2. A1 u u An v B if OE j= A1 u u An v B, A1; : : : ; An; B 2 NC in OE ; 3. A u 9r:C v 9r:(C u B) if 9r :A v B 2 OE and C is an E L( ) concept of depth bounded by ` 1.
It is straightforward to verify that OL is sound. To prove completeness, we use the same strategy as for Theorem 2. 6
We prove that nite 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 nite approximations nor depth bounded approximations of elementary size can be expected. We focus on the cases E LIHto-E LH, E LHF -to-E LH, and E LHI -to-E LH, starting with the non-existence of nite approximations.
Theorem 5. None of the ontologies f9r :A v Bg; ffunc(r); A v Ag; fr v s ; A v Ag has nite projective E LH approximations.
We next show that bounded depth approximations can be non-elementary in size. The function tower : N N ! N is de ned as tower(0; n) := n and tower(k + 1; n) := 2tower(k;n). The size of a ( nite) ontology is the number of symbols needed to write it, with concept and role names counting as one. We use n to denote a xed nite tautological set of E L concept inclusions that contains the symbols n = fr1; r2; A1; A^1; : : : ; An; A^ng. One could take, for example, 9r1:> v >, 9r2:> v >, and all A v A with A 2 fA1; A^1; : : : ; An; A^ng.
0 and let On be the union of n with any of the following Theorem 6. Let n sets: f9r :A v Bg; ffunc(r); A v Ag; fr v s ; A v Ag
be of size at least tower(`; n). 7
There are several questions that emerge from our work. For example, it remains an open problem to develop a convincing approximation for E LHI F?-to-E LH? in the non-projective case, or even for Horn-SRIF -to-E LR?. It would also be useful to consider more expressive target DLs such as the extension of E LH? or E LR? 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 context, 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 under subconcepts. For example, if one wants to decide subsumption between E L concepts C and D relative to an E LI ontology OE , one can approximate OE in E L relative to the set of subconcepts of C and D; the resulting E L ontology OL will entail C v D i 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. 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 reasoning. In: AAAI (2010) 26. Schaerf, M., Cadoli, M.: Tractable reasoning via approximation. Arti cial Intelligence 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 extensions with n-ary roles and numerical domains. Fundam. Inform. 156(3-4), 361{411 (2017) 30. Tserendorj, T., Rudolph, S., Krotzsch, 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-yougo ontology query answering using a datalog reasoner. J. Artif. Intell. Res. 54, 309{367 (2015)