Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach

We present a method for forgetting concept symbols in ontologiesspecified in the description logic ALCOI. The method is anadaptation and improvement of a second-order quantifier eliminationmethod developed for modal logics and used for computing correspondenceproperties for modal axioms. It follows an approach exploiting aresult of Ackermann adapted to description logics. An important featureinherited from the modal approach is that the inference rules are guidedby an ordering compatible with the elimination order of the concept symbols.This provides more control over the inference process and reducesnon-determinism, resulting in a smaller search space. The method is extendedwith a new case splitting inference rule, and several simplificationrules. Compared to related forgetting and uniform interpolation methodsfor description logics, the method can handle inverse roles, nominals andABoxes. Compared to the modal approach on which it is based, it is moreefficient in time and improves the success rates. The method has beenimplemented in Java using the OWL API. Experimental results showthat the order in which the concept symbols are eliminated significantlyaffects the success rate and efficiency.