Finding maximally satisfiable terminologies for the description logic ALC

Abstract

For ontologies represented as Description Logic Tboxes, op-timised DL reasoners are able to detect logical errors, but there is comparatively limited support for resolving such problems. One possible remedy is to weaken the available in-formation to the extent that the errors disappear, but to limit the weakening process as much as possible. The most obvi-ous way to do so is to remove just enough Tbox sentences to eliminate the errors. In this paper we propose a tableau-like procedure for finding maximally concept-satisfiable ter-minologies represented in the description logic ALC. We discuss some optimisation techniques, and report on prelimi-nary, but encouraging, experimental results.