@INPROCEEDINGS{KoopmannSchmidt13a,
AUTHOR = {Koopmann, P. and Schmidt, R. A.},
YEAR = {2013},
TITLE = {Uniform Interpolation of $\mathcal{ALC}$-Ontologies Using Fixpoints},
EDITOR = {Fontaine, P. and Ringeissen, C. and Schmidt, R. A.},
BOOKTITLE = {Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {8152},
PUBLISHER = {Springer},
PAGES = {87-102},
DOI = {http://dx.doi.org/10.1007/978-3-642-40885-4_7},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/KoopmannSchmidt13a.html}},
ABSTRACT = {
We present a method to compute uniform interpolants with fixpoints for
ontologies specified in the description logic $\mathcal{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 $\mathcal{ALC}$ uniform interpolants cannot
always be finitely represented. Our method computes uniform interpolants
for the target language $\mathcal{ALC}\mu$, which is $\mathcal{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 $\mathcal{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.
}
}