Count and forget: Uniform interpolation of SHQ-ontologies

Abstract. We propose a method for forgetting concept symbols and non-transitive roles symbols of SHQ-ontologies, or for computing uni-form interpolants in 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 inter-esting 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 ALC or EL. The presented method computes uni-form interpolants on the basis of a new resolution calculus for SHQ. The output of our method is expressed using SHQµ, which is 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 SHQ without fixpoints operators using additional concept symbols or by approximation.