Black Box Techniques for Debugging Unsatisfiable Concepts
Aditya Kalyanpur, Bijan Parsia, Evren Sirin · 2005
Now that OWL is a W3C Recommendation, one can expect that a much wider community of users and developers will be exposed to the expressive description logic SHIF(D) and SHOIN(D) which are the basis of OWL-DL. These users and developers are likely not to have a lot of experience with knowledge representation (KR), much less logic-based KR, much less description logic based KR. For such people, having excellent documentation, familiar techniques, and helpful tools is a fundamental requirement. A ubiquitous activity in programming is debugging, that is, finding and fixing defects in a program. Ontologies too have defects, and a common activity is to find and repair these defects. Unfortunately, the tool and training support for debugging ontologies is fairly weak. 1 We have chosen to focus on debugging unsatisfiable concepts (and contradictory ABoxes) because contradictions, in general, seem analogous to fatal errors in programs. Debugging fatal errors in programs can be relatively straightforward: the program crashes, there is a stack trace or similar information, and (one measure of) success is a running program. Current tools do support indicating the dramatic failure of a unsatisfiable class, and success is similarly clear, however, supporting the diagnosis and resolution of the bug is not supported at all. In [2], we investigated better support for debugging unsatisfiable concepts using both glass box (wherein the reasoner is 1 While, historically, good KR modeling practices have been developed and described, often with an emphasis on description logics[3], tool support for “good ” modeling remains elusive, especially given the lack of consensus on practice and the strong dependence of goodness on application and domain specifics. modified return explanations of the unsatisfiability) and black box (wherein the only inference service is satisfiability checking) techniques. In this paper, we extend our investigation of black box techniques which have two advantages over glass box ones: reasoner independence (you do not need a specialized, explanation generating reasoner) and avoiding the performance penalty of glass box techniques.