Explaining Reasoning Results for Description Logic Ontologies

In a world where subsymbolic methods from AI are the main focus of research, symbolic reasoning with knowledge representations still offers a level of transparency and control that cannot be matched by such methods. The reason is that in knowledge representation, we represent our knowledge explicitly in a format that is both machine-processable and human-understandable. Through symbolic reasoning, we can make new inferences on these knowledge bases in a transparent manner. This is in particularly true for logic-based systems, which come with a clearly defined semantics and allow for deductive reasoning methods for which we can mathematically prove that they only make correct inferences. If a symbolic system comes to a conclusion that is not true, assuming that the reasoning engine is bug-free, this can only be due to an error in the knowledge base, which can then be identified and fixed.

Description logics are arguably one of the most important logic-based knowledge representation formalisms. They are the logic-based underpinning of the Web Ontology Standard OWL 2.0 [33], and are used to describe ontologies. An ontology describes a conceptualization of some domain of interest – it defines and puts constraints on the terms that are relevant in that domain for a particular application, considering unary relations (concepts) and binary relations (roles). Automated reasoning systems for description logics can be used to solve a variety of tasks with an ontology: in addition to determining whether an ontology is logically consistent, they can infer implicit relationships between the defined concepts (a task called classification), they can classify nodes in knowledge graphs, and they can be used to evaluate complex queries on databases, which then also take into account the implicit knowledge in the data that can be inferred through use of the ontology [14].

Research on description logics in the late 1990s and 2000s lead to two developments: on the one hand, the discovery of lightweight description logics such as $ℰℒ$ [13] and DL-Lite [10] which allow tractable and practically efficient reasoning with ontologies and databases that have 100,000s of entries, and on the other hand the development of very expressive description logics such as $𝒮ℛ𝒪ℐ𝒬(D)$ [40], the description logic underlying the OWL 2 DL standard. $𝒮ℛ𝒪ℐ𝒬(D)$ pushes the limit of expressivity without losing decidability of the logic, and is a logic for which reasoning becomes challenging: standard reasoning tasks for $𝒮ℛ𝒪ℐ𝒬(D)$-ontologies are N2ExpTime-complete [41]. Nonetheless, we have now highly optimized reasoning systems that can reason over large $𝒮ℛ𝒪ℐ𝒬(D)$ ontologies as they occur in the real world [61]. This is achieved by dedicated, highly optimized reasoning systems, and especially the latest developments, the reasoners Konclude [70] and Sequoia [26], are based on very complex algorithms that are hard to understand by non-experts.

A side effect of these developments is that preserving the transparency of reasoning with ontologies becomes more challenging. Understanding why a particular inference was performed on an ontology with 10,000s of statements, potentially due to complex interactions between expressive operators, is not possible without appropriate tool support. Motivated by this, a multitude of explanation methods for description logic has been developed, and the topic has recently gained increased attention again. The ontology editor Protégé comes with an in-built explanation functionality based on justifications [37], and recent developments such as Evee [5] and Evonne [59] offer more advanced explanation methods such as proofs, abduction and counterexamples.

The aim of this tutorial is to give an overview over the most important explanation methods for description logics, taking a closer look at a selection of methods and problems. In particular, we will look at methods for explaining positive entailments, that is, for explaining why a particular statement is logically entailed from a description logic knowledge base, and at methods for explaining negative entailments, that is, for explaining why a particular statement is not logically entailed.

We start with an introduction to description logics that are relevant to the tutorial. Methods for explaining positive entailments include justifications, proofs and Craig interpolation. Justifications have been the focus of an earlier tutorial of the summer school [32]. In Section 3, we give a more brief discussion on central algorithms and challenges. In Section 4, we then have a look at proofs based on inference rules as a more detailed type of explanation, providing a formal definition, and a discussion on how to compute explanations that optimize different optimality criteria. How to generate proofs without a dedicated set of inference rules is discussed in Section 6. One of these techniques is based on the notion of interpolation, which provides a different type of explanations on its own, which we discuss before in Section 5. Methods for explaining negative entailments include counterinterpretations and abduction. There are not a lot of works on counterinterpretations, which we mention briefly in Section 7, which otherwise focuses on abduction. Abduction in description logics is a topic that would fill a tutorial on its own, which is why we give a more superficial overview about the different challenges and variants.

Most of the methods discussed here are available in tools for end-users: justifications are integrated by default in the ontology editor Protégé [60], proofs are supported by the Elk Protégé plugin [42] as well as by the web application Evonne [59], and the Evee plugin for Protégé supports the different methods for proofs and abduction that are discussed here in more detail [5].

We recall the description logics (DLs) that are relevant to this tutorial. For a full introduction, we refer to the DL textbook [14].

The central construct of DLs are concept descriptions, simply called concepts in the following. Those concepts are constructed from two disjoint, countably infinite sets of concept names (${𝖭}_{𝖢}$) and role names (${𝖭}_{𝖱}$), which correspond to unary and binary predicates in first-order logic. In this chapter, we often call role names just roles. Concept and role names are used to construct the following concepts, where $A\in {𝖭}_{𝖢}$, $r\in {𝖭}_{𝖱}$ $C$ and $D$ are concepts:

• $\mathrm{■}$

  concept name $A$, top $\top$ and bottom $\perp$,

• $\mathrm{■}$

  complement $\neg C$,

• $\mathrm{■}$

  conjunction $C\sqcap D$,

• $\mathrm{■}$

  disjunction $C\bigsqcup D$,

• $\mathrm{■}$

  existential restriction $\exists r.C$,

• $\mathrm{■}$

  universal restriction $\forall r.C$.

While there are DLs with many more concept constructors, the preceding operators are available in the DL $𝒜ℒ𝒞$, which is why they are called $𝒜ℒ𝒞$ concepts. While many results in this paper apply to more expressive DLs, this is the most expressive DL we will use in this paper when the DL is relevant. By restricting the set of operators, we can define two more DLs that will be relevant: $ℰℒ$, which only has the operators concept name, top, conjunction and existential restriction, and $ℰ{ℒ}_{\perp }$, which in addition allow for bottom. Concepts are used to build concept inclusions (CIs) $C⊑D$ and equivalence axioms $C\equiv D$. A finite set of CIs and equivalence axioms is called a TBox, and intuitively specifies a terminology by putting different concepts in relation.

To also talk about specific facts, we use a set ${𝖭}_{𝖨}$ of countably infinite individual names disjoint from ${𝖭}_{𝖢}$ and ${𝖭}_{𝖱}$. We call concept names, role names and individual names jointly names. An ABox is then a finite set of concept assertions $C(a)$ and role assertions $r(a,b)$, where $C$ is a concept, $r\in {𝖭}_{𝖱}$ and $a$, $b\in {𝖭}_{𝖨}$. The union $𝒯\cup 𝒜$ of a TBox $𝒯$ and an ABox $𝒜$ is called a knowledge base (KB).¹¹1In the literature, sometimes knowledge bases are called ontologies, and sometimes only TBoxes are called ontologies. To avoid this confusion, we avoid the term ontology in most of the following paper. Observe that TBoxes and ABoxes are special cases of KBs. CIs, equivalence axioms, concept assertions and role assertions are collectively called axioms.

To define the meaning of concepts and axioms, we need to specify their semantics, which is usually done using interpretations. An interpretation is a tuple $𝒥=⟨{\mathrm{\Delta }}^{𝒥},{\cdot }^{𝒥}⟩$. The domain ${\mathrm{\Delta }}^{𝒥}$ is a finite set of elements, and the interpretation function ${\cdot }^{𝒥}$ gives meaning to concept names and roles, by assigning to each individual name $a\in {𝖭}_{𝖨}$ an element $a^{𝒥}\in {\mathrm{\Delta }}^{𝒥}$, to each concept name $A\in {𝖭}_{𝖢}$ a set $A^{𝒥}\subseteq {\mathrm{\Delta }}^{𝒥}$, and each role $r\in {𝖭}_{𝖱}$ to a binary relation $r^{𝒥}\subseteq {\mathrm{\Delta }}^{𝒥}\times {\mathrm{\Delta }}^{𝒥}$. The interpretation function is then lifted to concepts as follows:

The interpretation $𝒥$ then satisfies a CI $C⊑D$ if $C^{𝒥}\subseteq D^{𝒥}$, an equivalence axiom $C\equiv D$ if $C^{𝒥}=D^{𝒥}$, a concept assertion $C(a)$ if $a^{𝒥}\in C^{𝒥}$, and a role assertion $r(a,b)$ if $⟨a^{𝒥},b^{𝒥}⟩\in r^{𝒥}$. For an axiom $\alpha$, we write $𝒥\vDash \alpha$ to indicate that $𝒥$ satisfies $\alpha$. If $𝒥$ satisfies all axioms in a KB $𝒦$, we write $𝒥\vDash 𝒦$ and call $𝒥$ a model of $𝒦$. The notion of a model now lets us define logical entailments. In particular, $𝒦\vDash \alpha$ if $𝒥\vDash \alpha$ for all models $𝒥$ of $𝒦$. If an axiom $\alpha$ is satisfied in all interpretations, we call it a tautology. A KB that does not have any model is called inconsistent.

If $𝒦\vDash C⊑D$, we say that $C$ is subsumed by $D$, and if $𝒦\vDash C(a)$, we also say that $a$ is an instance of $C$.

Given a KB $𝒦$, we use $\text{ind}(𝒦)$ to refer to the individuals occurring in it. For a KB/axiom/concept $X$, we use $\text{sig}(X)$ to refer to its signature, i.e. the concept and role names occurring in $X$. If a KB/axiom/concept $X$ uses only names from a signature $\mathrm{\Sigma }$, i.e. a set of concept and role names, then we call $X$ a $\mathrm{\Sigma }$-KB/axiom/concept.

$ℰℒ$ and $𝒜ℒ𝒞$ form the basis of two families of DLs that extend those logics by additional expressivity. Nominals are concepts of the form $\{a\}$ that refer to a set containing just the individual name $a$, inverse roles are inverses of roles ($r^{-}$) that can be used instead of role names, functionality constraints allow to express that a role is functional, and role hierarchies are axioms of the form $r⊑s$ where $r$ and $s$ are roles. To describe which additional features a DL supports, we use calligraphic letters, which are then appended to the name of the DL: $𝒪$ stands for nominals, $ℐ$ for inverse roles, $ℱ$ for functionality constraints, $\mathscr{H}$ for role hierarchies. For example, $ℰℒℐ$ is a logic that extends $ℰℒ$ with inverse roles, and $𝒜ℒ𝒞\mathscr{H}𝒪$ is a logic that extends $𝒜ℒ𝒞$ with role hierarchies and nominals. To refer to the extension of a logic $ℒ$ with $\perp$, we use ${ℒ}_{\perp }$. A prominent example is $ℰ{ℒ}_{\perp }$ which extends $ℰℒ$ with bottom. For more information about these operators, we refer to [14].

$ℰℒ$ can be seen as the prototypical lightweight DL that admits tractable reasoning, while $𝒜ℒ𝒞$ is the prototypical more expressive DL for which reasoning is ExpTime-complete [14]. In fact, many logics of the $ℰℒ$ family allow for tractable reasoning: deciding entailment in any logic between $ℰℒ$ and $ℰℒ\mathscr{H}{𝒪}_{\perp }$ is PTime-complete [13]. Adding any of the operators disjunction, negation, value restriction or inverse roles on the other hand makes the logic ExpTime-hard [13]. Indeed, $ℰℒℐ$ allows to express a limited form of value restrictions, which are sometimes added to the language as syntactic sugar: specifically, $C⊑\forall r.D$ can be expressed as $\exists r^{-}.C⊑D$.

Justifications are the best investigated way of explaining entailments $𝒦\vDash \alpha$. As a means to understand and debug ontologies, they have been first proposed in [66], and since then many different approaches for computing them practically have been suggested [38, 16, 17, 15, 67].

The idea of justifications is quite simple:

Intuitively, a justification points to a minimal portion of the KB that is sufficient for the entailment, and can thus be considered ‘responsible’ for it. This is in particular relevant if we want to understand entailments from large and complex KBs. An example that is often given is that an older version of SNOMED CT entailed $\text{AmputationOfFinger}⊑\text{AmputationOfHand}$ [17]. This is clearly a bug, but to fix it, one would need to find the responsible axioms in a set of around 300,000 axioms, for which justifications can be very helpful. Since justifications point to axioms in the KB responsible for the entailment, the process of finding justifications is also called axiom pinpointing. Justifications are now a standard functionality of the ontology editor Protégé and of the Java OWL API.

There is a range of different approaches for computing justifications, many of which involve modifying the DL reasoner itself to track which axioms are used for determining the entailment. An alternative is the black box approach, where an existing reasoner is used as a black box without further modifications. Indeed, the black box approach implemented in [38] provides comparable performance to implementations of glass box approaches such as the one presented in [69]. The advantage of black box approaches is that they can be used with any reasoning system, and thus benefit from future developments into more efficient reasoning systems.

For the remainder of this section, fix a KB $𝒦$ and an axiom $\alpha$ s.t. $𝒦\vDash \alpha$. It is not hard to see that using a black box approach, we can compute a justification for $𝒦\vDash \alpha$ using at most polynomially many entailment checks: specifically, we can go through the axioms in $𝒦$ one after the other, and check for each whether removing it from $𝒦$ would still preserve the entailment, and remove it if this is not the case. The resulting set of axioms will be a justification (we cannot remove any axiom without breaking the entailment). From the perspective of computational complexity, we are often happy with such a polynomial procedure. However, from a practical perspective, we can do much better.

Algorithm 1 shows a simplified version of the black box algorithm presented in [38] for computing a justification for $𝒦\vDash \alpha$. The algorithm uses a divide and conquer strategy. The main idea is to fix a part ${𝒦}_f\subseteq 𝒦$ of the KB and only consider the remaining axioms in $𝒦\setminus {𝒦}_f$ when trying to find a minimal subset. Once this part of the KB has been minimized, we set the minimized part as fixed, and minimize the part of the KB that was previously fixed. Consequently, our algorithm uses an internal procedure that takes as arguments a fixed KB (${𝒦}_f$) and a varied part ${𝒦}_v$ that is to be optimized (Line 6). This procedure is called unless $\alpha$ is a tautology (Line 3), and we start with a fixed part that is empty (Line 5). If the variable part ${𝒦}_v$ has only one element, there is nothing to minimize, since we know that $\alpha$ is not a tautology, and we can directly return ${𝒦}_v$ (Line 8). Otherwise, we split ${𝒦}_v$ into two subsets ${𝒦}_1$ and ${𝒦}_2$ (Line 9) and check whether either of those sets is alone sufficient to produce the entailment. If it is, we can ignore the other set and continue (Line 11 and 13). If it is not (Line 14), we minimize ${𝒦}_1$ with fixed part ${𝒦}_f\cup {𝒦}_2$, obtaining the set ${𝒦}_1^{\prime }$ which is subsequently fixed to minimize ${𝒦}_2^{\prime }$. The union ${𝒦}_1^{\prime }\cup {𝒦}_2^{\prime }$ of the two minimized sets is then returned.

Justifications show which axioms from the KB are responsible for the entailment, but not how they are responsible. Proofs are more detailed explanations. Roughly, a proof is an acyclic, directed graph that shows how the entailment in question can be inferred in small steps from the axioms in the KB. Typically, proofs are generated using a set of sound inference rules that describe on an abstract level how to infer a new axiom from an existing set of axioms. Indeed, there are reasoning methods for DLs that use such a set of rules for reasoning [36, 68, 25, 26], though many established reasoners for more expressive DLs are based on other reasoning methods such as tableaux [69, 31, 70]. Using such inference rules not only as a mechanism for reasoning but also as a means to compute explanations seems natural. Indeed, one of the earliest works on explanations in DLs, which was published well before the first works on justifications, used proofs [58]. Elk is an efficient and widely used reasoner that supports an extension of $ℰℒ$, and that does use inference rules [43]. Figure 1 shows the inference rules used as they are presented in the paper for the Elk reasoner, restricted to $ℰℒ$.²²2In [43], the second premise of ${𝖱}_{⊑}$ is instead a side condition. In the context of this paper, this difference is not relevant. We call such a set of rules also calculus. The way to read these rules is as follows: if we have axioms as on top of the bar, then we can infer the axiom below the bar. Another calculus for $ℰℒ$ can be found in [14], which also presents the calculus for $ℰℒℐ$ shown in Figure 2. A calculus for $𝒜ℒ𝒞$ can be found in [68, 51], and for more expressive logics, rule sets can be found in [36, 25, 26, 57, 50]

As we have seen in Section 3, there can be exponentially many justifications for a given entailment. For proofs, there are even more degrees of freedom. To determine which proof is best to be used as an explanation, one can define quality criteria for proofs. The question is then how to compute a proof that is optimal with respect to this criterion. As one would expect, some criteria are harder to implement than others. We present a polynomial algorithm for computing proofs that are optimal for one such criterion, and then indicate how this quality criterion can be generalized to a larger class of quality criteria that admit tractable proof generation. But before we can even speak of the complexity of generating good proofs, we need a formal account on what proofs are and how they are generated.

Formally, we define proofs as a special case of derivation structures, which are hypergraphs labeled with axioms.

The edges $⟨S,v⟩\in E$ in the hypergraph correspond to the inference steps. Our conditions ensure that every inference is sound, and if some axiom is not the result of an inference, then it has to be from the KB. Note that in this setting, tautological axioms $\alpha$ can occur in edges $⟨\mathrm{\varnothing },\alpha ⟩$, and thus are also the result of an inference step.

Derivation structures are a generalization of proofs, and will help us in defining the problem of computing a proof. Proofs are defined as follows:

Note that the last condition does not require every axiom to occur only once in the proof, since different nodes can be labeled with the same axiom. The purpose of this condition is to make inferences in a proof unique, while a derivation structure may contain many possible inferences for the same node. Our definition is flexible enough to allow also for proofs that are not tree shaped, but instead correspond to directed acyclic graphs (DAGs). Indeed, this can be a more compact representation in many cases.

There are different ways in which proofs can be generated, and inference rules are just one possibility. In Section 6, we will see methods that work without a set of inference rules. In the following, we abstract away from the specific inference mechanism, and refer to a system that produce proofs as deriver. A deriver is a method $𝒟$ that takes as argument a pair $⟨𝒦,\alpha ⟩$ of a KB $𝒦$ and an entailment $\alpha$, and produces a derivation structure $𝒟(𝒦,\alpha )$ that contains all the inferences the deriver could perform towards proving $𝒦\vDash \alpha$. From this derivation structure, we then extract different proofs that optimizes some desired optimality criteria such as its size. For convenience, we assume that the cardinality of any inference step $(S,v)$ is polynomially bounded, and that no two nodes have the same label. For instance, the reasoner Elk only infers CIs over concepts that already occur as sub-concepts in the input. This means that for the corresponding deriver ${𝒟}_{\text{Elk}}$, the derivation structure ${𝒟}_{\text{Elk}}(𝒦,\alpha )$ is always of a size that is polynomially bounded by the size of $𝒦$ and $\alpha$. For languages for which entailment is in ExpTime, such as $𝒜ℒ𝒞$ and $ℰℒℐ$, derivers based on inference rules would instead produce derivation structures that can be exponential in the size of the input. This is for instance the case for the deriver based on the $ℰℒℐ$ calculus in Figure 2, whose derivation structures are exponentially bounded. In fact, derivers may even produce larger derivation structures or even unbounded derivation structures, which are discussed in [8].

We consider the complexity of computing a good proof for a given deriver. This complexity will be influenced by whether the size of the derivation structure is polynomially bounded or larger – for simplicity, we will in the following distinguish polynomial and exponential derivers, based on whether the size of derivation structures is polynomial or exponential in the size of the input. Computing the entire derivation structure $𝒟(𝒦,\alpha )$ is inefficient, which is why we instead see derivation structures as functions that 1) can return the node corresponding to an axiom $\alpha$ with $[𝒟(𝒦,\alpha )](\alpha )$, and 2) verify whether a given edge $(S,v)$ is part of a derivation structure ($𝒟(𝒦,\alpha )(S,v)=\text{true}$). In case the deriver is defined via a set of inference rules, these function calls correspond to checking whether an inference is valid according to this set of inference rules.

The first quality measure for proofs $𝒫=⟨V,E,\lambda ⟩$ uses its size, which is simply defined as $|E|$, the number of edges or inference steps in the proof. Rather than considering the problem of computing an optimal proof w.r.t. that measure, it is more convenient to instead look at the corresponding decision problem, which asks for a given entailment $𝒦\vDash \alpha$ and integer $n$ whether there exists a proof of size at most $n$. If $n$ is encoded in unary (e.g. using a sequence of $n$ symbols), this problem is clearly in NP, since we can always guess a proof of size $n$ in polynomial time and then just use the deriver to verify whether it is a valid proof. As shown in [2], we cannot do much better than that – computing optimal proofs is NP-hard already for the polynomial deriver ${𝒟}_{\text{Elk}}$. If we consider instead binary encoding of the bound $n$, and consider exponential derivers, we obtain NExpTime-completeness.

We know from an analysis with the Elk deriver on a larger corpus of OWL ontologies that proofs are rarely have a size beyond 20 [2, 1], which makes these complexities a bit less dramatic. Indeed, we are usually able to compute size-minimal proofs without a noticeable delay [1].

Finding proofs becomes tractable if we instead consider tree size. The tree size of a proof corresponds to the size of its tree unravelling, which is actually how proofs are represented e.g. in the ontology editor Protégé. To avoid having to introduce tree unravellings and since it will make our life easier when we later generalize to a larger class of quality measures, we define tree size directly on proofs. Given a proof $𝒫=⟨V,E,\lambda ⟩$ with final conclusion on the node $v_0$, we call the unique inference $(S_0,v_0)\in E$ the final inference in $𝒫$. Given $v\in V$, we refer by ${𝒫}_v$ as the proof below $v$, which is the sub-proof of $𝒫$ that has $v$ as final conclusion.

Note that the case where there is no $(S,v)\notin V$ corresponds to the case where $v\in 𝒦$.

Proofs based on inference calculi provide very detailed explanations, which may not always be desired. Before we continue on the topic of proofs and consider less detailed variants, we discuss explanations using Craig interpolation, and start with entailments of CIs.

Craig interpolation has first been investigated in the context of classical logics [24, 52]. The classical definition is as follows: Given two formulas $\phi$ and $\psi$ s.t. $\phi \vDash \psi$, a Craig interpolant for $\phi \vDash \psi$ is a formula $\chi$ s.t. $\phi \vDash \chi$, $\chi \vDash \psi$ and $\text{sig}(\chi )\subseteq \text{sig}(\phi )\cap \text{sig}(\psi )$. We can see $\chi$ as an explanation of the entailment using only the common terms of $\phi$ and $\psi$. If we lift this idea to complex DL concepts, such interpolants can be used to explain positive entailments of CIs.

In the presence of a TBox, using as signature the common terms of $C$ and $D$ makes less sense. Consider that we want to explain CIs of the form $A⊑B$, where $A$ and $B$ are concept names. A meaningful concept to to explain this entailment will have to use names other than $A$ and $B$. Consequently, concept interpolation is defined with the signature as additional parameter.

Whether a concept interpolant exists or not depends on the signature as well as on the DL. If a DL has the so-called Craig interpolation property (CIP), then interpolant existence can be polynomially reduced to entailment. A DL has the CIP if whenever for two ontologies ${𝒪}_1$, ${𝒪}_2$ and concepts $C$, $D$, we have ${𝒪}_1\cup {𝒪}_2\vDash C⊑D$, then there exists a concept $E$ using only names that occur in ${𝒪}_1$, $C$ as well as in ${𝒪}_2$, $D$. If we consider the simple ontology $𝒪=\{A_1⊑A_2$, $A_2⊑A_3\}$, with concepts $C=A_1$ and $D$, it is a simple exercise the verify that this property indeed holds for any ${𝒪}_1$, ${𝒪}_2$ s.t. $𝒪={𝒪}_1\cup {𝒪}_2$. For example, setting ${𝒪}_1=\{A_1⊑A_2\}$ and ${𝒪}_2=\{A_2⊑A_3\}$ yields $E=A_2$. Indeed, this works for any CI entailed by ontologies formulated in $ℰℒ$ or $𝒜ℒ𝒞$, as well as for their extensions with transitivity, inverse roles and functionality restrictions, because those are the logics that have the CIP.

To see how this property can be used to decide concept interpolants, assume a DL has the CIP and fix $𝒯$, $\mathrm{\Sigma }$, $C$ and $D$ s.t. $𝒯\vDash C⊑D$. We construct a new TBox ${𝒯}_{\mathrm{\Sigma }}$ and a new concept $D_{\mathrm{\Sigma }}$ from $𝒪$ and $D$ by replacing every non-$\mathrm{\Sigma }$ symbol uniformly by a fresh symbol. It is shown in [11, Lemma 5.3] that then a concept $\mathrm{\Sigma }$-interpolant for $𝒯\vDash C⊑D$ exists iff we have $𝒯\cup {𝒯}_{\mathrm{\Sigma }}\vDash C⊑D_{\mathrm{\Sigma }}$.

As soon as we add nominals or role hierarchies to our DL, it loses the CIP, and concept interpolation becomes much harder: for both $𝒜ℒ𝒞𝒪$ and $𝒜ℒ𝒞\mathscr{H}$, deciding the existence of interpolants ins coNExpTime-complete, for $𝒜ℒ𝒞\mathscr{H}𝒪$, it is even 2ExpTime-complete [11].

While some papers describe algorithms [71, 65], currently, there are no dedicated implementations available that can compute concept interpolants in practice. Before we address this problem, we consider interpolation on the level of KBs.

Similar to concept interpolants, KB interpolants can be used to explain entailments. Specifically, we can explain $𝒦\vDash C⊑D$ by providing a KB interpolant for $𝒦\vDash \{C⊑D\}$. Moreover, we can reduce concept interpolation to KB interpolation:

Proofs based on calculi give a very fine-grained explanation, where each inference follows a systematic and transparent principle, the inference rule. In order to compute proofs for a DL $ℒ$, we need to implement a calculus for $ℒ$ that is sound and complete. While there do exist now calculi for a range of DLs, the majority of implemented reasoning systems for expressive DLs is not based on such a set of rules.

There are other methods for computing proof-like, more detailed explanations that do not depend on a set of inference rules, and instead use reasoning methods as black boxes. One of them are justification-based proofs [39], and another one are elimination proofs [5, 2], which combine KB interpolants with justifications.

Justification-based proofs use a very flexible definition, and can be computed with any reasoner as black box. The general idea is to incrementally refine a justification-based explanation by adding layers of intermediate steps. To create an intermediate layer for a justification $𝒥$ for an entailment $\alpha$, we generate a set $𝔄$ of axioms over the signature of $𝒥$, based on a set of predefined syntactic axiom patterns. An example of such a set of axiom patterns is $\{X⊑Y$, $X⊑\exists R.Y$, $X\sqcap Y⊑Z\}$, which is then instantiated by replacing $X$, $Y$, $Z$ by all concept names in $𝒥$, and $R$ by all possible role names in $𝒥$. We remove from $𝔄$ all axioms that are not entailed by $𝒥$, resulting in a new set $𝔅$, and compute for each $\beta \in 𝔅$ a justification ${𝒥}_{\beta }$ for $𝒥\vDash \beta$, which then constitutes an inference step ${𝒥}_{\beta }\Rightarrow \beta$. Furthermore, every justification ${𝒥}_{𝔅}$ for $𝔅\vDash \alpha$ constitutes an inference step ${𝒥}_{𝔅}\Rightarrow \alpha$. We use some evaluation function to rank the inference steps generated in this way, and extract a proof for $𝒪\vDash \alpha$ by selecting one inference ${𝒥}_{𝔅}\Rightarrow \alpha$, and for every $\beta \in {𝒥}_{𝔅}$, one inference step ${𝒥}_{\beta }\Rightarrow \beta$. This construction results in a proof in which every inference step corresponds to a pair of a justification and an entailment. We can further refine each such inference step by applying the same procedure again.

Of all the explanation techniques for positive entailments discussed in this chapter, justification-based proofs are the most flexible: they make no assumptions on the reasoner used, they can be equipped with any set of axiom patterns and use arbitrary quality criteria to select the best inference step. Moreover, the incremental approach allows to flexibly refine proofs on demand. This amount of freedom is at the same time the main limitation of this approach. Since it is essentially a brute-force which considers all possible axioms that fit a defined shape, justification-based proofs are computationally expensive.

Elimination proofs follow a similar idea, but use KB interpolants as the intermediate layers. In particular, we use a sequence ${𝒦}_1$, $\mathrm{\dots }$, ${𝒦}_n$ of KBs s.t. ${𝒦}_n=\{\alpha \}$, ${𝒦}_1$ is a justification for $𝒦\vDash \alpha$, and each ${𝒦}_i$ is a ontology ${\mathrm{\Sigma }}_i$-interpolant for $𝒦\vDash \alpha$, where the signatures ${\mathrm{\Sigma }}_i$ are such that for , ${\mathrm{\Sigma }}_i=\text{sig}({𝒦}_{i-1})\setminus \{X_i\}$ for some concept or role name $X_i\in \text{sig}({𝒦}_{i-1})$. Intuitively, each KB in the sequence ‘eliminates’ a name from the preceding one. We have already seen such a sequence of interpolants in Figure 3. To extract a proof from this sequence of interpolants, we again use justifications. Namely, for every and $\beta \in ({𝒦}_i\setminus {𝒦}_{i-1})$, we produce an inference step ${𝒥}_{\beta }\to \beta$, where ${𝒥}_{\beta }$ is a justification for ${𝒪}_{i-1}\vDash \beta$.

Those proofs are called elimination proofs because in principle, each inference step may eliminate a name from its premises. In particular, such an elimination step has the form ${\alpha }_1,\mathrm{\dots },{\alpha }_n\Rightarrow \beta$, where $\{{\alpha }_1$, $\mathrm{\dots }$, ${\alpha }_n\}$ contains a name $X$ that does not occur in $\beta$. The intuition is that $\beta$ is inferred through an inference on $X$. As it is described here, the method will still produce inference steps where the signature is not changed for a specific axiom. We can however easily avoid this by skipping over inference steps that do not eliminate a name.

Having discussed several methods for explaining positive entailments, we now turn to the problem of explaining missing entailments, e.g. of explaining cases where $𝒦\vDash ̸\alpha$. Here, one can follow two approaches: 1) using counterinterpretations and 2) using abduction.

The idea of counterinterpretations follows directly from the formal definition of non-entailment: if $𝒦\vDash ̸\alpha$, then there exists a model $𝒥$ of $𝒦$ s.t. $𝒥\vDash ̸\alpha$. The model $𝒥$ is a counterinterpretation that explains $𝒦\vDash ̸\alpha$. Reasoning methods such as tableaux, but also the completion method for $ℰℒ$ presented in [13] are indeed model construction methods, and can as such be used to create such counterinterpretations. To make them more useful as explanations, one can highlight elements in the model that are relevant to the non-entailment. [9] discusses different types of counterinterpretations, including also a contrastive variant that explains missing entailments of the form $𝒦\vDash A⊑B$ by providing a counterinterpretation that contrasts an instance of $A$ with an instance of $B$, highlighting what is missing for $A$.

Because there is not a lot of literature on counterinterpretations, we focus in the following on the other way of explaining missing entailments, which is using abduction. Abduction explains a missing entailment by pointing out what is missing in the KB for the entailment to hold. In particular, using abductive reasoning for a missing entailment $𝒦\vDash ̸\alpha$, we compute a set $\mathscr{H}$ of axioms s.t. $𝒦\cup \mathscr{H}\vDash \alpha$. The set $\mathscr{H}$ can be either used directly as explanation, or together with an explanation method for positive entailments to connect $\mathscr{H}$ with $\alpha$ and $𝒦$. Abduction is not only useful for explaining missing entailments. The original motivation is to provide rational explanations for observations that cannot be logically deduced based on our knowledge. An example of abductive reasoning in daily life is that we observe that a street is wet, and come to the conclusion that it must have rained, since this would explain why the street is wet. Usually, abduction allows for more than one possible explanation: another one would be that someone spilled water on the street.

Formally, we can define abduction as follows:

This definition captures the bare minimum of what we would require of a hypothesis, which is usually not enough to get a useful explanation. In addition to consistency, we often also find the following criteria (e.g. [30]):

While these criteria have their motivation, we may usually need further restrictions. Indeed, as the following example illustrates, we may often require additional user input to distinguish usefull hypotheses from less usefull ones.

As the example illustrates, we cannot distinguish between useful and useless abductive explanations solely based on the logical structure, but may need additional user input. One solution is to simply accept that some hypotheses will be not be helpful to the user, and always compute several alternatives to choose from. Since there can be many options, we may still need to put restrictions or sort solutions based on optimality criteria. Another solution is to let the user specify beforehand what kind of hypotheses they expect, for instance by letting them restrict the signature to be used.