Debugging incoherent ontology by extracting a clash module and identifying root unsatisfiable concepts

The calculation of minimal incoherence-preserving sub-TBox (MIPS) is an important task in incoherent ontology debugging. Existing approaches to this task are inefficient when debugging large incoherent ontology with a lot of unsatisfiable concepts. To resolve the problem, we first extract a clash module from the ontology and then identify the root unsatisfiable concepts from the clash module. Afterward, the minimal unsatisfiability-preserving sub-TBox (MUPS) of each root unsatisfiable concept can be calculated on the basis of the clash module. We have proved that the MIPS of an incoherent ontology is equal to the union of the MUPSes of the root unsatisfiable concepts. Our approach can successfully avoid calculating a considerable number of MUPSes irrelevant to the MIPS. Experiments with a variety of test ontologies show that the proposed approach of calculating MIPS is efficient and practical.