@INPROCEEDINGS{KoopmannSchmidt15b,
AUTHOR = {Koopmann, P. and Schmidt, R. A.},
YEAR = {2015},
TITLE = {Saturation-Based Forgetting in the Description Logic {$\mathcal SIF$}},
EDITOR = {Calvanese, D. and Konev, B.},
BOOKTITLE = {Proceedings of the 28th International Workshop on Description Logics (DL-2015)},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {1350},
PUBLISHER = {CEUR-WS.org},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/KoopmannSchmidt15b.html},
ABSTRACT = {
Forgetting, which has also been studied under the names
uniform interpolation, projection and variable elimination, deals with
the elimination of symbols from an input ontology in such a way that
all entailments in the remaining signature are preserved. The computed
result, the uniform interpolant, can be seen as a restricted view of the
original ontology, projected to a specified subset of the signature. Forgetting
has applications in ontology reuse, ontology analysis and information
hiding, and has been studied for a variety of description logics in
the last years. However, forgetting in description logics with functional
role restrictions and inverse roles has been an open problem so far. In
this paper, we study the problem of forgetting concept symbols in the
description logic SIF, an expressive description logic supporting transitive
roles, inverse roles and functional role restrictions. Saturation-based
reasoning has been proven to be a well-suited technique for computing
uniform interpolants practically in recently introduced methods. Since
existing methods are usually optimised towards a specific aim such as
satisfiability checking or classification, they cannot always directly be
used for forgetting. In this paper we present a new saturation technique
that is complete for forgetting concept symbols, and show how it can be
used for computing uniform interpolants.
}
}