Uniform Interpolation of ALC-Ontologies Using Fixpoints

Koopmann, P. and Schmidt, R. A. (2013)

In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102. BiBTeX, PDF (final version available via DOI link to Springer).

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 ALCmu, 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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 23 Sep 13
Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk