Saturation-Based Forgetting in the Description Logic SIF

Forgetting, which has also been studied under the namesuniform interpolation, projection and variable elimination, deals withthe elimination of symbols from an input ontology in such a way thatall entailments in the remaining signature are preserved. The computedresult, the uniform interpolant, can be seen as a restricted view of theoriginal ontology, projected to a specified subset of the signature. Forgettinghas applications in ontology reuse, ontology analysis and informationhiding, and has been studied for a variety of description logics inthe last years. However, forgetting in description logics with functionalrole restrictions and inverse roles has been an open problem so far. Inthis paper, we study the problem of forgetting concept symbols in thedescription logic SIF, an expressive description logic supporting transitiveroles, inverse roles and functional role restrictions. Saturation-basedreasoning has been proven to be a well-suited technique for computinguniform interpolants practically in recently introduced methods. Sinceexisting methods are usually optimised towards a specific aim such assatisfiability checking or classification, they cannot always directly beused for forgetting. In this paper we present a new saturation techniquethat is complete for forgetting concept symbols, and show how it can beused for computing uniform interpolants.