Resolution Based Uniform Interpolation for Expressive Description Logics

Ontologies represented using description logics model domains of interest in terms of concepts and binary relations, and are used in a range of areas including medical science, bio-informatics, semantic web or artificial intelligence. Often, ontologies are large and complex and cover 10,000s of concepts. Uniform interpolants are restricted views of ontologies, that only use a specified set of symbols, while preserving all entailments that can be expressed using these symbols. Uniform interpolation can be used for analysing hidden relations in an ontology, removing confidential concepts from an ontology, computing logical differences between ontologies or extracting specialised ontologies for ontology reuse and has many more applications.

We follow a resolution-based approach to make the computation of uniform interpolants of larger ontologies feasable. Uniform interpolants cannot always be represented finitely in the language of the input ontology, for which situation we offer three solutions: extending the signature with additional concepts, approximating the uniform interpolant, or using fixpoint operators.