B.: Towards practical uniform interpolation and forgetting for ALC TBoxes

Abstract We develop a clausal resolution-based approach for computing uni-form interpolants of TBoxes formulated in the description logicALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and its applications to concept forgetting, ontology obfuscation and lo-gical difference on real-life ALC ontologies. Our results indicate that in many practical cases a uniform interpolant exists and can be computed with the presen-ted algorithm.