This tutorial discusses resolution-based methods for computing uniform interpolants in various expressive description logics (DLs) and their implementations, and their relations to second-order quantifier elimination. DLs [1] are fragments of first-order logic used to define terminological knowledge in form of ontologies, using a set of unary and binary predicates called concept and role names, which form the signature of the ontology. Forgetting a set of given concept and role names from an ontology means computing a new ontology that does not use these concept and role names, but preserves all logical entailments of the original ontology over the remaining signature. The resulting ontology is then a uniform interpolant of the original ontology for the remaining signature. There is a range of applications for uniform interpolants, such as for ontology reuse, ontology analysis, or computing logical differences. Theoretical results on uniform interpolation seem discouraging. In most known DLs, uniform interpolants do not always exist, and already the problem of deciding whether a uniform interpolant exists for a given ontology and signature is ExpTime-complete for the Horn DL E L [7], and 2ExpTime-complete for the expressive DL ALC [8]. Moreover, in both DLs, uniform interpolants have in the worst case a size that is triple-exponential in the size of the input ontology [9,8]. The former problem can be solved by computing uniform interpolants in DLs that have fixpoint operators, which often ensures that uniform interpolants do always exist. Regarding the size of the uniform interpolants, experiments indicate that the worst-case rarely occurs with real-life ontologies, and that uniform interpolants are in most cases not larger than the original ontology. However, due to the high worst case complexity, the practical computation of uniform interpolants in expressive DLs requires dedicated and goal-oriented procedures. Forgetting and uniform interpolation are similar to second-order quantifier elimination in the sense that the goal is to eliminate predicates from a logical formulae, while preserving logical entailments in the remaining signature. However, while the result of second-order quantifier preserves all second-order entailments of the original formula, uniform interpolants only preserve entailments that can be expressed in the DL at hand. Despite these differences, the similarity to second-order quantifier elimination motivates the use of similar techniques for computing uniform interpolants. This tutorial presents such an approach, which is based on the idea of computing relevant entailments using resolution. For this, it uses a resolution-based calculus that was first presented in [2] for the DL ALC, and later extended to more expressive DLs such as SHQ [3] and SIF [5], as
well as to knowledge bases with ABoxes [