Ontology Approximation in Horn Description Logics

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 fromOS 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 OT must be formulated in Σ (non-projective approximation) and the case that additional symbols are admitted (projective approximation).

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

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 ontology 2 , slightly simplified for presentation purposes. Let PathoPhen stand for "pathological phenomenon", isConOf for "is consequence of", and hasCon 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 ⊑ PathoPhen ⊓ ∃hasCon.ClammySkin ∃isConOf.PathoPhen ⊑ PathoPhen ∃hasCon.PathoPhen ⊑ PrecipitatingFactor hasCon ⊑ isConOf-.

These imply as a consequence

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

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 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.

2 http://www.opengalen.org/

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 BioPortal 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-LiteF is presented in [Pan and Thomas, 2007] and complete (projective) approximations of SROIQ ontologies in DL-LiteA are given in [Botoeva et al., 2010]. Such approximations are guaranteed to exist due to the limited expressive power of DL-LiteA. 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

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 ⊥.

We briefly introduce the relevant fragments of HornSRIF, 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 HornSRIF ontology in which both the left- and 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 HornSRIF introduced above. A (potentially infinite) LT ontology OT is an LT approximation of OS if

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

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

∃reportsTo.∃hasSupervisorn .⊤ ⊓ ∃reportsTom.⊤ ⊑ ∃reportsTo.(∃hasSupervisorn .⊤ ⊓ ∃reportsTom-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. ⋃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 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 fromOS;
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 fromOS.

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 fromOS;
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 fromOS;
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.

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:

1. 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 ℓ;
2. 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

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;

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

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

This CI, in turn, can be proved fromOT as follows:

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 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 clEL(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 clEL(OS) decoration of C if it can be obtained from C by conjunctively adding concepts from clEL(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 clEL(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

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

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:

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⊥-toELH⊥ or even for Horn-SHIF-to-ELH⊥ and HornSRIF-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.