We present a method to compute uniform interpolants with fixpoints for ontologies specified in the description logic ALC. The aim of uniform interpolation is to reformulate an ontology such that it only uses a specified set of symbols, while preserving consequences that involve these symbols. It is known that in ALC uniform interpolants cannot always be finitely represented. Our method computes uniform interpolants for the target language ALCμ, which is ALC enriched with fixpoint operators, and always computes a finite representation. If the result does not involve fixpoint operators, it is the uniform interpolant in ALC. The method focuses on eliminating concept symbols and combines resolution-based reasoning with an approach known from the area of second-order quantifier elimination to introduce fixpoint operators when needed. If fixpoint operators are not desired, it is possible to approximate the interpolant.
展开▼
