Despite prominent standardization efforts such as OWL, a large variety of description logics (DLs) continues to be used as ontology languages. In fact, ontology designers choose a DL suitable for their purposes based on many factors including expressive power, computational properties, and tool support [1]. Since ontology engineering frequently involves (partial) reuse of existing ontologies, this raises the problem of converting an ontology written in some source DL L S into a desired target DL L T . A particularly important case is ontology approximation where L T is a fragment of L S , studied for example in [2,3,5,10,11,12] In practice, ontology approximation is often done in an ad hoc way by dropping all statements from the source ontology O S that are not expressible in L T , or at least the inexpressible parts thereof. It is well-known that this results in incomplete approximations, that is, there will be knowledge in O S that could be expressed in L T , but is not entailed by the resulting approximated ontology. The degree and nature of the resulting incompleteness is typically neither understood nor analyzed. One reason for this unsatisfactory situation might be the fact that it is by no means easy to construct complete approximations and, even worse, finite complete approximations are not guaranteed to exist. This was studied in depth in [2] where ontologies formulated in expressive Horn DLs such as Horn-SHIF and ELI are approximated in tractable Horn DLs such as EL. For example, it is shown there that finite complete ELI-to-EL approximations do not exist even in extremely simple cases that frequently occur in practice. This gives rise to a new research agenda for ontology approximation that consists in mapping out the structure of complete infinite ontology approximations to guide informed decisions when manually constructing incomplete finite approximations in practice. It also enables a better understanding of the degree and nature of incompleteness.

In the paper that this abstract reports about [7,8], we consider L S -to-L T ontology approximation where L S is a non-Horn DL such as ALC and L T is a tractable Horn DL such as EL. We believe that these are extremely natural cases of ontology approximation, given that Horn vs. non-Horn is nowadays the most important classification criterion for DLs [1]. Non-Horn DLs include expressive features such as negation and disjunction and require 'reasoning by cases' which is computationally costly, but also have considerably higher expressive power than Horn DLs. Horn DLs, in contrast, enjoy favourable properties such as the existence of universal models and of 'consequence-based' reasoning algorithms that avoid reasoning by cases [6]. It turns out, though, that non-Horn-to-Horn approximation is a challenging endeavour.

We start with the fundamental case of ELU-to-EL approximation. Given an ELU ontology O S , we aim to find a (potentially infinite) EL ontology O T such that for all EL concepts C, D in the signature of The last two lines of O T illustrate that EL consequences of ELU ontologies can be rather non-obvious.

We first prove that finite approximations need not exist in the ELU-to-EL case and that depth bounded approximations may be non-elementary in size. Our main result is then a concrete approximation scheme that makes explicit the structure of complete infinite approximations and aims to keep as much structure of the source ontology as possible. An interesting and, given the results in [2], surprising feature of our scheme is that it can be expected to often deliver finite approximations in practical cases. We perform a case study based on the Manchester ontology corpus that confirms this expectation. We also show that if O S is an acyclic ELU ontology, then a finite EL approximation always exists (though it need not be acyclic).

We then proceed to the cases of ELU ⊥ -to-EL ⊥ and ALC-to-EL ⊥ approximations which turn out to be closely related to each other. They also turn out to be significantly different from the ELU-to-EL case in that finite approximations do not exist in extremely simple (and practical) cases, much like in the Horn approximation cases studied in [2]. Also, finite approximations of acyclic ontologies are no longer guaranteed to exist. While this is not good news, it is remarkable that the addition of the ⊥ symbol to the source DL has such a dramatic effect. We again provide an (infinite) approximation scheme.

Finally, we propose a notion of approximation that is tailored towards applications in ontology-mediated querying [4] and show that it is intimately related to the subsumption-based approximations that we had studied before. Remarkably, if we concentrate on atomic queries (AQs), then we obtain finite approximations even in the ALC-to-EL ⊥ case. Compared to the related work presented in [9], we do not require the preservation of all query answers, but only of a maximal subset thereof, and our method is applicable to all ontologies formulated in the source DL chosen rather than to a syntactically restricted class. We also observe an interesting application to the rewritability of ontology-mediated queries OMQ, that is, we use our results to prove that it is decidable wether an OMQ from the OMQ language (ALC, ALCQ) is rewritable into an equivalent OMQ from the language (EL ⊥ , AQ). Here, ALCQ denotes the query language that consists of all ALC concepts and AQ denotes the class of atomic queries of the form A(x).