Knowledge engineering is an error-prone task and the need for automated tools to help correct existing errors has been long recognised. While many ontology repair methods have been proposed, most ignore a fundamental issue: only a domain expert can state whether an ontology reflects the domain knowledge or not. In this paper, we consider an interactive ontology repair procedure where a domain expert guides the system by signalling axioms that are identified as erroneous from sets of suspicious axioms. To avoid overwhelming the human expert with the number and complexity of information requests, we propose methods to reduce the class of potentially suspicious axioms: first, the expert may signal a class of consequences they desire to preserve in the corrected ontology; second, we introduce a new notion of prolificacy to understand the impact axioms have in the derivation of consequences.
Description logics (DLs) [
There are many reasons why knowledge engineering is an error-prone task: experts may disagree on some information, details may be lost in the translation from human expertise to logical formalism, or simply syntactic misunderstandings and typos may occur. The fact is that it is not uncommon to face errors in an ontology. For instance, the Snomed knowledge base was found to entail that every amputation of finger is also an amputation of hand, which is obviously unwanted in the modelled domain. Managing these errors, specially in large ontologies, requires the help of specialised automated tools.
Throughout the last two decades, many methods have been proposed to explain [
To-date, most proposals for selecting one ontology which corrects the observed errors follow an
idea akin to the minimal-change restriction used in belief revision [
While all these methods are adequately motivated and provide some guarantees, they still ignore a fundamental element of error correction: correctness of an ontology—in the sense of its alignment to the knowledge domain it is supposed to represent—is a meta-logical property, and no amount of syntactic or semantic logical manipulation can access this “ground truth.” Indeed, only domain experts can state whether an ontology correctly reflects the domain knowledge or not. Thus, to fully correct an ontology, we cannot escape asking for the expert feedback.
Since human expert access is limited and expensive, ontology repair requires a delicate balance
between automation and interaction. While too much automation may lead to incorrect ontologies,
human experts may at some point be unable to answer too many or too complex requests for feedback.
Indeed, while in theory one could automatically compute all possible repairs and ask the expert to
choose among them, the number of existing solutions makes this approach infeasible in practice. The
goal is then to build an iterative procedure in which a knowledge engineer (henceforth called the user)
is asked a series of questions designed to yield a correct repair. The idea is somehow reminiscent of
iterative ontology completion methods [
The goal of this paper is to devise a technique to reduce the number and size of the sets presented to the user for verification, without first computing all possible repairs. To this end, we propose two complementary techniques to reduce the search space for the “correct” repair. The first is a manual phase, where the user is allowed to provide a class of consequences which must be preserved. These in general refer to well-established, uncontroversial, and clear knowledge from the representation domain, which might be implicitly derivable from the ontology, even if the user does not know exactly from which ontology axioms. Given this information, the class of potentially wrong axioms is reduced, and the potential for deriving an answer that does not align with the domain is diminished.
The second phase is an automated one, which relies on a new notion of prolificacy of axioms. In a nutshell, prolificacy refers to how many consequences depend on the axiom in question. In the spirit of minimal change, most prolific axioms are those that preserve the most original consequences, and hence most desired in a final repair. Interestingly, if restricted to atomic consequences only, prolificacy of all axioms in ontologies from the ℰℒ family is computable in polynomial time. In order to decide how many, and which, prolific axioms to save, we focus on preserving the prolificacy of justifications (see Algorithm 2 for details).
These two phases combined allow us to focus on fewer axioms to present to the user, at each step and in total, and construct a better ordering strategy. We emphasise that for this paper we focus mainly on these pruning strategies, but the overarching goal is to deal with the full iterative repair process. In particular, the pruning phase can be repeated every time that the user has identified an erroneous axiom, to further decrease the number of remaining questions to be asked to them.
We first introduce all the preliminaries needed for understanding the rest of this work. Specifically,
we briefly explain the description logic ℰℒ⊥ as a representative of the ℰℒ family, and the notions of
justifications and repairs.
2.1. The Description Logic ℰℒ⊥
ℰℒ⊥ [
Consider three countable, mutually disjoint sets , , and of individual names, concept names, and role names, respectively. ℰℒ⊥ concepts are built through the grammar rule ::= | ⊤ | ⊥ | ⊓ | ∃., where ∈ and ∈ . The semantics is based on interpretations, which are pairs ℐ = (∆ ℐ , · ℐ ), where ∆ ℐ is a non-empty (potentially infinite) set called the domain, and · ℐ is the interpretation function which maps every individual name ∈ to an object ℐ ∈ ∆ ℐ ; every concept name ∈ to a set ℐ ⊆ ∆ ℐ ; and every role name ∈ to a binary relation ℐ ⊆ ∆ ℐ × ∆ ℐ . This function is extended to arbitrary concepts by setting: ⊤ℐ := ∆ ℐ ; ⊥ℐ := ∅; ( ⊓ )ℐ := ℐ ∩ ℐ ; and (∃.)ℐ := { ∈ ∆ ℐ | ∃ ∈ ℐ .(, ) ∈ ℐ }.
The goal of DLs is to represent the knowledge of a domain in a formal way which allows for automated reasoning. This is achieved by introducing restrictions on the class of interpretations of interest; namely, those which comply with what is known about the knowledge domain.
, are ℰℒ⊥ concepts. A TBox is a finite set of GCIs. An assertion is an expression of the form () or (, ) where is a concept, ∈ , and , ∈ . An ABox is a finite set of assertions. An ontology is a pair = (, ) consisting of an ABox and a TBox . For brevity, we will often use the term axiom to refer generally to GCIs and assertions alike.
and the assertion (, ) if ( ℐ , ℐ ) ∈ ℐ . ℐ is a model of the ABox, TBox, or ontology (represented as ℐ |= ) if it satisfies all the axioms in .
In general, we say that an ontology is consistent if it has a model, and it entails an axiom (written
|= ) if every model of is also a model of {} . It is well known that consistency and entailments
for ℰℒ⊥ ontologies can be decided in polynomial time through consequence-based algorithms which
make implicit consequences explicit [
When dealing with ℰℒ⊥ it is often useful to assume that the ontology axioms are limited to a kind of
normal form. We say that a TBox is in normal form if all GCIs are of one of the forms
⊑ , 1 ⊓ 2 ⊑ , ⊑ ∃.,
∃. ⊑ ,
where , 1, 2 ∈ ∪ {⊤} and ∈ ∪ {⊤, ⊥}. An ABox is in normal form if concept assertions
are atomic (i.e., refer to concept names only). An ontology is in normal form if its TBox and ABox
are both in normal form. It is easy to see that any ontology can be transformed in polynomial time
into another one that preserves the same consequences over the original vocabulary, but is in normal
form [
Ontologies written in ℰℒ⊥ and other variants from the ℰℒ family have been successfully used to represent various application domains, particularly from the biomedical fields. The complexity of these domains, and the simplicity of the language (specially if axioms are presented in normal form), means that real-world ontologies tend to have tens of thousands—or hundreds of thousands—axioms, making the process of constructing them error-prone, and corrections very dificult. Hence techniques for helping understand and correct unwanted consequences have been developed.
Finding the axioms responsible for an error in an ontology among several thousands is infeasible
without the help of some automated deduction tool. In monotonic languages (like all classical DLs
including ℰℒ⊥), this corresponds to a task known as axiom pinpointing; that is, identifying one or all
minimal sub-ontologies that entail the consequence—also known as justifications [
Note that this definition includes justifications for ontology inconsistency, by considering the axiom ⊤ ⊑ ⊥ as the consequence .
Justifications can be seen as means to logically “explain” the consequence by retaining only the
necessary information for deriving it and removing all superfluous knowledge. Yet, justifications are
not unique; in fact, a consequence may have exponentially many justifications w.r.t. a single ontology
(on the size of ) [
If the goal is to get rid of an unwanted consequence, it makes sense to rather consider the notion of a
repair; that is, maximal sub-ontologies which do not entail this consequence [
Definition 3 (repair). Let be an ontology and an axiom such that |= . An ontology ℛ is a repair for w.r.t. if (i) ℛ ⊆ ; (ii) ℛ ̸|= ; and (iii) for all ℛ ⊊ ℛ ′ ⊆ , ℛ ′ |= .
Justifications and repairs are dual not only from a definitorial point of view, but in fact they can be
computed from each other. Indeed, if J is the class of all justifications, then any minimal hitting set of J
is the complement of a repair (also known as a diagnosis). Dually, the minimal hitting sets of the class
of the diagnoses form all the justifications. Moreover, the number of diagnoses and repairs can also
be exponential on the size of the ontology. All these are well-known classical results; see e.g. [
Methods for computing justifications and repairs have been studied over the years, along with techniques for reasoning in the presence of errors or inconsistencies. However, from the point of view of an ontology life-cycle, we cannot be content with using an ontology which is known to contain errors. Rather, we want to correct the ontology for future use. In the next section, we provide a brief overview of existing ontology repair methods.
From the point of view of knowledge engineering, we are not interested in one arbitrary repair or in all repairs to correct an ontology. We are rather interested in the “right” one, which actually fixes the issues.
The task of finding an adequate repair is similar to contraction from belief revision [
Every repair, as in Definition 3, can be considered to be minimally diferent from the original ontology,
as no further axioms can be re-introduced without reintroducing the error. It has also been proposed to
consider only repairs of maximal cardinality, as they minimize the number of removed axioms. Yet,
these are not only hard to compute [
A diferent perspective comes from trying to extend the class of models of the ontology, without
necessarily preserving its full syntactic structure. From this point of view, one idea is to weaken (i.e.,
make more general or less restrictive) the axioms in a diagnosis through syntactic refinement operators.
These gentle repairs preserve more of the original consequences, and do not damage too much the
original structure, by substituting an axiom by one of its maximally strong weakenings. On the other
hand, so-called optimal repairs aim to semantically preserve as many of the original consequences as
possible, with less regard towards the ontology syntax [
The main limitation of all these approaches is that they are purely logical, and hence cannot really take into account the domain knowledge to generate the ontology which best coincides with the intent of the modeller. Indeed, correctness of an ontology is a meta-logical property, and logic alone cannot distinguish which of all the possible repairs available best describes the domain knowledge. To find the “true” repair, the only solution is to ask domain experts which are able to identify erroneous constraints. However, the sheer number of options available makes it impossible for any human expert to select among them. Thus, we propose an iterative approach which relies on user-input to identify the best possible ontology repair. The main dificulties and proposed solutions are described in the next section.
We recall that the final goal is to repair an ontology; yet, as repairs are almost as big as the original ontologies (with up to hundreds of thousands of axioms), presenting a user with the choice between two repairs (or more) is not helpful. Rather, we take advantage of the duality between justifications and repairs and focus on the computation of the former—which are typically of a much smaller size—and the diagnoses that arise from them. A naïve idea is to enumerate all the justifications, one at a time, and ask the user to identify one axiom to be removed, until at least one axiom from each justification has been deleted. This idea is not only impractical given the potentially exponential number of justifications available, but might also lead to the deletion of too many axioms if the user was unable to identify that a diferent choice would “touch” other yet-unseen justifications. Indeed, by studying one justification at a time, the user cannot grasp the full picture of the repair process, which forces them to think about individual axioms instead of their global consequences. Note that despite being a domain expert, the user is not omniscient towards all the consequences that are afected by the removal of an axiom.
We present in detail our novel approach for interactively repairing ontologies. The basic idea is very simple: ask a sequence of questions from the knowledge engineer which will allow to identify the correct repair among the large number of candidates. However, as human experts are scarce, costly, and tire easily, we should try to minimise the number of questions and their dificulty, thus maximising the investment on human work. Moreover, the order in which the questions are asked may influence the quality of the final result.
The first step towards an adequate user-guided ontology repair is to prune the search space; i.e., reduce the amount of answers required by the user. We introduce a two-phase procedure. In the first phase (interactive pruning), the user specifies some consequences and axioms which should be preserved in the repair. In the second phase (automated pruning) the system identifies and protects structurally central axioms from the ontology. After pruning, the approach goes into a diagnosis computation phase, which can be performed either manually, by interacting with the user, or fully automatically, letting the system using predefined strategies to select the most appropriate diagnosis according to the desired repair goals. Yet, an important element of our approach is that we do not want to compute the whole set of justifications or repairs either a-priori or during the interaction. Instead, we try to minimise this computational efort as well.
To simplify the procedure and its exposition, we assume that the ontology is in normal form (see
Section 2). If this is not the case, we can always first pre-process the ontology through a normalisation
method like the ones suggested in [
It can be seen that conjuncts appearing in a normalised ontology are necessarily syntactically disjoint; i.e., they refer to diferent syntactic (concept) names even if they may have implicit semantic connections derivable from the ontology. This syntactic disjointness and the simplicity of the normal form allow for more fine grained repairs, without removing more information than what is needed. This property is guaranteed in gentle repairs, since the maximally strong weakening would preserve as much information as possible without any need for preprocessing. Nevertheless, the preprocessing is useful in general, as it allows to present to the user smaller axioms and to avoid the problem of having justifications consisting of very few, but very complex axioms. Normalisation renders axioms and justifications more comprehensible for the user, who can manage them more eficiently, leading to an improvement in the user experience.
As we have seen, the naïve approach to repairing the ontology may lead to a deletion of too many axioms. The main issue is that presenting one justification or one axiom at a time to the user may not let them understand the implications of its removal. Thus, our algorithm should select a subset of relevant questions from all the possible ones, structuring them in a convenient way to let the user express their preferences obtaining the repair that better fits their needs.
First note that only axioms which appear in at least one justification will ever need to be removed to obtain a repair. Hence we start with the set defined as the union of all justifications. Although it is expensive to compute this set, we can do that process once, in the background, before any interaction with the user. The next step is to identify which axioms are more important than others for reasoning with the ontology. Once these important axioms are identified, we can prevent them from being excluded from the repair, by removing them from the set . This efectively ensures that the repair, whatever it will be, will maintain such axioms and their consequences. We call this technique of identifying important axioms that should be retained in the final repair justification pruning. As we will see, this pruning allows to overcome many of the limitations of the naïve approach. However, we still have not formally defined what does it mean for an axiom to be important. As we explain next, in the context of interactive repair, it is useful to distinguish between two complementary notions of axiom importance, which guide the reduction of the repair search space: relevance and prolificacy.
We call an axiom relevant when it is identified as such by the user. This could be either because the user explicitly stated its importance for the ontology; because it is frequently used in deployed reasoning tasks; or because it is required to derive other specific consequences that the user wishes to preserve. The importance of relevant axioms is thus subjective and driven by the user’s intent. In the context of our strategy, we identify relevant axioms as those that appear in at least one justification for a user-specified desired consequence. These axioms are considered important precisely because they enable the derivation of such consequence.
On the other hand, the notion of prolificacy assesses the objective importance of an axiom in the knowledge base for deducing consequences. Informally, we say that an axiom 1 is more prolific than an axiom 2 if the number of consequences for which 1 is necessary is greater than the number for which 2 is necessary. In this case, we say that 1’s prolificacy is greater than 2’s. In our framework, most prolific axioms are automatically identified and protected during the automated pruning phase; see Section 4.3 for details.
By combining both perspectives, the repair process benefits from a dual safeguard: relevant axioms, computed via desired consequences, ensure the preservation of the consequences relevant to the user; whereas the identification of most prolific axioms avoids removing semantically meaningful knowledge when less expensive alternatives are available.
Before going into details, note that in general it seems reasonable to assume that prolific axioms (from which many consequences can be derived) are also relevant; that is, are also subjectively important to the user. However, this correlation depends on how the ontology is used and on the user’s specific goals. If this overlap were guaranteed, there would be no need for an interactive approach, and it would sufice to compute the repair that maximises prolificacy. Since we need to understand what are the specific preferences of the user, we implement two distinct strategies for identifying important axioms, corresponding to two phases of justification pruning: interactive pruning, which preserves axioms based on user specified desired consequences and feedback; and automated pruning, which protects most prolific axioms in a justification according to objective metrics.
To order these strategies, we assume that the user preferences are more important than the objective entailments of single axioms, as they represent the ground truth for the domain knowledge. Thus, the starting point is to ask the user for desired consequences. In doing so, we establish that axiom relevance is more important than prolificacy. In particular this means that, whenever it is not possible to preserve relevance while maximising prolificacy, priority will be given to the former, as exemplified next. Example 4. Consider the ontology composed of the ABox := { 1 : (), 5 : (, )} and the TBox := { 2 : ⊑ , 3 : ⊑ ⊥, 4 : ∃.⊤ ⊑ ⊥}, where the prefixes are just names given to the axioms for brevity of presentation. It is easy to see that is inconsistent, and that there are two justifications for inconsistency; namely, 1 := { 1, 2, 3} and 2 := { 4, 5}; this means that there are six diagnoses and repairs for this inconsistency.
these three axioms are marked as relevant, and must be protected through the repair process.
At this point, the system moves to the automated pruning phase. Consider that the system identifies 4 as the most prolific axiom. Protecting it from removal would result in preserving the full justification 2 (as 5 is already protected) and hence the inability to repair , or on removing 5, and thus the consequence requested by the user. As the user preference is prioritised, the system does not protect the axiom 4. This illustrates the precedence of interactive pruning over automated pruning: the system should prioritise the will of the user over automatic choices. In fact, considering this precedence, the system could have avoided (in this simple example) computing the prolificacy of 3 and 4 and conclude that they form the only available diagnosis that satisfies the user’s request.
In brief, justification pruning is a method which allows to protect some of the axioms from so that they cannot appear in any computed diagnosis—and by extension, are guaranteed to appear in the ifnal repair found. This has the advantage of reducing the number and complexity of questions to be asked to the user in the repair process, and ultimately reduce the human efort. Note that there is no pre-defined number of axioms that should be saved in the repair: this number varies depending on the specific case. However, is always suficient for computing a diagnosis after pruning.
Having introduced justification pruning, we can now explore more in detail each of the two phases. In the following, as done before, we will use the expressions "save," "preserve," and "protect" to indicate that some axioms are prevented from being included in the diagnosis. We will sometimes express the same idea by saying that these axioms are removed from the union of all justifications . This is motivated by the fact that diagnoses will be built as subsets of .
As seen, justification pruning is needed to reduce the search space for a repair by reducing the amount of questions to submit to the user. In the interactive pruning phase, what we do is to interact with the user, asking them to freely express desired consequences and axioms that they want to preserve in their repair. That is, user expresses desiderata by stating knowledge that they know to be correctly reflecting the representation domain.
If the user knows that an axiom is important for their scopes, they are free to instruct the system
to protect such axiom, and it will immediately be removed from the set of the axioms from where
a diagnosis is being built. Yet, the user may not want to point to specific axioms, but rather to more
general consequences of the ontology. In this case, we propose that, after a desired consequence
is indicated by the user, the system removes one justification for from the set . This efectively
reduces the number of potential axioms to be verified by the user. Computing one justification for a
consequence requires polynomial time, so is completely feasible in ℰℒ⊥ [
Pinpointing the desired consequences is a smart strategy to restrict the search space for repairs with minimal eforts from the user, since they do not have to compare diferent options, but can directly indicate their preferences on consequences. Indeed, thanks to this idea of specifying desired consequences, the user is free to input whatever consequence they want (as long as it is correct). In this sense, we have addressed the problem of structuring questions. Indeed, this design is way better than presenting sets of axioms or one justification at a time as in the naïve approach, that does not allow to reason about implicit knowledge.
To compute the justification for we can use the well-known black-box algorithm that makes a linear number of calls to a standard reasoner. The algorithm tries to remove one axiom at a time from the ontology, while is still entailed. While irrelevant for correctness, the order in which the axioms are removed influences the justification found. Here, two conflicting forces come into place. On the one hand, we would like to reduce and hence, try to keep as many axioms from as possible in the justification. On the other hand, if is entailed already by ∖ , then we know that is preserved in all repairs, meaning that no special handling of is needed. Under these conditions, we prioritise preserving more potential repairs, as this helps guarantee that the “correct” one (from the domain knowledge point of view) can still be computed. This has the added advantage of preserving as many of the original consequences as possible as well. Intuitively, we want to order the axioms so that those belonging to are tested (and potentially excluded from the justification) first.
As our interest is mainly on the axioms that will be removed from , and not on the precise justifications of , we modify the black-box algorithm to further reduce the number of calls to the reasoner. First, we verify whether ∖ |= . In that case, we know that there is a justification w.r.t. ∖ and no axioms need to be protected. Otherwise, we apply the standard black-box algorithm, but only verifying whether the axioms in can be removed. This idea is described more formally in Algorithm 1 and exemplified next.
Example 5. Consider the ontology with an empty ABox and the TBox := { 1 : ⊑ , 2 : ⊑ ∃., 3 : ⊑ ∃., 4 : ⊤ ⊑ , 5 : ⊑ , 6 : ∃. ⊑ , 7 : ⊑ ∃., 8 : ⊑ , 9 : ⊑ ∃., 10 : ∃. ⊑ , 11 : ∃. ⊑ } having the erroneous consequence := ⊑ ∃. . The error has two justifications; namely, 1 := { 1, 2} and 2 := { 3, 4}. So, := { 1, . . . , 4}. justifications: 1 := { 1, 5} and 2 := { 6, 7}.
Suppose that := ⊑ is a desired consequence provided by the user, which can be seen to have two computed the justification 2 , thus (unnecessarily) protecting 1.
Applying Algorithm 1, we see that ∖ |= because 2 ⊆ ∖ . Hence, is preserved in any repair, and no axiom needs to be protected. Note that without the first check, the black-box algorithm could have Consider now the desired consequence := ⊑ ∃. whose only justification is := { 1, 7}.
Algorithm 1 first verifies that
∖ ̸|= and enters the for loop with the axioms in . In the first iteration, ∖ { 1} ̸|= , and hence enters the else in line 6, updating to { 1}. At this point, the algorithm verifies that ( ∖ ) ∪ = { 1, 5, . . . , 11} |= which breaks the for loop and terminates the algorithm with
If the user wishes to preserve multiple consequences, a simple idea would be to apply Algorithm 1 to axioms. Yet, as we see next, this may lead to erroneous results. each of them sequentially, updating the set between calls to take into account the known protected 1 := { 1, 8} and 2 := { 2, 9, 10, 11}. and := ⊑ . As seen already, has only one justification Example 6. Continuing Example 5, suppose that the user specifies as desired consequences := ⊑ ∃. = { 1, 7}. Instead, has justifications:
unwanted consequence and no repair could be computed.
2 which would require 2 to be protected. But in that case, we would preserve a justification for the
However, note that the order in which the desired consequences are analysed influences the final result. Indeed, in the previous example, if had been analysed before , we could have protected 2, which, as we have seen, would later lead to a wrong path. To solve this, we further extend the algorithm so that the justification is not computed for a single desired consequence, but for all simultaneously; that is, instead of considering an input , it considers the whole set Γ of desired consequences to be entailed in each test. This guarantees that all requirements are satisfied, minimising the number of protected axioms.
Other modifications can be applied to try to improve eficiency. For instance, one may focus on justifications or diagnoses of minimal cardinality, either for protecting fewer axioms or for diminishing the potential options remaining. Alternatively, one may consider axioms that appear in the most justifications, as they allow for smaller hitting sets, and thus smaller diagnoses, as illustrated in the following example.
Example 7. Consider the ontology = ( , ) formed by := { ⊑ | 1 ≤ ≤ } ∪ { ⊑ } ∪ { ⊓
⊑ | 1 ≤ ≤ } := {()} ∪ {() | 1 ≤ ≤ } and suppose that () is an erroneous consequence. The justifications for this error are {{(), (), ⊓ ⊑ B} | 1 ≤ ≤ }.
Suppose now that the user specifies a desired consequence = (), which has the justifications := {(), ⊑ }, +1 := {(), ⊑ } 1 ≤ ≤ ;
⊑ . As a consequence, the diagnoses left for () are all the possible hitting sets of the justifications for this unwanted consequence which do not contain (). In other words, the diagnosis will necessarily contain axioms. On the other hand, if the black-box algorithm is instructed to remove first the axioms that are shared with other justifications from the set , then the axioms (), ⊑ will be protected for some , making it possible to reach the smallest diagnosis {()} which has only one axiom to remove from the ontology to reach a repair.
According to the definition of justification, it cannot be the case that a justification for an error entails another justification for the same error. However, this property may no longer hold after the interactive pruning phase.
1 = { 1, 2, 3}, 2 = { 1, 2, 4, 5}.
justification = { 3, 60} for . As a result, 3 is marked as relevant and protected. Looking into 1, we see that only 1 and 2 could be selected in a diagnosis to compute a repair. Since both of those axioms appear also in 2, any of these choices is already a hitting set of the justifications and no further analysis is necessary.
This example highlights an important efect of interactive pruning: the decision to preserve an axiom in one justification can directly influence others by narrowing the available options for removal. In particular, when two justifications share a subset of axioms, and pruning removes one of such axioms in order to maintain a desired consequence, the remaining axioms in the second justification may no longer need to be considered during the repair process. As a result, some axioms can be automatically preserved or ignored, further narrowing the set .
We now change our attention to the second stage of axiom pruning, which allows to automatically prune justifications of size greater than or equal to two. It should be clear that we cannot prune justifications of size one, as any diagnosis must contain them (otherwise, it would not be a hitting set of all justifications). As mentioned earlier, we want to prune justifications according to the prolificacy of their axioms, where prolificacy is a measure of axiom importance for deducing consequences. Defining and assessing axiom prolificacy is not straightforward. Intuitively, prolificacy refers to the number of consequences that depend on the axiom; however, as the number of consequences of an axiom or an ontology is typically infinite, we need a way to restrict to only relevant information. In ℰℒ⊥, we focus on atomic subsumptions (i.e., GCIs of the form ⊑ with , ∈ ) and concept name instances (assertions () with ∈ and ∈ ) as basic consequences of interest. The class of these consequences has polynomially many objects in the vocabulary of the ontology. For the rest of this paper, we use C to refer to the (finite) class of relevant consequences of interest. In addition, one should also consider the interactions between axioms in the derivation of these consequences. Example 9. Consider the very simple ontology := { 1 : ⊑ , 2 : ⊑ , 3 : ⊑ }. In addition to the axioms, entails only the atomic subsumptions : ⊑ , : ⊑ , and : ⊑ .
We see that none of the axioms, by itself, sufices to derive any of the consequences, yet, in pairs and triples they entail some or all of the consequences: { 1, 2} |= { 1, 2, } { 1, 3} |= { 1, 3} This analysis clearly shows how much each axiom contributes to verify consequences.
Assuming that is the unwanted consequence, it should be excluded from the number of relevant entailments. We can see that 1 contributes only to the derivation of (and the error), while 2 and 3 contribute also to the derivation of . Hence, we consider these latter axioms as the most prolific from .
Without consider prolificacy, any of the two diagnoses 1 := { 1} and 2 := { 2} is an equally good solution, from a logical point of view, for getting rid of the error. Yet, in light of the entailments computed, we observe that opting for 2, i.e. removing 2 from the ontology leads to a repair which does not entail , while removing 1 from still yields as a consequence. As the goal is to preserve the most consequences, we prefer to use the diagnosis 1 or, more in general, to remove first the least prolific axioms.
This example has illustrated that including a prolific axiom in a diagnosis may result in the loss of relevant knowledge. To avoid this problem, we suggest to identify a set of highly prolific axioms to preserve in the repair. Moreover, it has explained that to assess the prolificacy of an axiom we should look at how it interacts with others in the knowledge base. There are diferent possibilities to assess the prolificacy of an axiom: usage statistics (frequency of use in inference tests or user tasks); structural measures (centrality in the graph); impact of removal (found by simulating removal and measuring loss of desired inferences); and many others.
Usage statistics are dificult to obtain, since they require a set of queries that are submitted by users,
which typically are not available, nor easy to produce. For what concerns the structural measures, it
is possible to estimate the importance of an axiom by analysing the dependency graph or the atomic
decomposition the ontology. In such a graph, the knowledge base is partitioned into modules, each
containing a set of axioms supporting related entailments [
Definition 10 (prolificacy). Let cl() = { ∈ C | |= } be the closure of over C; that is, set of all the consequences in C entailed by the ontology . The prolificacy of an axiom ∈ is defined as () = |cl()| − |cl( ∖ {})|.
Note that this definition of P() makes sense just if |cl()| < ∞, which is the reason why we restrict to relevant consequences. Still we emphasise that within the logics of the ℰℒ family, it is common to focus on atomic consequences only. Interestingly, in ℰℒ⊥ the full classification (i.e., computing all the atomic subsumptions) and all the basic entailed instances can be computed in polynomial time in the size of the ontology. Thus overall it is possible to compute the prolificacy of all axioms in polynomial time. Yet, to improve eficiency, we focus on some of these axioms only. Recall that the aim of the prolificacy computation is to reduce the search space for finding a repair. For this reason, we only care about the prolificacy of the axioms in , from which diagnoses are being created. However, looking at prolificacy alone may still lead to errors, specially when some axioms are shared among justifications. This problem is avoided by verifying that a diagnosis still exists, before protecting an axiom from . However, there is also the issue that prolificacy may be relative among justifications; that is, the most prolific axioms in one justification may be the least prolific in another one. In that case, it is not clear which justification should take precedence in deciding which axioms to protect. Algorithm 2 Automated Pruning of Prolific Axioms Require: Justification of size > 1, threshold Ensure: ′ ⊆ of minimal cardinality such that ( ′) ≥ · ( ).
1: Sort into { 1, . . . , } such that ( 1) ≥ ( 2) ≥ · · · ≥ ( 2: ′ ← ∅ 3: ← 0 4: ← 1 5: while < · ( ) do 6: ′ ← ′ ∪ { } 7: ← + ( ) 8: ← + 1 9: end while 10: return ′ )
To avoid these problems of suboptimal solutions and the impossibility of finding a diagnosis, it would be more informative and precise to compute the impact of removal of entire diagnoses, and check the diferences among them. However, this would contrast with our aim of not calculating all the diagnoses. So, the solution we propose is to compute the prolificacy of only the axioms in a justification without shared axioms. Computing the impact of removal for such axioms, is actually a good estimate of the role they would play in the repair. In doing so, we avoid all the problems caused by axioms that are shared, and we reduce the number of axioms for which we compute () . Next, we describe the algorithm to prune such justifications.
An Algorithm for Automated Pruning. Once the system has computed the impact of removal () for each axiom ∈ , it sorts the axioms in descending order of () . After that, the algorithm should remove from the most prolific axioms in a quantity determined by a parameter as explained next.
Given a justification = { 1, 2, . . . , } for an error , let ( ) = ∑︀=1 ( ) denote the total
impact of removal of all axioms in . The algorithm then identifies the smallest subset ′ ⊆ , taken
in order of decreasing (), such that:
∑︁ () ≥ · ( )
∈ ′
where is a threshold parameter in the interval [
Note that in Example 9 we said that, when computing the prolificacy of an axiom, we should not count the error as a consequence. However, note that there is no need to modify () , since we are now calculating the prolificacy just for the axioms in the justifications that do not have axioms in common with others. So, in the case where diferent justifications for the error exists, the unwanted consequence will not be counted for any of the axioms in the justification; whereas, in the case where the justification for whose axioms we are calculating the prolificacy, the error will be counted as a consequence in () of all the axioms.
This strategy is a trade of between simplification and preservation of relevant knowledge, making the pruning phase both flexible and adaptive to the structure of each justification. In fact, it ensures that longer justifications are pruned more that smaller ones, reducing the number of axioms in and facilitating the user in the computation of a diagnosis.
Again, note that automating the process of finding the prolific axioms is better than asking to the user to autonomously identify all the axioms that are important. This is due to the fact that the knowledge engineer may not be completely aware of which axioms of the knowledge base are important, in other words they may not see the consequences of keeping or removing a given axiom. The error of keeping a redundant axiom, which may occur if the knowledge engineer is free to choose, is avoided using the impact of removal.
So far, we have discussed strategies to prune the search space to find the “true” repair in the sense of restricting the number of axioms (and questions) to present to the user. This phase has ensured that all the remaining repairs verify the desired consequence of the user. Moreover, thanks to the identification of prolific axioms, we have an approximation of the fact that these repairs will be maximal (according to the desiderata of the user). At this point, most of the issues of the naïve approach have been overcome, and, as explained, we can continue either in an automatic way, or by presenting questions to the user. Next, the two options are presented.
For the manual one, we still need to think of an efective way to present justifications and axioms to the user. To this end, we will use some heuristics. For the automatic alternative, we will base the computation of the diagnosis on assumption that we prefer to apply minimal changes to the ontology, thus trying to remove the smallest set of axioms from . To this aim, the algorithm will present the smallest possible diagnosis, allowing the user to approve or modify it. Recall that the two options (manual and automatic) are not mutually exclusive nor fully intertwined, since the knowledge engineer is free to stop whenever they want, and let the process finish automatically.
If the knowledge engineer wants to control the construction of a diagnosis, the system should let them manually choose one axiom from each justification. Since they have already specified their preferences on consequences, we can safely present one justification at a time, and let the user choose from them. However, there are still multiple ways of presenting axioms and justifications to the user, each resulting in a diferent sequence of decisions. Some of these sequences are smaller than others; thus, presenting the justifications in a certain order may reduce the number of questions. Also, since after the pruning phase all the possible reachable repairs will verify the desired consequences, all possible diagnoses that can be built are considered to be already adequate from the user requirements point of view—that is, from the perspective of preserving the true knowledge from the domain. At this point of the procedure, since the knowledge engineer has already freely expressed their desiderata on consequences (and axioms), the user discovers their preferences in the interaction with the system. Thus, the very idea of presenting justifications in an “optimal” way is flawed. At this stage, what the system can do is to guide the user, and order justifications and axioms thanks to heuristics that help minimise the number of questions and maximise the utility of the answers.
In particular, the heuristics should act on the two dimensions that render the number of options to consider too big from the user’s point of view: the length of each justification; and the number of justifications.
The issue of the length of each justification refers to the fact that a single justification may have a number of axioms too high to be manageable by the user. However, at this point of our procedure, the problem has mostly been solved thanks to both interactive and automated pruning. It may still be the case that long justifications have survived, but it is unlikely. In fact, if such justifications exist, it is because they did not have axioms in common with any of the justifications computed for the desired consequences. At the same time, they must also be justifications that share axioms with others. Otherwise, they would have been reduced during the automated pruning. As we will see in what follows, this observation provides us with the solution for solving the problem.
For what concerns the other dimension, the number of justifications may indeed be too long. However, we can try to overcome the problem by suggesting to the user to remove axioms that are shared by most of the justifications. When these axioms are removed from one justification, as an inherited answer they are also removed from all the justifications where they appear. Hence, we do not need to present those justifications to the user, and the number of questions is reduced. Moreover, consider that, in any case, if the amount of questions is too large for the user, they always have the option to let the system automatically compute the diagnosis.
In case of automatic computation, the heuristics help the user to orientate among the axioms of the justifications. Diferent heuristics may serve diferent goals, so, before implementing one heuristic, we have to figure out what each heuristic is useful for. If our scope is to apply minimal changes to the ontology, we should try to build the smallest possible diagnosis via shared axioms. If the aim is to preserve as much consequences as possible, we should start by presenting to the user the axioms less prolific for each justification; if our aim is to understand as quick as possible which axiom should be removed from each justification, we should present the smaller justifications first. These heuristics are presented more in detail in the next subsections.
In any case, it is important to remember (and to stress) that, in the end, the decisions of the user should be the primary consideration. The system defines an order just to help the user, but should not force them to choose one axiom over another. Also, we assume that the knowledge engineer knows how the system works, in the sense that they know that the machine orders axioms based on the estimation of which ones are preferable to remove first. Therefore, we stated that the approach is interactive, as it is based on an eficient Human-Computer collaboration.
As we have seen, axioms that are shared by diferent justifications may cause issues in the naïve approach, since they influence diferent justifications. We now show how they can be used to the user’s advantage. The idea is that, in ordering the axioms in the justification that the system presents to the user, shared axiom should be presented first. In fact, these are the axiom that appear more frequently than others in the justifications for the error. If such axioms are removed, they are likely to lead to the smallest possible diagnosis.
Since the aim is to reduce as fast as possible the search space for repairs, the idea behind presenting shared axioms first, is that these allow to build a diagnosis in fewest step. The reason is that, once selected (and removed) from one justification, they are discarded also from all other justifications where they appear. Therefore, there is no need to select other axioms for such justifications, reducing the number of questions. The extreme case is that of a shared axiom appearing in all justifications, in such a case, the shared axiom constitutes a diagnosis by itself.
The idea of shared axioms can also be applied to, and is particularly useful in cases where there are more errors in an ontology, for instance when errors arise from merging knowledge bases. In this case we can call maximally shared axioms those that are the most common among the justifications of the two errors.
The benefits of this strategy are two, namely, that it reduces the number of questions the user has to answer, and that it leads to apply minimal changes to the knowledge base from the syntactic point of view. Of course, it only works if the shared axioms are actually removed by the user. On the other hand, if the user wants to keep the axioms, we do not reduce our search space by a lot, but we do not have to ask for such axioms again in the next justifications. Otherwise, if the system would ask for those axioms in following justification, and the user chooses to remove the shared axiom, the minimality of the diagnosis is lost. This is yet another example of the fact that a greedy approach leads to suboptimal results, as we have seen for the naïve approach.
It could also be useful for the user to see the number of justifications left to be answered. This number shows the worst case scenario, and should be updated after each axiom is chosen from a justification.
We have seen that within the justifications, it is a good idea to order axioms presenting those that are shared first. However, what is the system supposed to do with justifications that do not share axioms with others? Recall that in the automated pruning phase, we ordered such axioms according to their prolificacy. Hence, we can reuse this previous computation to order the axioms presenting them from the less to the most prolific one. Indeed, we want to suggest to the user to remove the less prolific axioms, so that the least consequences are removed from the final repair. Moreover, since we have computed the entailments for each axiom, it is also possible for the user to see which are the efects of removing a certain axiom; i.e. which are the consequences that are lost. This is actually much more informative from the user’s point of view than looking at the single axioms.
Recall that, within an interactive diagnosis process, the order in which justifications are presented to the user plays a key role in optimizing the interaction. In this section we explain that the simple heuristic of presenting the shortest justifications first is a good strategy to order them.
First note that shorter justifications contain fewer axioms, which means that the user can analyse them more quickly and with less efort. So, by prioritising shorter justifications, the system allows the user to tackle simpler cases first, reducing the risk of early disengagement. This aligns with the goal of reducing the cognitive load of the knowledge engineer.
Second, if the user chooses to stop interacting with the system before completing the entire process, they will have only dealt with simpler and smaller justifications, avoiding the burden of analysing more complex ones and possibly selecting axioms from more justifications. This ensures that even partial interaction can contribute meaningfully to refining the repair process. For example, if the user has energy to analyse just twenty axioms and we present a justification consisting of twenty axioms, they will ultimately analyse only this single justification. On the other hand, if we present four justifications consisting of five axioms each, the user will still consider twenty axioms, but will respond to four justifications.
In summary, presenting the shortest justifications first balances eficiency and user engagement, supporting a more user-friendly and practical interactive repair process.
In the previous sections, our focus was on finding ways to minimise the human efort in the computation of a repair, by protecting some axioms that are considered correct or at least wanted in the ontology. We should bear in mind that the user, when presented with the diferent questions, is iteratively selecting a diagnosis: the axioms signalled as erroneous.
From the point of view of classical repairs, the final step after computing a diagnosis is to remove it from the ontology, thus obtaining a repair à la Definition 3. However, removing full axioms from the ontology can be seen as an extreme solution: one should take into account that axioms are not added arbitrarily, but there is usually a motivation behind them. Moreover, some of the information provided by the axiom may be correct, even if not all of it. We partially considered all these issues by requiring the ontology to be in normal form. Yet, even in this simplified scenario, it is worth asking whether removing full axioms is the best solution.
A proposal to preserve more of the original knowledge is to weaken rather than delete, the elements
of the diagnosis. This approach is typically known as gentle repair [
A common approach for axiom weakening is to apply concept refinement operators to the elements of the axioms. Briefly, to weaken a GCI of the form ⊑ , one may specialise to a concept that is necessarily subsumed by , or generalise to a concept subsuming it. In both cases, the result is an axiom which has strictly more models than ⊑ . Analogously, the assertion () can be weakened by generalising . Note that if, as assumed, we have an ℰℒ⊥ ontology in normal form, then syntactic refinement operators are not only quite simple—in fact, concepts in the left-hand side of a normalised GCI can only specialise to ⊥—but easily lead to tautologies, which is equivalent to removing the axiom. Hence, although gentle repairs can be very useful to preserve more consequences, on normalised ontologies their impact is limited. However, if the ontology is not originally in normal form or if the language under consideration is more expressive, they could provide better results.
It is well known that ontology engineering is an error-prone task, which has attracted quite some attention over the years in the development of methods which automatically correct a given ontology. Yet, there may be many diferent ways to correct an error. Many diferent ideas have been proposed for selecting the “best” among them like choosing largest correct sub-ontology or maximising the set of preserved consequences. However, these syntactic and semantic approaches ignore one fundamental issue: the correctness of an ontology—i.e., its expression of the knowledge domain under consideration— is a meta-logical property, which can only be verified by a domain expert. In other words, there is no way to guarantee that repairs with minimum change actually reflect the knowledge of the domain.
On the other hand, the size of the ontology and the potential number of justifications (and diagnoses) and axioms appearing in them makes it impossible for a knowledge engineer to select the most adequate repair from all the available options without the help of an automated tool. Moreover, human experts are costly and tire fast, so we should try to minimise their efort.
In this paper, we proposed an intermediate path, where the knowledge engineer is iteratively asked to choose one axiom from each justification to be removed as considered wrong, without the need to compute all justifications or diagnoses at any time. The main novelty of our work is to include first a pruning phase, which identifies axioms that are considered “correct” and hence safe from removal. This pruning takes input from the knowledge engineer, who specifies a set of consequences that need to be preserved, to choose minimal conditions that guarantee this request. It also applies an heuristic for minimal change, based on a new notion of prolificacy: the impact an axiom has on the number of consequences derived.
Our procedure computes a diagnosis, which refers to the class of axioms identified as wrong in the ontology. At this point, one could decide to simply remove these axioms (yielding a repair) or to weaken them towards a gentle repair, as suggested in previous work.
It should be clear that the choice of prolificacy as a way to find axioms to be preserved is a heuristic based on the centrality (or importance) of the axiom for the concept hierarchy. As mentioned already, no purely logical, syntactic, or semantic measure can fully characterise the meta-logical property of correctness for the representation domain in consideration. Thus, this one may also yield an incorrect repair. However, we argue that exactly their centrality makes these axioms to be subject to deeper scrutiny, and hence less likely to be wrong from the domain point of view.
One could imagine other measures for automated pruning like, e.g., a degree of trust associated to
axioms, depending on their source and use in the ontology. In this way, one can measure trust on
one or more consequences using the techniques from provenance [
For this work we focused on the light-weight DL ℰℒ⊥. The main reason for this is that its
polynomialtime reasoning services allow us to provide polynomial-time algorithms for each of the steps of the
iterative procedure, except for the initial one of computing the union of all justifications , which
requires superpolynomial time (unless = ) [
As part of our future work, we expect to build a better understanding about the properties of prolificacy and develop more eficient methods for computing them directly. Moreover, we will try to understand the guarantees that preserving axioms based on their prolificacy provides from the ontology repair and belief revision point of view. Note also that our approach is parameterised to maintain a proportion ( ) of the prolificacy of a justification, but we did not specify a precise value for this parameter. From a practical point of view, we want to study the impact of this parameter on the overall efort and quality of the repair process.
Part of this work was developed during a research visit by the first author to TU Dresden, funded by the University of Milan under the programme “Tesi all’estero.” We are thankful to Prof. Franz Baader for his advise and fruitful discussions during this visit and to Christian Alrabbaa for clarifications.
The authors have not employed any Generative AI tools.