# ontology_approximation_in_horn_description_logics__45f11171.pdf

Ontology Approximation in Horn Description Logics

Anneke B otcher1 , Carsten Lutz1 , Frank Wolter2

1University of Bremen, Germany 2University of Liverpool, UK {anneke, clu}@uni-bremen.de, wolter@liverpool.ac.uk

We study the approximation of a description logic (DL) ontology in a less expressive DL, focussing on the case of Horn DLs. It is common to construct such approximations in an ad hoc way in practice and the resulting incompleteness is typically neither analyzed nor understood. In this paper, we show how to construct complete approximations. These are typically infinite or of excessive size and thus cannot be used directly in applications, but our results provide an important theoretical foundation that enables informed decisions when constructing incomplete approximations in practice.

1 Introduction

There is a large number of description logics (DLs) that vary considerably regarding their expressive power and computational properties [Baader et al., 2017] and despite prominent standardization efforts, many different DLs continue to be used.1 As a result, it can be necessary to convert an ontology formulated in a DL LS, the source DL, into a different DL LT , the target DL. For example, this happens in ontology import when an engineer who designs an ontology formulated in LT wants to reuse content from an existing ontology formulated in LS. A particularly important case is that LT is a fragment of LS, in which case the described problem is ontology approximation, a form of knowledge compilation [Selman and Kautz, 1996; Darwiche and Marquis, 2002]. In this paper, we are interested in approximating an ontology OS formulated in a DL LS by an ontology OT formulated in a fragment LT of LS, aiming to preserve all information from OS that is expressible in LT ; this is called a greatest lower bound in knowledge compilation [Selman and Kautz, 1996]. Formally, for every LT concept inclusion C D that is formulated in the signature Σ of OS, we require that OS |= C D if and only if OT |= C D, and likewise for role inclusions and any other type of ontology statement supported by LT . We say that OT is sound as an approximation if it satisfies the if part of this property and complete if it satisfies the only if part. We consider the case that

1See, for example, the Bio Portal repository at https://bioportal. bioontology.org/.

OT must be formulated in Σ (non-projective approximation) and the case that additional symbols are admitted (projective approximation). In practice, approximations are often constructed in an ad hoc way that is sound but not complete. In fact, it is common to simply drop all statements from OS that are not expressible in LT , or at least inexpressible parts thereof. This easily leads to incompleteness, as illustrated by the following example extracted from the Galen ontology2, slightly simplified for presentation purposes. Let Patho Phen stand for pathological phenomenon , is Con Of for is consequence of , and has Con for has consequence . Galen contains the following statements formulated in the DL ELHI, the first three being concept inclusions and the fourth one a role inclusion:

Hyperhidrosis Patho Phen has Con.Clammy Skin is Con Of.Patho Phen Patho Phen has Con.Patho Phen Precipitating Factor has Con is Con Of .

These imply as a consequence

Hyperhidrosis Precipitating Factor. (1)

Assume that this ontology has to be approximated in the fragment ELH of ELHI that does not admit inverse roles. A typical ad hoc approach would be to simply drop the role inclusion in the fourth line, resulting in an incomplete approximation that no longer has Consequence (1). This, however, can easily be fixed by further adding the concept inclusion

Hyperhidrosis has Con. has Con. is Con Of.Hyperhidrosis. (2)

as a (partial) substitute of the dropped role inclusion. The aim of this paper is to systematically study the structure of complete ontology approximations. There is, however, a major caveat. As we show, complete approximations must be infinite even in rather simple cases. Moreover, while finite approximations exist when the depth of the concept inclusions to be preserved is bounded by a constant, the resulting approximations are still of non-elementary size. There is no miraculous way around these facts and thus the approximations constructed in this paper cannot be directly used in

2http://www.opengalen.org/

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

applications. However, they provide an important theoretical foundation that enable and guide informed decisions when constructing incomplete approximations in practice. In the above example taken from Galen, for instance, concept inclusion (2) is part of the complete approximation proposed in this paper and thus an explicit candidate for inclusion also in approximations constructed in practice. As the source DL LS, we consider the expressive Horn DL Horn-SRIF and fragments thereof. As the target DL LT , we consider ELR and corresponding fragments thereof, where ELR denotes the extension of the more widely known DL ELH with role inclusions of the form r1 rn r. Subsumption is EXPTIME-complete in all considered source DLs and PTIME-complete in all cosidered target DLs [Baader et al., 2005; Kr otzsch et al., 2013]. While our approximations do not aim at efficient reasoning, 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 computationally more expensive DL. We provide the following results. In Section 3, we construct ELF-to-EL approximations, thus approximating away functional roles. We then proceed to ELHI-to-ELH, approximating away inverse roles, where the I typeset in small font means that inverse roles are admitted only in role inclusions of the form r s but not in concept inclusions. This is a very common way to use inverse roles in practice, for example more than 96% of the ontologies in Bio Portal that use inverse roles at all use them only in this form and this is similar for other ontology repositories. We next treat ELHIF - to-ELH under a certain syntactic assumption that restricts the interplay of role inclusions, functional roles, and inverse roles in OS. This covers also other relevant subcases such as ELHF-to-ELH, without syntactic restrictions. All approximations constructed in Section 3 are non-projective and also provide finite approximations in the depth bounded case. The completeness proofs are non-trivial and use a version of the chase that is specifically tailored to our approximation schemes. In Section 4, we present ELRIF -to-ELR approximations. The presented approximations are non-projective when OS is inverse closed, meaning that for every role name r in OS, there is a role name ˆr that is defined via role inclusions 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 wellknown normalization procedure. The completeness proof is again non-trivial, but based on a different approach, namely a novel connection between ontology approximation and the axiomatizations of quasi-equations valid in classes of semilattices with operators (SLOs) [Sofronie-Stokkermans, 2013; Sofronie-Stokkermans, 2017; Kikot et al., 2017]. We then proceed to study ELI -to-EL approximations in Section 5. In contrast to the cases considered before, where (after normalization) both LS and LT are based on the concept language EL , here the concept language of LS is different from the one of LT . We present non-projective approximations for unrestricted ontologies OS and for ontologies OS which are in the well-known normal form for ELI ontologies that avoids syntactic nesting of concepts. The two

approximation schemes are remarkably different. In Section 6, we show that finite approximations are not guaranteed to exist and that there are cases where depth bounded approximations must be non-elementary in size. Proof details are available in the appendix, which is available at http://www.informatik.uni-bremen.de/tdki/.

Related Work Approximation in a DL context was first studied in [Selman and Kautz, 1996] where FL concepts are approximated by FL concepts and in [Brandt et al., 2002] 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-Lite F is presented in [Pan and Thomas, 2007] and complete (projective) approximations of SROIQ ontologies in DL-Lite A are given in [Botoeva et al., 2010]. Such approximations are guaranteed to exist due to the limited expressive power of DL-Lite A. In [Lutz et al., 2012], 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 whether a finite complete approximation exists. An incomplete approach to approximating SROIQ ontologies in EL++ is in [Ren et al., 2010]. There are also approaches towards efficient DL reasoning that involve computing approximations which are intentionally incomplete to avoid compromising efficiency [Schaerf and Cadoli, 1995; Groot et al., 2005; Carral et al., 2014]. Related to approximation is the problem whether a given LS ontology can be equivalently rewritten into the fragment LT of LS, either non-projectively [Lutz et al., 2011] or projectively [Konev et al., 2016]; note that this asks whether we have to approximate at all.

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 R, where L and R are concepts defined by the syntax rules

R, R ::= | | A | A | R R | L R | ρ.R | ρ.R

L, L ::= | | A | L L | L L | ρ.L

with A ranging over concept names and ρ over roles. The depth of a concept R or L is the nesting depth of the constructors ρ and ρ. For example, the concept r.B r. s.A is of depth 2. A Horn-SRIF ontology O is a set of Horn-SRIF concept inclusions, functionality assertions func(ρ), and role inclusions (RIs) ρ1 ρn ρ. We adopt the standard restriction that if n 2, then neither O |= func(ρ) nor O |= func(ρ ). The semantics of Horn-SRIF is standard, see [Baader et al., 2017]. While ontologies used in practice have to be finite, in this paper we shall frequently consider also infinite ontologies. W.l.o.g,, we generally assume that the concept occurs only in CIs of the form C , where C does not contain .

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

We briefly introduce the relevant fragments of Horn SRIF, for details see [Baader et al., 2017]. An ELI concept is built according to the syntax rule for L above, but omitting disjunction. An ELRIF ontology is a Horn SRIF ontology in which both the leftand right-hand sides of CIs are ELI concepts. ELHIF is defined likewise, but admitting only role hierarchies instead of role inclusions, which take the form r s. Fragments of ELRIF and ELHIF can obtained by dropping expressive means that are identified by a standard naming scheme: H indicates role hierarchies, R role inclusions, I inverse roles, F functionality assertions, and the bottom concept. It should thus be understood, for example, what an ELI ontology is and what an EL concept is. Among these DLs, ELR is maximal with a tractable subsumption problem. In all of the above DLs not contained in ELR , subsumption is EXPTIME-complete [Baader et al., 2005; Baader et al., 2008]. A signature Σ is a set of concept and role names, uniformly referred to as symbols. When speaking of EL(Σ) concept, we mean EL concepts that only use symbols from Σ, and likewise for other DLs. We use sig(O) to denote the set of symbols used in ontology O. We now define the central notions of this paper. Definition 1 Let OS be a Horn-SRIF ontology with sig(OS) = Σ and let LT be any of the fragments of Horn SRIF introduced above. A (potentially infinite) LT ontology OT is an LT approximation of OS if

OS |= α iff OT |= α

for all concept inclusions, role inclusions, and functionality assertions α that fall within LT and use only symbols from Σ. We say that OT is non-projective if sig(OT ) Σ and projective otherwise. For ℓ N {ω}, (non-projective and projective) ℓbounded LT approximations are defined in the same way except that only concept inclusions α = C D are considered where C and D are of depth bounded by ℓ. Note that ω-bounded approximations are identical to unbounded approximations, we use the term only for uniformity. Trivially, infinite (non-projective and projective) approximations always exist: take as OT the set of all inclusions and assertions from LT that are entailed by OS. One can show that there are ELI ontologies OS that have a finite projective EL approximation, but no finite non-projective EL approximation; details are in the appendix. Example 1 Consider the ELF ontology

OS = { has Supervisor. Employee, func(reports To)}.

There is no finite EL approximation since for all n, m 1, OS entails the EL concept inclusion

reports To. has Supervisorn. reports Tom. reports To.( has Supervisorn. reports Tom 1. ).

In practice, it clearly does not make sense to include all these CIs in the approximation. Similarly to the example in the

introduction, though, it may pay off to include some of them. Choosing the right ones requires a careful inspection of the ontology and application at hand.

With LS-to-LT approximation, LS an ontology language and LT a fragment thereof, we mean the task of approximating an LS ontology in LT . We call LS the source DL and LT the target DL. An alternative definition of approximations is obained by dropping the restriction that α can use only symbols from Σ. We do not use that definition because then even in the 1-bounded case, finite approximations might not exist.

Example 2 Take the ELI ontology OS = { r .A B}. Then O |= A r.X r.(B X) for each of the infinitely many concept names X NC. Thus, every (projective or non-projective) 1-bounded EL approximation of OS must be infinite under the alternative definition of approximation.

We now make some basic observations regarding approximations. The proof is straightforward.

Lemma 1 Let OS be a Horn-SRIF ontology with sig(OS) = Σ and LT a fragment of Horn-SRIF. Then

1. OT is an LT approximation of OS iff OS |= OT and for every LT ontology O with OS |= O and sig(O) Σ, OT |= O;

2. S i 0 Oℓis an LT approximation of OS if for all ℓ 0, Oℓis an ℓ-bounded LT approximation of OS; the same is true for projective LT approximations provided that sig(Oℓ) sig(Oℓ ) Σ when ℓ = ℓ .

Point 1 may be viewed as an alternative definition of (nonprojective) approximations. Point 2 is important because it sometimes allows us to concentrate on bounded approximations in proofs. The following is well-known, see for example [Bienvenu et al., 2016].

Lemma 2 Given a Horn-SRIF ontology OS with sig(O) = Σ, one can construct in polynomial time an ELRIF ontology O S with sig(O S) Σ that entails the same Horn-SRIF(Σ) concept inclusions, role inclusions, and functionality assertions.

The construction of the ontology O S from Lemma 2 requires the introduction of fresh concept names. Still, every ℓbounded LT approximation of O S is a projective ℓ-bounded LT approximation of OS.

3 Depth Bounded Approximation

The goal of this section is to study non-projective approximations in various DLs, both in the unbounded case and in the depth bounded case. We start with approximating away functionality assertions, then inverse roles, and finally their combination (assuming a certain syntactic restriction), also admitting role hierarchies and the bottom concept. This stepby-step approach aims to facilitate presentation and in fact the final theorem in this section subsumes the earlier ones and is the only one that we prove explicitly. We start with ELF-to-EL approximation. Let C be an EL concept and k 0. A leaf occurrence of a concept name A in C means an occurrence of A inside a conjunction that

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

does not contain conjuncts of the form r.D. For example, all occurrences of A in A B and in B r.(A B) are leaf occurrences, but the occurrence of A in A B r. is not. By decorating C with subconcepts from OS at leaves, we mean to replace any number of leaf occurrences of a concept name A by a concept A D1 Dk where D1, . . . , Dk are concepts that occur in OS, possibly as subconcepts. Theorem 1 Let OS be an ELF ontology, Σ = sig(OS), and ℓ N {ω} a depth bound. Define OT to be the EL ontology that contains: 1. all CIs from OS; 2. all CIs r.C1 r.C2 r.(C1 C2) such that func(r) OS and C1, C2 are EL(Σ) concepts of depth bounded by max{0, ℓ 1} decorated with subconcepts of OS at leaves. Then OT is an ℓ-bounded approximation of OS. Note that the construction of OT is entirely syntactic, that is, it involves no reasoning. Due to Point 2, OT is infinite when ℓ= ω. On the other hand, OT is finite when ℓ< ω and thus Theorem 1 proves the existence of finite depth bounded non-projective approximations in the ELF-to-EL case. It is interesting to remark that Theorem 1 also reproves the upper bound for subsumption in ELF: first extend the ontology so that it suffices to decide subsumption between concept names, then compute the 0-bounded approximation which is of single exponential size, and then decide subsumption in EL in PTIME [Baader et al., 2005]. Note that for ℓ= 0, the concepts C1, C2 in Point 2 of Theorem 1 are simply conjunctions of subconcepts from OS. We next consider inverse roles. Here, the most basic case is that inverse roles can occur in role inclusions, but not in concepts. As noted in the introduction, this case actually occurs rather frequently in practice. To indicate the restricted use of inverse roles, we typeset the I in a smaller font, as in ELHIF and ELRIF. The most basic case is now that of ELHI-to-ELH approximation. We assume w.l.o.g. that role inclusions only take the two forms r s and r s . Theorem 2 Let OS be an ELHI ontology, Σ = sig(OS), and ℓ N {ω} a depth bound. Define OT to be the ELH ontology that contains, for ℓ = max{0, ℓ 1}: 1. all CIs from OS; 2. all RIs r s such that OS |= r s and role names r, s occur in OS; 3. all CIs C1 r.C2 r.(C2 s.C1) such that OS |= r s , s.C1 is a subconcept of OS or an EL(Σ) concept of depth bounded by ℓ, and C2 is an EL(Σ) concept of depth bounded by ℓ decorated with subconcepts of OS at leaves. Then OT is an ℓ-bounded approximation of OS. Note that Point 2 is not entirely syntactic, but involves reasoning. It is easy to see and well-known, however, that in ELI deciding whether OS |= r s is in PTIME. We now consider the ELHIF -to-ELH case which combines functional and inverse roles. It turns out that there are subtle interactions between functional, inverse roles, and role hierarchies which we tame by making the following assumption:

( ) OS |= r s implies that neither func(s) OS nor func(s ) OS. The next theorem is the main result of this section. Theorem 3 Let OS be an ELHIF ontology that satisfies ( ), Σ = sig(OS), and ℓ N {ω} a depth bound. Define OT to be the ELH ontology that contains, for ℓ = max{0, ℓ 1}: 1. all CIs from OS; 2. all r s such that OS |= r s, r, s role names that occur in OS; 3. all CIs C1 r.C2 r.(C2 s.C1) such that OS |= r s , s.C1 is a subconcept of OS or an EL(Σ) concept of depth bounded by ℓ, and C2 is an EL(Σ) concept of depth bounded by ℓ decorated with subconcepts of OS at leaves; 4. all CIs r1.C1 r2.C2 r1.(C1 C2) such that there is a role name s with OS |= r1 s, OS |= r2 s, and func(s) OS, and C1, C2 are EL(Σ) concepts of depth bounded by ℓ decorated with subconcepts of OS at leaves. Then OT is an ℓ-bounded approximation of OS. It is not hard to see that Theorem 3 implies Theorems 1 and 2. It also settles additional approximation cases such as ELHF -to-ELH , without syntactic assumptions. Points 2 to 4 require deciding whether OS |= r s( ), which is EXPTIME-complete in ELHIF as can be proved by mutual reduction with subsumption. It is straightforward to verify that the ontology OT constructed in Theorem 3 is sound as an approximation, that is, OS |= OT . Completeness is non-trivial. It is established by first introducing a version of the chase that is closely tailored towards the construction of OT given in Theorem 3, then showing that the chase is sound and complete regarding the derivation of EL(Σ) CIs of depth bounded by ℓ, and finally proving that the CIs in OT can simulate derivations of the chase. With chase, we mean a rule based approach to constructing (infinite) canonical models [Kontchakov and Zakharyaschev, 2014]. An interesting observation about the proof of Theorem 3 is that it actually yields a more general result than stated in that theorem. Instead of ℓ-bounded approximations, one could define Γ-bounded approximations for any set of EL -concepts Γ closed under subconcepts, that is, only concepts from Γ are considered in concept inclusions α in Definition 1. We then obtain a version of Theorem 3 in which concept of depth bounded by ℓor ℓ is replaced with concept from Γ (decorated with subconcepts of OS at leaves as needed). While one could choose for Γ the set of all concepts of depth bounded by some ℓ, other choices of Γ might be natural, too. For example, if one wants to decide subsumption between compound EL concepts C and D relative to an ELHI ontology OS without resorting to concept names, then one can approximate OS in EL relative to the set Γ of subconcepts of C and D and then check whether OT entails C D. While this is clearly not efficient in practice, it raises the interesting question of how to identify sets Γ that are tailored towards the actual application of an ontology.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

We now briefly discuss the case in which the restriction ( ) is dropped. One can prove that we then need to extend Points 1 to 4 of Theorem 3 with the following:

5. all CIs r. s.C C such that OS |= r s , func(s) OS, and C is a subconcept of OS or an EL(Σ) concept of depth bounded by ℓ; 6. all CIs s. r.C C such that OS |= r s , func(s ) OS, and C is a subconcept of OS or an EL(Σ) concept of depth bounded by ℓ.

However, this is still not sufficient to obtain a complete approximation. Consider the ELHI ontology

OS = {A r1. r2.(B s. ), s r1, s r 2 , func(r 1 ), func(r 2 )}.

It can be verified that OS |= A B. However, it can also be proved that even when OT is the set of all statements from Points 1 to 6 with ℓ= 0, OT |= A B. It remains open whether a transparent (non-projective) approximation is possible when ( ) is dropped.

4 Unbounded Approximation

We provide a significant extensions of Theorem 3 for the case of unbounded approximations, using an entirely different strategy for the completeness proof. In particular, we do not assume the ( ) restriction adopted in Theorem 3, admit inverse roles also in concepts, and add general role inlusions both to the source and target DL, that is, we consider ELRIF -to-ELR approximation. There is a small price that we have to pay for this generality: the approximations constructed here are projective as for every role name from the original ontology, they contain a (potentially fresh) role name that represents its inverse. It is remarkable that this rather mild form of projectiveness overcomes several problems from the purely non-projective case. An ELRIF ontology O is inverse closed, that is, for every role name r in O, there is a role name ˆr such that O contains r ˆr and ˆr r . We provide non-projective approximations under the assumption that the source ontology is inverse closed. This also yields projective approximations for source ontologies that are not inverse closed because we can first extend OS with the required role names ˆr and then approximate. Note that in practice, there are relevant examples of ontologies that are inverse closed such as Galen. If our source is inverse closed, we can further assume that there are no other occurrences of inverse roles in OS, neither in concept inclusions nor in other role inclusions. In other words, our source ontology is formulated in ELRIF .

Theorem 4 Let OS be an inverse closed ELRIF ontology and Σ = sig(OS). Define OT to be the ELR ontology that contains for all EL(Σ) concepts C, D:

1. all CIs in OS; 2. all RIs r s with OS |= r s, r, s Σ role names; 3. all RIs r1 rn r and ˆrn ˆr1 ˆr such that r1 rn r OS with n 2; 4. all CIs C r.D r.(D ˆr.C);

5. all CIs r.C r.D r.(C D) such that func(r) OS; 6. all CIs r. ˆr.C C such that func(ˆr) OS. Then OT is an ELR approximation of OS. Note that Points 1 to 3 essentially take over the part of OS 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 inverse roles. Points 4 to 6 all introduce infinitely many CIs. Via Lemma 2, Theorem 4 also yields projective approximations for the Horn-SRIF-to-ELR case. The following example shows that the CIs in Point 5 of Theorem 3, which unlike Point 5 of Theorem 4 mix functional roles and role inclusions, are implied by the ontology OT constructed in Theorem 4. The example also illustrates the strength of the inverse closed property. Example 3 Let r1 s, r2 s, func(s) OS, and let C1, C2 be EL-concepts. We aim to show that

OT |= r1.C1 r2.C2 r1.(C1 C2).

Due to Points 2 and 5 in Theorem 4, it suffices to show that

OT |= s.Ci ri. ri.Ci for i {1, 2}.

This CI, in turn, can be proved from OT as follows:

OT |= s.Ci ri. ri.( ˆri. s.Ci) (Point 4) ri.( ˆs. s.Ci) (ˆri ˆsi OT by Point 2) ri.( Ci) (Point 6).

It is straightforward to show that the ontology OT from Theorem 4 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) [Jackson, 2004; Sofronie-Stokkermans, 2017; Kikot et al., 2017]. Roughly speaking, 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 in the original ontology, with EL concepts.

5 Inverse Roles in Concept Inclusions As discussed before Theorem 4, the approximations provided by that theorem also cover the case where inverse roles are admitted in concept inclusions. This is achieved, however, by first making the ontology inverse closed and then dropping inverse roles from CIs. Here, we investigate alternative approaches in the basic case of ELI -to-EL , both nonprojectively and projectively, in the latter case using a wellknown normal form for ELI ontologies that avoids syntactic nesting [Baader et al., 2017]. A key to constructing non-projective approximations is the observation that concepts of the form r .C can be used as a marker that is invisible to EL . Example 4 Let OS = {A s . , r . s . s . , s . B}. Then OS |= C C for all EL concepts C, C where C is obtained from C by decorating with

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

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 [Konev et al., 2018]). We now give a non-projective approximation that captures the effect demonstrated in Example 4. For an ELI ontology OS, let cl EL(OS) denote the set of all EL concepts that can be obtained by starting with a subconcept of a concept from OS and then replacing every subconcept of the form r .D with . Let C be an EL concept. An EL concept C is a cl EL(OS) decoration of C if it can be obtained from C by conjunctively adding concepts from cl EL(OS) to a single occurrence of a subconcept in C.

Theorem 5 Let OS be an ELI ontology and Σ = sig(OS). Define OT to be the EL ontology OT that contains for all EL(Σ) concepts C: 1. all CIs C C such that OS |= C C , C a cl EL(OS) decoration of C; 2. all CIs C such that OS |= C . Then OT is an EL approximation of OS.

We prove completeness by a chase based approach. The CIs in Theorem 5 are rather different from those that we have used in Sections 3 and 4 to deal with inverse roles. Being much less constrained, they provides less guidance for constructing approximations in practice. We next observe that we can get back to the more constrained CI scheme for inverse roles by assuming the source ontology OS to be in normal form, that is, all CIs in OS have one of the forms A1, A1 , A1 ρ.A2, ρ.A1 B, and A1 An B where A1, . . . , An, B range over concept names and ρ ranges over roles. Every ELI ontology OS can be converted into an ELI ontology O S in normal form in linear time such that O S is a conservative extension of OS [Baader et al., 2017]. Clearly, any approximation of O S is then a projective approximation of OS. Theorem 6 Let OS be an ELI ontology in normal form, Σ = sig(OS), and ℓ N {ω} a depth bound. Define OT to be the EL ontology OT that contains: 1. all CIs from OS that are of the form A, A , r.A B, or A r.B,; 2. all CIs A1 An B such that OS |= A1 An B, A1, . . . , An, B NC occur in OS; 3. all CIs A r.C r.(C B) such that r .A B OS and C is an EL(Σ) concept of depth bounded by ℓ 1. Then OT is an ℓ-bounded EL appoximation of OS. It is straightforward to verify that OT is sound. To prove completeness, we again use a chase based strategy.

6 Size of Approximations We prove that finite approximations are not guaranteed to exist and that depth bounded approximations can be nonelementary 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 also for

most ontologies that occur in practical applications, neither finite (complete) approximations nor depth bounded (complete) approximations of elementary size can be expected. We focus on the cases ELIH-to-ELH, ELHF-to-ELH, and ELHI-to-ELH, starting with unbounded approximations. Theorem 7 None of the ontologies

{ r .A B}, {func(r), A A}, {r s , A A}

has finite projective ELH approximations. To get an idea of the proof, consider OS = { r .A B} and let OT be a projective ELH approximation of OS. For all n 0, let Cn = rn. , where rn denotes n-fold nesting of an existential restriction, and observe that

OS |= A r.Cn r.(B Cn).

To establish the desired result, we prove that for every n 0, there is a subconcept Mn of OT such that OT |= Mn Cn and OT |= Mn Cm for any m > n. 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, ˆA1, . . . , An, ˆAn}.

Theorem 8 Let n 0 and let On be the union of Γn with any of the following sets:

{ r .A B}, {func(r), A A}, {r s , A A}

For every ℓ 1, any ℓ-bounded projective ELH approximation OT of On must be of size at least tower(ℓ, n).

7 Conclusion It remains an open problem to develop informative nonprojective approximations for (unrestricted) ELHIF -to ELH or even for Horn-SHIF-to-ELH and Horn SRIF-to-ELR . It would also be interesting to further extend the expressive power of both the source and target DLs. For example, nominals and range restrictions could be added even without compromising tractability of the latter [Baader et al., 2005]. We remark that Theorem 4 can be adapted to the extension ELRdr of ELR with range restrictions as the target DL by additionally including in OT the range restriction ran(r) ˆr. for every role name r in OS. Once more, inverse closedness pays off here as a corresponding extension of Theorem 3 appears to be more challenging. There are many other relevant approximation cases that we did not touch upon, including the approximation of non-Horn DLs such as ALC, SHIQ, and SROIQ in (tractable and intractable) Horn DLs. It would further be of interest to understand how approximations can be better tailored towards relevant applications, for example in the spirit of choosing a set Γ of relevant concepts as discussed in Section 3.

Acknowledgements B otcher and Lutz were supported by DFG CRC 1320 Ease.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

References [Baader et al., 2005] Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope. In Proc. of IJCAI, pages 364 369. Morgan Kaufmann, 2005. [Baader et al., 2008] Franz Baader, Carsten Lutz, and Sebastian Brandt. Pushing the EL envelope further. In Proc. of OWLED, volume 496 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. [Baader et al., 2017] Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. [Beklemishev, 2014] Lev D. Beklemishev. Positive provability logic for uniform reflection principles. Ann. Pure Appl. Logic, 165(1):82 105, 2014. [Bienvenu et al., 2016] Meghyn Bienvenu, Peter Hansen, Carsten Lutz, and Frank Wolter. First order-rewritability and containment of conjunctive queries in Horn description logics. In Proc. of IJCAI, pages 965 971. AAAI Press, 2016. [Blackburn et al., 2001] Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001. [Botoeva et al., 2010] Elena Botoeva, Diego Calvanese, and Mariano Rodriguez-Muro. Expressive approximations in DL-Lite ontologies. In Proc. of AIMSA, pages 21 31. Springer, 2010. [Brandt et al., 2002] Sebastian Brandt, Rralf K usters, and Anni-Yasmin Turhan. Approximation and difference in description logics. In Proc. of KR, pages 203 214. Morgan Kaufman, 2002. [Carral et al., 2014] David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler, and Ian Horrocks. EL-ifying ontologies. In Proc. of IJCAR, pages 464 479, 2014. [Darwiche and Marquis, 2002] Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17(1):229 264, 2002. [Goldblatt, 1989] R. Goldblatt. Varieties of complex algebras. Ann. Pure Appl. Logic, 44(3):173 242, 1989. [Groot et al., 2005] Perry Groot, Heiner Stuckenschmidt, and Holger Wache. Approximating description logic classification for semantic web reasoning. In Proc. of ESWC, pages 318 332. Springer, 2005. [Jackson, 2004] Marcel Jackson. Semilattices with closure. Algebra Universalis, 52(1):1 37, 2004. [Kikot et al., 2017] Stanislav Kikot, Agnes Kurucz, Yoshihito Tanaka, Frank Wolter, and Michael Zakharyaschev. Kripke completeness of strictly positive modal logics over meet-semilattices with operators. Co RR, abs/1708.03403, 2017. [Konev et al., 2016] Boris Konev, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Conservative rewritability of description logic TBoxes. In Proc. of IJCAI, pages 1153 1159. AAAI Press, 2016.

[Konev et al., 2018] Boris Konev, Carsten Lutz, Ana Ozaki, and Frank Wolter. Exact learning of lightweight description logic ontologies. J. Mach. Learn. Res., 18(201):1 63, 2018. [Kontchakov and Zakharyaschev, 2014] Roman Kontchakov and Michael Zakharyaschev. An introduction to description logics and query rewriting. In Proc. of RW, volume 8714 of LNCS, pages 195 244. Springer, 2014. [Kr otzsch et al., 2013] Markus Kr otzsch, Sebastian Rudolph, and Pascal Hitzler. Complexities of Horn description logics. ACM Trans. Comput. Log., 14(1):2:1 2:36, 2013. [Lutz and Wolter, 2010] Carsten Lutz and Frank Wolter. Deciding inseparability and conservative extensions in the description logic EL. J. Symb. Comput., 45(2):194 228, 2010. [Lutz et al., 2011] Carsten Lutz, Robert Piro, and Frank Wolter. Description logic TBoxes: Model-theoretic characterizations and rewritability. In Proc. of IJCAI, pages 983 988. IJCAI/AAAI, 2011. [Lutz et al., 2012] Carsten Lutz, Inanc Seylan, and Frank Wolter. An automata-theoretic approach to uniform interpolation and approximation in the description logic EL. In Proc. of KR, pages 286 296. AAAI Press, 2012. [Pan and Thomas, 2007] Jeff Z. Pan and Edward Thomas. Approximating OWL-DL ontologies. In Proc. of AAAI, pages 1434 1439. AAAI Press, 2007. [Ren et al., 2010] Yuan Ren, Jeff Z. Pan, and Yuting Zhao. Soundness preserving approximation for TBox reasoning. In Proc. of AAAI, pages 351 356. AAAI Press, 2010. [Schaerf and Cadoli, 1995] Marco Schaerf and Marco Cadoli. Tractable reasoning via approximation. Artificial Intelligence, 74(2):249 310, 1995. [Selman and Kautz, 1996] Bart Selman and Henry A. Kautz. Knowledge compilation and theory approximation. J. ACM, 43(2):193 224, 1996. [Sofronie-Stokkermans, 2013] Viorica Sofronie Stokkermans. Locality and applications to subsumption testing in EL and some of its extensions. Sci. Ann. Comp. Sci., 23(2):251 284, 2013. [Sofronie-Stokkermans, 2017] Viorica Sofronie Stokkermans. 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. [van Benthem, 1984] Johan van Benthem. Correspondence theory. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 2, pages 167 247. Reidel, Dordrecht, 1984.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)