Understanding logical entailments derived by a description logic reasoner is not always straight-forward for ontology users. For this reason, various methods for explaining entailments using justifications and proofs have been developed and implemented as plug-ins for the ontology editor Protégé. However, when the user expects a missing consequence to hold, it is equally important to explain why it does not follow from the ontology. In this paper, we describe a new version of Evee, a Protégé plugin that now also provides explanations for missing consequences, via existing and new techniques based on abduction and counterexamples.
We present a Protégé plugin for explaining missing entailments from OWL ontologies. The
importance of explaining description logic reasoning to end-users has long been understood,
and has been studied in many forms over the past decades. Indeed, explainability is one of the
main advantages of logic-based knowledge representations over sub-symbolic methods. The
ifrst approaches to explain why a consequence follows from a Description Logic (DL) ontology
were based on step-by-step proofs [
While reasoning can sometimes reveal unexpected entailments that need explaining, very
often the problem is not what is entailed, but what is not entailed. In order to explain such
missing entailments, and ofer suggestions on how to repair them, both counterexamples and
abduction have been suggested in the literature. A counterexample is a model of the ontology
that does not satisfy the entailment, which may be further augmented to focus the attention of
the user to the part of the model that is most relevant for explaining the non-entailment [
In this paper, we present version 0.2 of Evee, a collection of plugins for the OWL ontology
editor Protégé, which now also ofers explanations for missing entailments. Those plugins integrate
the functionality provided by the external tools Capi and Lethe-Abduction for abduction, as
well as the counterexample generation methods discussed in [
We describe the new Missing Entailment tab of Evee in the next section, before explaining in
detail the diferent explanation services and how they are accessed through the user interface.
In Section 5, we explain how developers can use the infrastructure of the Evee Java libraries to
provide new explanation services for missing entailments. Additional proofs can be found in
the technical report [
We assume the reader to be familiar with the syntax and semantics of DLs [
Figure 1 shows this tab in action. It is divided into three major parts: In the upper part, one of the installed missing entailment explanation services can be chosen, the computation process can be started, and general information is displayed. On the left, the missing entailment and
2https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/ classic-spass-theorem-prover 3https://lat.inf.tu-dresden.de/~koopmann/LETHE-Abduction vocabulary can be entered, and in the center, the explanation will be displayed. The explanation view depends on the selected explanation service (see Sections 3 and 4). If the entered missing entailment and vocabulary are not supported by the service, the Generate Explanation button at the top will be disabled and an explanatory message will be shown.
How missing entailments are entered can be see on the left in Figure 1. The text field at the top can be used to enter individual axioms. The buttons in the middle allow the user to add an axiom to the list below, remove a selected axiom, or reset the whole list. Only OWL logical axioms are allowed, e.g. subclass-, equivalence-, and disjointness axioms and assertions. The selected missing entailment can also be saved to or loaded from an OWL ontology file, which can be useful for demonstration purposes.
By selecting the Vocabulary tab, the users can restrict the vocabulary used by the explanations, which can be seen in Figure 2. Here, the Ontology Vocabulary of the currently active ontology can be accessed via the class hierarchy, object property hierarchy, and list of individuals. The vocabulary of the explanation will be restricted to the names in the tab Permitted Vocabulary on the bottom, while Forbidden Vocabulary shows the remaining names of the ontology vocabulary. Depending on the currently opened tabs, the arrows and the button Add missing entailment vocabulary can be used to add or remove names to and from the selected vocabulary. Again, the permitted vocabulary can be saved to and loaded from an external file. By default, the whole ontology vocabulary is permitted, but this can be changed in the plug-in preferences at Preferences → Explanations → Missing Entailment → General.
While the explanation is generated, a progress window is used to indicate the computation status and show additional information. The computation can be canceled by closing the window or clicking the Cancel button. This will show a separate cancelation window while the computation is being terminated.
As a running example to illustrate the diferent explanation services, we consider a modified, incomplete version of the Pizza ontology.4 This version is missing some axioms to make it entail SpicyAmerican ⊑ SpicyPizza. It will turn out that other things are missing in this ontology as well, and the plugin will help the user in adding those missing parts.
The first obvious way to explain the missing entailment is to show an example of a SpicyAmerican
that is not a SpicyPizza, as shown in Figure 1. Evee 2.0 includes two plug-ins that provide
counterexample generation services: the Small Model Counterexample Generator and the Relevant
Counterexample Generator using Elk [
To visualize the counterexamples, we use GraphStream,5 a Java library for modeling, analyzing and visualizing graphs. Its functionality allows not only to visualize models, but also to dynamically make changes to models when the ontologies change. In the generated graphs, domain elements are depicted as circles. We highlight elements that are of particular importance for understanding the generated model. For instance, each counterexample contains a root element, marked in black, which satisfies the concept on the left-hand side of the GCI to be explained. For readability, only some of the concept names for each domain element are shown, whose number can be adapted using the Number of displayed classes slider on the right panel of the counterinterpretation view. When the user selects a node, the Classes of selected element list in the right panel displays all the concept names to which the selected element belongs. In the
node selected in Figure 1, the user notices in this way an element that is both a TomatoTopping and a MozzarellaTopping, pointing at another bug in the ontology—but more on this later.
The graphical model view allows zoom to facilitate exploring large graphs, and users can move the nodes of the graph. Dragging the mouse over the background canvas navigates through the graph. To make the graphical representation of a counterexample more informative, we display concept names in the order from more specific to less specific. In Figure 1, we display that the root element belongs only to SpicyAmerican and MeatyPizza, but it implicitly is also a Pizza, a Food, and ultimately a DomainThing, since the first two classes are subsumed by them. However, if we instead displayed in the graph that this element is a DomainThing, we would give no useful information about the element.
As in the present example, the visualized model can also reveal missing disjointness axioms in the ontology. As already noticed, in Figure 1, the selected element is both a MozzarellaTopping and a TomatoTopping. The reason is a missing disjointness between CheeseTopping and VegetableTopping. The right panel allows the user to add new disjointness axioms as needed and visualize the result. For this, the user selects the corresponding concept names in the Classes of selected element list and presses Add disjointnesses. A disjointness axiom with the selected names is then added to the Disjointnesses list, as shown in the figure. By pressing the Recompute example button, the user gets shown an updated model with the new disjointness applied. If the user is not satisfied with the changes to the model resulting from the new axioms, they can be deleted using the Remove disjointnesses button. Finally, axioms from the Disjointnesses list can be added to the active ontology with a click of the Add all to ontology button.
In this explanation service, counterexamples are generated using a tableau-based algorithm
for the description logic ℰ ℒ⊥. Given a GCI ⊑ , the algorithm first initializes an ABox
containing as only axiom (* ), where * is a fresh individual name. Next, it adds ⊑ *
to the TBox, where * is a fresh concept name, and normalizes [
The model of the ontology is obtained using a complete and clash-free ABox ′ obtained from the ABox by an exhaustive application of the expansion rules from Table 1. The ⊑-rule is almost identical to the similar rule in algorithms for ℒ. The only diference is that it takes into account the structure of the normalized TBox. It becomes applicable only to concept assertions with concept names or with a concept name under an existential restriction. The ⊓- and ∃1-rules are designed to add assertions that make the ⊑-rule applicable. For individual names having a successor belonging to some concept name, the ∃1-rule creates a concept assertion with this concept name under an existential restriction. The ⊓-rule breaks conjunctions into simpler assertions.
To keep the model small, we reuse existing individuals as successors when trying to satisfy existential role restrictions. Before reusing an individual name, a consistency check is performed, so that the rule cannot introduce any inconsistency. Moreover, we only reuse an individual as successor if this does not make the root element an instance of * , since the aim is to construct a counterexample for ⊑ * . if contains (), but not (), ∈ At() then →− ∪ { ()} if contains (, ) and (), is a concept name or ⊤, but not ∃.() →− ∪ {∃ .()} if contains ∃.(), but there is no s.t. (, ) and ()
if there is some , s.t. ∩ ∪ {(, ), ()} is consistent and does not entail * (* ) then →− ∪ { (, ), ()} else →− ∪ { (, ), (), ⊤()}, where is new in if () ∈ , ⊑ ∈ or {1(), 2()} ⊆ , 1 ⊓ 2 ⊑ ∈ or ∃.() ∈ , ∃. ⊑ ∈ and () ̸∈ .
then →− ∪ { ()}
The expansion rules are applied exhaustively, but the ∃2-rule is applied only if no other rule is
applicable. This restriction reduces the number of applications of the ∃2-rule, and consequently
the number of individuals added. The algorithm iteratively applies the rules until no more rule
is applicable, and then translates the resulting ABox into an interpretation in the usual way.
The correctness of the algorithm is shown in the technical report [
A more focussed explanation to missing entailments is provided by the Relevant
Counterexample Generator. Relevant counterexamples explain missing entailments by showing relevant
parts of the models of ℰ ℒ ontologies, where this time canonical models [
We distinguish four types of relevance as shown in [
The Δ-relevant part is a refinement of the -relevant part that focuses on the conditions
that are imposed by the ontology on , but not on . This allows for an “explanation by
contradiction” as follows. If |= ⊑ , then every subsumer of must also subsume .
However, there is a model of (the canonical model) in which there is an element of
that intuitively does not satisfy some condition that is satisfied by every element of .
Hence, cannot be subsumed by w.r.t. . Therefore, the Δ-relevant part contains only those
elements illustrating the contrasting conditions , e.g. -successors (not) satisfying in case
that = ∃. . The Δ¯ -relevant part is a further refinement of the Δ-relevant part that tries to
generalize these conditions . For example, if |= ⊑ , ̸|= ⊑ and = ∃.∃.∃. ,
then it is suficient to consider ∃.⊤ instead of , assuming that ̸|= ⊑ ∃.⊤. For more
details we refer the reader to [
Counterexamples always focus only on one model, and they do not necessarily make it obvious
what needs to be done to fix a missing entailment. This is where the explanation services based
on abduction come into play. For our running example, we show an explanation based on
abduction in Figure 2. Evee 0.2 includes two plug-ins based on abduction, namely the Complete
Signature-Based Abduction solver based on Lethe [
entailments consisting of a single GCI, and hypotheses are always without role restrictions. To use CAPI, the FOL theorem prover SPASS needs to be installed separately. We require an adapted version of SPASS, which can be installed following the instructions on the web page of CAPI.8
After computing an explanation with an abduction solver, one or more hypotheses will be
displayed in a list, as shown in Figures 2 and 3. Depending on the input and the algorithm,
the number of results may difer and may even be infinite. Therefore, the user can specify the
number of new results that are added to the list whenever the Generate Explanation button
is clicked again. Using additional buttons shown at each hypothesis, the user can then easily
add the hypothesis to the ontology (to repair the non-entailment) and get an explanation
why the hypothesis entails the non-entailment, using the proof functionality provided by the
proof-explanation and Evee 0.1 plug-ins [
Signature based hypotheses are computed by the abduction extension of the external library
LETHE [
The CAPI abduction solver internally relies on the FOL theorem prover SPASS to compute the
solutions to an abduction problem. In particular, based on a translation into first-order logic
clauses, SPASS computes a set of prime implicates, which are then used by the Java component
of the tool to construct the diferent hypotheses (see [
For developers who want to add their own non-entailment explanation services, the module evee-protege-core provides two new extension points for Protégé plug-ins:
de.tu_dresden.inf.lat.evee.nonEntailment_explanation_service for explanation services and
de.tu_dresden.inf.lat.evee.nonEntailment_preferences for managing plug-in-specific preference settings.
The preferences extension point is simple: One implements the interface PreferencesPanel provided by Protégé, and the resulting panel will be displayed in a tabbed pane accessible via Preferences → Explanations → Missing Entailment. Using the explanation service extension point requires a few more steps. Essentially, an explanation service needs to provide the nonentailment explanations as a Java Stream and visualize the elements of this stream in Protégé. To facilitate this for abduction and counterexamples, we provide two abstract base classes for abduction and counterexample services.
The main interface for explanation services is IOWLNonEntailmentExplainer, whose most important methods are supportsExplanation() and generateExplanations(). The first method determines whether the Generate Explanation button should be enabled or disabled. Since this method is called whenever the input changes, its implementation should not be computationally expensive. The second method returns the explanation in the form of a Stream<Set<OWLAxiom>>, where each set represents a single explanation for the missing entailment.9 We use streams to accommodate a potentially infinite number of explanations, as in the case of signature-based abduction.
On top of these generic methods, INonEntailmentExplanationService provides functionality to connect to the user interface. The method computeExplanation() is called when the Generate Explanation button is clicked, and cancel() is called when the user wants to cancel. The explanation service can also use an IProgressTracker to send information to the loading window and an IExplanationGenerationListener to send events to the main tab. To the loading window, one can send the current progress as well as a String describing the current computation status. The events for the listener can have an ExplanationEventType of COMPUTATION_COMPLETE, RESULT_RESET, WARNING, or ERROR. This allows the explanation service to display new results, clear the shown result, or display warnings or errors, respectively. The main tab ultimately requires the result in the form of a java.awt.Component, which is retrieved via the method getResult right after an event of type COMPUTATION_COMPLETE is received. This way, each service enjoys a great degree of freedom in displaying its explanation. We already provide pre-built functionality for abduction and counterexample services, as described in the following sections.
The class AbstractCounterexampleGenerationService contains all functionality related to the visualization of counterexamples and implements all methods of the INonEntailmentExplanationService interface. Classes extending AbstractCounterexampleGenerationService difer primarily in the used counterexample generator, which must be specified in the constructor using the method setCounterexampleGenerator().
Each counterexample generator implements the IOWLCounterexampleGenerator interface. The interface extends IOWLNonEntailmentExplainer by generateModel() and getMarkedIndividuals(). The model returned by generateModel() is represented using a set of OWLIndividualAxioms. Each of those should be an instance of either OWLClassAssertionAxiom or OWLObjectPropertyAssertionAxiom, which specify the content of the classes and properties in the interpretation. These axioms are also returned by the method generateExplanations() of the interface IOWLCounterexampleGenerator. Finally, using the method getMarkedIndividuals(), the service can specify individual names that will be highlighted in the visualization of the model. 9For abduction, these sets are the hypotheses, and for counterexamples they are sets of assertions that describe models.
As an example of how the abstract counterexample generator operates, consider again the algorithm described in Section 3.1. This algorithm is implemented in a separate counterexample generator and executed when generateModel() is called. Afterwards, the abstract counterexample generator sends an ExplanationEvent of type COMPUTATION_COMPLETE to the main tab. The resulting counter example is then provided to the main tab via the method generateExplanations().
The class AbstractAbductionSolver is used by both of the plug-ins presented in Section 4. The main responsibilities of this class are caching the results computed for a specific input, creating and maintaining the actual result component that is displayed to the user, and handling user input when any of the Add- or Delete-buttons of a hypothesis are clicked (see Figure 3). The class is generic in order to facilitate the caching of diferent kinds of results for each implementing solver via its generic type parameter. Caching is not done automatically by the abstract solver class. Instead, the implementing solver can use the methods checkResultInCache, saveResultToCache and loadResultFromCache.
In contrast to these user-experience-related functionalities, the actual computation of the missing entailment explanation is left to the individual implementations of the abstract class. As explained above, implementing the interface IOWLNonEntailmentExplainer requires providing a stream of explanations via the method generateExplanations(), i.e. a stream of sets of OWLAxioms, where each set represents a single hypothesis. This method will ultimately be called by the AbstractAbductionSolver when creating the list of non-entailment explanations that is shown to the user.
We believe that our plug-ins are an important step towards making reasoning more understandable to ontology users. The implementation is still relatively new and there are little performance issues that need to be solved. We hope that our framework will encourage other developers to implement their own explanation services in Evee. In addition to further improving Evee, we would like to evaluate our plug-ins in a user study. It would also be interesting to investigate whether Evee can be used to improve university-level teaching on ontologies and description logics.
This work was supported by DFG grant 389792660 as part of TRR 248 – CPEC (see https: //perspicuous-computing.science).