Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$-Ontologies

Abstract

We propose a method for forgetting concept symbols and non-transitive roles symbols of $\mathcal{SHQ}$-ontologies, or for computing uniform interpolants in $\mathcal{SHQ}$. Uniform interpolants restrict the symbols occuring in an ontology to a specified set, while preserving all logical entailments that can be expressed using this set in the description logic under consideration. Uniform interpolation has applications in ontology reuse, information hiding and ontology analysis, but so far no method for computing uniform interpolants for expressive description logics with number restrictions has been developed. Our results are not only interesting because they allow to compute uniform interpolants of ontologies using a more expressive language. Using number restrictions also allows to preserve more information in uniform interpolants of ontologies in less complex logics, such as $\mathcal{ALC}$ or $\mathcal{EL}$. The presented method computes uniform interpolants on the basis of a new resolution calculus for $\mathcal{SHQ}$. The output of our method is expressed using $\mathcal{SHQ}\mu$, which is $\mathcal{SHQ}$ extended with fixpoint operators, to always enable a finite representation of the uniform interpolant. If the uniform interpolant uses fixpoint operators, it can be represented in $\mathcal{SHQ}$ without fixpoints operators using additional concept symbols or by approximation.