As ontologies grow in size and complexity, it becomes ever more important to understand the underlying causes for a consequence followed from an ontology, specially if this consequence is unexpected or unwanted for the representation domain. A usual approach in description logics (DL) is to compute one or all justi cations ; that is, the minimal subontologies that still entail the consequence under consideration. Several approaches have been developed for computing these justi cations. Black-box approaches|which repeatedly call an unmodi ed reasoner|dominate the scene for more expressive DLs, while glassbox approaches modifying the underlying behaviour of the reasoner have been implemented mainly for lightweight DLs only [12]. Recent work has highlighted the importance of approximating the set of all justi cations through two sets: the intersection and union of all justi cations. The intersection (also known as the core) provides a lower approximation, with axioms that are necessary for the entailment. In fact, removing any axiom from the core automatically removes the consequence. The union, on the other hand, yields an upper approximation containing all relevant axioms. That is, as long as one is only interested in the consequence at hand, one can safely ignore all the axioms that do not belong to this union. In other words, this union is the smallest possible justi cation-preserving module. There is, to date, a lack of approaches for computing these upper and lower approximations, specially in the case of the union of justi cations, which has an underlying computationally-hard task. We ll this gap by presenting new methods for computing the core and the union of justi cations. Core. The algorithm for computing the core follows a simple black-box approach based on the notion of necessity. In essence, an axiom is necessary (and hence belongs to the core) if and only if removing it from the ontology means getting rid of the consequence. Our algorithm simply checks necessity of by calling a reasoner with the ontology minus f g: if the consequence does not ? Jieying Chen is supported by the SIRIUS centre, which is funded by the Norwegian Research Council, project number 237898 and is co-funded by its partner companies. Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
hold anymore, the is added to the core. This approach requires one entailment
test for each axiom, and thus incurs in a linear overhead over standard reasoning.
To avoid unnecessary checks, we run the algorithm over a justi cation-preserving
module [
Union of all Justi cations. We introduce two algorithms for computing
the union of all justi cations. The rst one is a black-box approach inspired
by Reiter's Hitting Set Tree algorithm [
The second algorithm reduces the problem of computing the union of all
justi cations to a related problem over propositional formulas, through three main
steps. First, we compute a CNF formula using the consequence-based reasoner
condor [
Proposition 1. Let Just(O; ) be the set of all justi cations for the GCI w.r.t. the ontology O. If S is the set of all smallest minimal hitting sets for Just(O; ), then fO n S j S 2 Sg is the set of all optimal repairs for O j= .
Specially, if the core is not empty, a smallest minimal hitting set for all
justi cations is a singleton set that contains only one axiom from the core.
Evaluation. We built a prototypical implementation to evaluate the
performance of our algorithms in real-world ontologies. The black-box algorithm uses
the OWL API [
min max mean median
Note that in terms of computational complexity computing the core and one justi cation are equally hard problems. But the black-box method for the latter should intuitively be faster than the former as it reduces the size of the ontology throughout the execution. Indeed, the latter method removes all unnecessary axioms, while the former always calls the reasoner with the original ontology minus one axiom. Our experiments tend to con rm this view, as shown in Table 1.
To evaluate the computation of the union of justi cations, we compared against the canonical approach of nding all justi cations and our approach on computing the union. Figure 1 plots the logarithmic computation time of the union (in the vertical axis) of each test instance (in the horizontal axis). Each blue, green or red dot corresponds to the computation time of the union by OWL API, the black-box algorithm or the MUS-MEM algorithm for a conclusion respectively. In our experiments, our black-box approach clearly outperformed the MUS-based translation and the enumeration of justi cations.
In the end, we also analysed the proportional sizes of cores, justi cations, and unions of justi cations. Interestingly, 85% of the test instances have only one justi cation, and even among the others, 84% of cores are non-empty, which means that we could be able to use core to compute the set of all optimal repairs for most cases. In general, the size of the union tends not to be much larger than that of the core.
Conclusion In this paper, we presented algorithms for computing the core and the union of all justi cations for a given DL consequence. As an application, we study how to compute optimal repairs e ectively, through the information provided by the core and the union of all justi cations.
In the future, we plan to further detailed analyse the experimental results and provide better insights to explain the results that we have shown in the evaluation. Currently, the MUS-based approach for computing the union of all justi cations only supports ALC ontologies. However, we would expect that this approach could be further generalised to more expressive languages.