Towards Practical Uniform Interpolation and Forgetting for ALC TBoxes.
Michel Ludwig, Boris Yur'evich Konev · 2013
Abstract We develop a clausal resolution-based approach for computing uniform interpolants of TBoxes formulated in the description logic ALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and its applications to concept forgetting, ontology obfuscation and logical difference on real-life ALC ontologies. Our results indicate that in many practical cases a uniform interpolant exists and can be computed with the presented algorithm. 1