Visualizing proofs and the modular structure of ontologies to support ontology repair

The classical approach for repairing a Description Logic (DL) ontology in the sense of removing an unwanted consequence is to delete a minimal number of axioms from the ontology such that the resulting ontology no longer has the consequence. While there are automated tools for computing all possible such repairs, the user still needs to decide by hand which of the (potentially exponentially many) repairs to choose. In this paper, we argue that exploring a proof of the unwanted consequence may help us to locate other erroneous consequences within the proof, and thus allows us to make a more informed decision on which axioms to remove. In addition, we suggest that looking at the so-called atomic decomposition, which describes the modular structure of the ontology, enables us to judge the impact that removing a certain axiom has. Since both proofs and atomic decompositions of ontologies may be large, visual support for inspecting them is required. We describe a prototypical system that can visualize proofs and the atomic decomposition in an integrated visualization tool to support ontology debugging.