Practical Forgetting and Uniform interpolation for Description Logics

Forgetting, and the dual task of computing uniform interpolants,
minimally restricts an ontology to a given set of concept and role
symbols in such a way that consequences involving these symbols are
preserved. This makes forgetting/uniform interpolation a useful tool for
knowledge extraction, ontology analysis, ontology debugging and information
hiding. Given the importance for all these applications,
forgetting/uniform interpolation has recently gained a lot of attention
in the description logic and knowledge representation literature.
Previous work devised methods for Horn description logics (such
as DL-Lite and EL) and for concept symbol elimination of ALC ontologies.
In recent work we have developed a new method for computing uniform
interpolants for a large number of more expressive description logics
with the advantage that it can eliminate both concept and role symbols
and can handle ontologies that include ABox statements (facts). We have
also shown how second-order quantifier elimination techniques can be
used to tackle these problems for yet more expressive description
logics.  Experiments on a large number of ontologies from real-world
applications have shown both methods are practical.

This is joint work with Patrick Koopmann and Yizheng Zhao.