Abstract:
We present a framework for the debugging of logically contradicting terminologies, which is based on traditional model-based diagnosis. To study the feasibility of this highly general approach we prototypically implemented the hitting set algorithm presented in (Reiter 1987), and applied it in three different scenarios. First, we use a Description Logic reasoning system as a black-box to determine (necessarily maximal) conflict sets. Then we use our own non-optimized DL reasoning engine to produce small, and a specialized algorithm to determine minimal conflict sets. In a number of experiments we show that the first method already fails for relatively small terminologies. However, based on small, or minimal conflict sets, we can often calculate diagnoses in reasonable time.