Abstract:Axiom pinpointing has attracted extensive interest for description logics due to its effect of exploring explicable defects in the ontology and searching hidden justifications for the logic consequence. Balancing the expressive power of description logics and the solving efficiency of reasoners has always been the focus of axiom pinpointing research. This study, from both glass-box and black-box perspectives proposed a consequence-based method to computing justifications. The glass-box method uses modified reasoning rules to trace the specific process of inference, and introduces the concept of pinpointing formula to establish the correspondence between the label of Boolean formula and all the minimal axioms sets. The black-box method directly calls the inference engine based on the unmodified reasoning rules, and further uses the HST to compute all justifications for the inference. Two reasoning tools have been designed based on the two axiom pinpointing algorithms for expressive description logics ontologies. Its feasibility is verified theoretically and experimentally, and its solving efficiency is compared with that of existing axiom pinpointing tools.