Abduction in EL via Translation to FOL ?

Abstract

We present a technique for performing TBox abduction in the description logic EL. The input problem is converted into first-order formulas on which a prime implicate generation technique is applied, then EL hypotheses are reconstructed by combining the generated positive and negative implicates. Description logic (DL) ontologies are used to formalize terminological knowledge in diverse areas such as medicine, biology, or the semantic web. Common reasoning tasks for ontologies are subsumption checking, which is to decide whether one description of a concept generalizes another, and classification, which is to compute the entire subsumption hierarchy of an ontology, that is, the set of all subsumption relationships that hold between atomic concepts in the ontology. Both problems can nowadays be computed rather efficiently using highly optimized description logic reasoners [24]. Modern ontologies can become very large and complex: for instance, the medical ontology SNOMED CT4 contains over 350,000 statements, while the Gene Ontology GO defines over 50,000 concepts. But even for less complex ontologies, it is easy to introduce bugs, and possible inferences may not always be transparent to ontology users and engineers. Correspondingly, services for explaining those inferences can be very helpful. Typical techniques for explaining why subsumption can be inferred include justifications [4, 16, 27] and proofs [1, 2], both of which have been included in the popular ontology development tool Prot´eg´e [17, 18]. In order to explain why a subsumption relationship cannot be inferred, one can use abduction [21]. The general setup in abduction is that we have an

Keywords

• Abduction
• Description Logic EL
• Prime Implicates
• Firstorder Logic

Introduction

input consisting of a knowledge base K and some logical statement α—the observation—that is not logically entailed by K. The aim is then to compute a hypothesis, a set of axioms whose addition to K would result in the entailment α. This way, the hypothesis not only provides for a possible explanation, it also offers a fix to repair the entailment in case it is supposed to hold. One way to avoid trivial hypotheses (such as the axiom α itself) is to restrict solutions syntactically, for instance by specifying a signature of predicates that can be used in the solution [ 20, 22 ].

In the context of DLs, depending on the shape of the observation to be explained, abduction can be classified into different categories: – In concept abduction observation and hypothesis are DL concepts. That means we are looking for a concept that is subsumed by a user-given concept (with respect to an ontology) [ 5 ]. – In ABox abduction, observations and hypotheses have the form of ABoxes, that is, they describe facts, which is the more typical scenario for diagnosis [ 6–9, 11, 15, 19, 20, 25, 26 ]. – In TBox abduction, observation and hypothesis consist of TBox axioms, which can be used to find fixes for missing subsumption relationships [ 10,28 ]. – Finally, in knowledge base abduction, the most general form, both hypotheses and observations can be arbitrarily composed of TBox and ABox axioms [ 13, 22 ].

We are interested in explaining missing subsumption relationships, which is what

is done by TBox abduction, in which background knowledge, observation, and hypothesis all consist of TBox axioms, that is, DL axioms expressing subsumption relationships between concepts. Optionally, a set of abducible concepts can be specified as part of the input, of which every hypothesis needs to be composed.

We work in the lightweight DL EL, used in many large scale ontologies [3].

TBox abduction has been considered before, albeit in different settings.

In [ 10 ], instead of a set of abducibles, a set of justification patterns is given, which is a set of syntactical patterns that hypotheses have to fit in. In contrast, [ 28 ] generalises both this work and the one in [ 10 ], in that it uses an arbitary oracle function to decide whether a solution is admissible or not (which may use abducibles, justification patterns, or something else). The work in [ 28 ] also considers EL, and abduction under various minimality notions such as subset minimality and size minimality. It is there shown that deciding the existence of hypotheses is tractable, while for certain minimality criteria, it can become coNP-complete. In addition to the theoretical results, the authors of [ 28 ] present practical algorithms, and an evaluation of an implementation. Different to our approach, they use an external DL reasoner to decide entailment relationships.

In contrast, we present an approach that directly exploits first-order reasoning,

and thus has the potential to be generalisable to more expressive DLs.

The TBox abduction technique we present proceeds in three steps. The first

step is the translation of the abduction problem into a first-order formula Φ.

Then, we compute the prime implicates of Φ, that is, a minimal set of logical consequences of Φ that subsume all other consequences of Φ. In the final step, we

C1 v C2

T Φ Σ

PIgΣ+(Φ)

PIgΣ−(Φ) translation

PI generation recombination

S construct TBoxes that are hypotheses of the original abduction problem, from the prime implicates of Φ.

Figure 1 illustrates this process with some more details. The translation to first-order relies on the assumption that the TBox T is normalized and this results in a set of definite Horn clauses Φ. Prime implicate (PI) generation in first-order logic can be done with an off-the-shelf tool [ 12, 23 ] or, in our case, by slightly altering a resolution-based theorem prover, such as included in the SPASS theorem prover [ 29 ]. Since the input is Horn, PIgΣ+(Φ), the set of ground positive prime implicates of Φ, contains only unit clauses. The recombination step looks at the negative ground prime implicates in PIgΣ−(Φ) one after the other and attempts to match each literal in one such clause with clauses in PIgΣ+(Φ). If this succeeds, the result is a solution to the original problem. We denote S the set of all solutions obtained in this way.

In this paper, we describe in details the translation and recombination steps

and prove that the S obtained in that way contains only solutions to the original problem. 2

Preliminaries

We begin with an introduction of the relevant notions, first in EL, then in first

order logic. 2.1

The Description Logic EL

Let NC and NR be pair-wise disjoint, countably infinite sets of respectively atomic

concepts and roles. Generally, we use letters A, B, E, F ,... for atomic concepts, and r for roles, possibly annotated, letters C, D, possibly annotated, denote EL concepts, built according to the syntax rule

C ::=

> | A | C u C | ∃r.C .

We use d{C1, . . . , Cm} as abbreviation for C1 u . . . u Cm, and identify the empty conjunction (when m = 0) with >. An EL TBox T is a finite set of concept inclusions (CIs) of the form C v D. We use C ≡ D as abbreviation for {C v D,

D v C}. The semantics of EL is defined as usual using DL interpretations, which are tuples I = (ΔI , ·I ) made of a domain ΔI and an interpretation function

·I that maps atomic concepts A ∈ NC to sets AI ⊆ ΔI and roles r ∈ NR to relations rI ⊆ ΔI × ΔI . The interpretation function ·I is extended to complex concepts as follows:

>I = ΔI (C u D)I = CI ∩ DI (∃r.C)I = {d ∈ ΔI | ∃(d, e) ∈ rI s.t. e ∈ CI } We say that I satisfies a CI C v D, in symbols I |= C v D, if and only if CI ⊆ DI , and if I satisfies all axioms in a TBox T , we write I |= T and call I a model of T . If a CI C v D is satisfied in every model of T , we write T |= C v D and say that C v D is entailed by T . In this case, we say that C is subsumed by D and call C a subsumee of D and D a subsumer of C.

Note that, if we identify NC with the set of unary predicates and NR with the

set of binary predicates, I is a classical first-order structure for those predicates.

We can thus define satisfaction of first-order formulas in DL interpretations as usual, and also relate first-order formulas with CIs and TBoxes via the usual entailment relation.

2.2

Abduction in EL

The abduction problem we are concerned with in this paper is the following.

Definition 1. Given a TBox T , a set of atomic concepts Σ ⊆ NC and a concept inclusion C1 v C2, called the observation, where C1 and C2 are atomic concepts and T 6|= C1 v C2, the corresponding TBox abduction problem, denoted by the tuple hT , Σ, C1 v C2i, is to find a TBox

H ⊆ {Ai1 u · · · u Ain v Bi1 u · · · u Bim | {Ai1 , . . . , Ain , Bi1 , . . . , Bim } ⊆ Σ} where m > 0, n ≥ 0 and such that T ∪ H |= C1 v C2 and T ∩ H = ∅. Such a solution H to the abduction problem is called a hypothesis.

As an example, suppose we have a TBox T = {C1 v ∃r.A, ∃r.B v C2}. For the abduction problem hT , {A, B}, C1 v C2i, the set H = {A v B} is a solution since T ] H |= C1 v C2. Note that since EL TBoxes are always consistent, the consistency condition usually required on T ∪ H is not needed in our setting. 2.3

Prime Implicate Generation in First Order Logic We consider first-order logic with unary and binary predicates, which we identify with the corresponding elements in NC and NR. Let V be a set of variables, and ΣFOL be a signature such that ΣFOL = NC ∪ NR, where NC and NR are the sets of EL atomic concepts and roles, used as unary and binary predicate symbols respectively. Furthermore, let F be a set of function symbols, which includes a set C of constants as nullary function symbols. A term t, possibly annotated, is either a variable x ∈ V, a constant c ∈ C, or of the form f (t1, . . . , tm), where f is an m-ary function symbol and t1, . . ., tm are terms. Atoms are either of the form A(t1) or r(t1, t2), where t1 and t2 are terms. Literals are either atoms κ (positive literals) or negated atoms ¬κ (negative literals). Clauses, denoted ϕ with possible annotations, are disjunctions of literals implicitly universally quantified. Formulas, denoted Φ, are described using universal and existential quantification, conjunction, disjunction, and negation. For convenience, by abuse of notation, we may sometimes identify sets of formulas or clauses with the conjunction over those.

Skolemization removes existentially quantified variables from formulas in the

usual way: for each existentially quantified variable, it adds a fresh function with variable arguments taken from the universally quantified variables outside the scope of the variable under consideration (if no such variables exist, we use a nullary function, ie. a constant). For example, ∀x.¬A(x) ∨ ∃y.r(x, y) is

Skolemized into ∀x.¬A(x) ∨ r(x, f (x)). Here, we assume that the formula is in

negation normal form, that is, every negation symbol occurs only in front of an atom. Furthermore, we assume that such Skolem functions are taken from a set NS not in the signature. In our context, we only require a single Skolem constant, namely sk0, since Skolemized atoms, literals, and clauses range over

Skolem terms either built over a given variable or sk0 instead of ranging over

variables. We let Tx(NS) be the set of Skolem terms built on x, where x is either sk0 or a variable in V.

Since we only consider formulas over unary and binary predicates, they can

be satisfied by DL interpretations as defined above, understood naturally as first-order structures. We call interpretations I with ΔI = Tsk0 (NS) Herbrand interpretations, which for convenience, by abuse of notation, we may treat as sets of ground atoms s.t. A(t) ∈ I if and only if t ∈ AI and r(t, t0) ∈ I if and only if (t, t0) ∈ rI .

Definition 2 (Prime Implicate). Given a set of clauses Φ, a clause ϕ is an implicate of Φ if Φ |= ϕ. Additionally, ϕ is a prime implicate of Φ if for any other implicate ϕ0 of Φ s.t. ϕ0 |= ϕ, it also holds that ϕ |= ϕ0. Given a Skolemized Φ, the set PIgΣ+(Φ) is the set of all positive ground prime implicates of Φ and the set PIgΣ−(Φ) is the set of all negative ground prime implicates where all of the predicate symbols belong to Σ.

Example 3. Given Φ as follows: Φ = {A(sk0), ¬B(sk0), ¬A(x) ∨ r(x, sk(x)), ¬A(x) ∨ E(sk(x)),

¬G(x) ∨ ¬r(x, y) ∨ ¬E(y) ∨ B(sk0)}, where sk0 is a constant and sk is a function symbol, the ground prime implicates of Φ are PIgΣ+(Φ) = {A(sk0), E(sk(sk0))} and PIgΣ−(Φ) = {¬B(sk0), ¬G(sk0) ∨ ¬E(sk(sk0))}. They are implicates because all of them are consequences of Φ (they are entailed by Φ). Moreover, these implicates are also prime implicates because it is not possible to obtain an implicate of Φ by removing a literal from one of them.

In some cases, the set of prime implicates can even be infinite.

Example 4. Consider Φ0, a slight variation on Φ from the previous example, where E(sk(x)) is replaced by A(sk(x)), so that:

Φ0 = {A(sk0), ¬B(sk0), ¬A(x) ∨ r(x, sk(x)), ¬A(x) ∨ A(sk(x)), Whereas the negative ground prime implicates are unchanged (PIgΣ−(Φ0) = PIgΣ−(Φ)), there are now infinitely many positive ground prime implicates, because PIgΣ+(Φ0) contains A(sk0), A(sk(sk0)), A(sk(sk(sk0))) . . . 3

From EL to FOL

We assume the EL TBox in the input to be in normal form as defined in [3],

which means that every CI is of the form A v B, A1 u A2 v B, ∃r.A v B or A v ∃r.B, where r ∈ NR and A, A1, A2, B ∈ NC ∪ {>}. Every EL TBox can be transformed in polynomial time into this normal form through the introduction of fresh concept names. This transformation preserves all entailments in the signature of the original ontology, even after the addition of CIs (assuming the same CIs are added also to the input ontology, and they don’t use any of the introduced concept names). Note that this transformation extends the signature, and thus potentially the solution space of the abduction problem: to avoid this, we may simply intersect the set of abducibles Σ with the signature of the original input ontology.

At the level of TBoxes, we use the standard, semantics-preserving translation

from EL to FOL [ 3 ].

Definition 5 (TBox translation). The function π translates concepts into first-order formulas: π(>, x) = true π(A, x) = A(x) π(∃r.C, x) = ∃y.(r(x, y) ∧ π(C, y)) π(C u D, x) = π(C, x) ∧ π(D, x) We lift π to concept inclusions with: π(C v D) = ∀x.¬π(C, x)∨π(D, x). Finally, we lift π to TBoxes with:

π(T ) = {π(C v D) | C v D ∈ T }. If T is in normal form, π(T ) contains only axioms of the following shapes: shapes from CIs with > : ∀x.true ∀x.¬A(x) ∨ ∃y.r(x, y), ∀x.¬A1(x) ∨ ¬A2(x) ∨ B(x), ∀x.¬(∃y.r(x, y) ∧ A(y)) ∨ B(x), ∀x.¬A(x) ∨ ∃y.(r(x, y) ∧ B(y)).

In practice, since the symbol > will be preprocessed, only the four last forms are

relevant in our work.

The function π is semantics-preserving in the following sense:

Theorem 6 (First-Order Semantics Preservation [ 3 ]). For any EL TBox T and possibly complex concepts C and D, T |= C v D if and only if π(T ) |= π(C v D).

The translation of a TBox abduction problem, built on top of the standard

TBox translation, is less straightforward.

The translation Π(T , C1 v C2) of hT , Σ, C1 v C2i to first-order logic is the

Skolemization of

π(T ] T 0) ∧ ¬π(C1 v C20) where sk0 is used as the unique fresh Skolem constant such that the Skolemization of ¬π(C1 v C20) results in {C1(sk0), ¬C20(sk0)}, and where several other things happen that are explained in the following paragraphs.

Before Skolemization, T is first preprocessed by replacing every occurrence

of the concept > in T with that of the fresh atomic concept A> and we add ∃r.A> v A> and B v A> to T for every role r and atomic concept B. This simulates for A> the implicit property that C v > holds for any C no matter what the TBox is. In particular, this ensures that whenever there is a positive prime implicate B(t) or r(t, t1), A>(t) also becomes a prime implicate.

Finally, we define T 0 by renaming all atomic concepts A from T using fresh

symbols A0. Notice that this is also done for C2, renamed to C20 in Π(T , C1 v C2).

Thanks to this encoding trick, the inferences can be traced back from C1(sk0)

or from ¬C20(sk0) and do not interfere with each other, making it easier to relate ground prime implicates and concept inclusions and capturing interesting solutions that would otherwise not be found.

We now look at a complete encoding example in details.

Example 7. Suppose given T over the signature where NC = {A, B, C1, C2, E, F, G, H} and NR = {r1, r2} as follows.

T = {C1 v ∃r1.A, C1 v B, C1 v ∃r2.G, ∃r2.E v B, ∃r1.F v H, B u H v C2}

Consider the abduction problem hT , NC, C1 v C2i. Preprocessing the > symbol turns T into:

and the renaming of atomic concepts produces:

T 0 = {C10 v ∃r1.A0, C10 v B0, C10 v ∃r2.G0,

∃r2.E0 v B0, ∃r1.F 0 v H0, B0 u H0 v C20} ]{∃r1.A0> v A0>, ∃r2.A0> v A0>} ]{J v A0> | J ∈ {A0, B0, C10, C20, E0, F 0, G0, H0}} The translation of T results in ΦT , the Skolemization of π(T ): ΦT = {¬C1(x) ∨ r1(x, sk1(x)), ¬C1(x) ∨ A(sk1(x)), ¬C1(x) ∨ B(x), ¬C1(x) ∨ r2(x, sk2(x)), ¬C1(x) ∨ G(sk2(x)), ¬r2(x, y) ∨ ¬E(y) ∨ B(x), ¬r1(x, y) ∨ ¬F (y) ∨ H(x), ¬B(x) ∨ ¬H(x) ∨ C2(x), ]{¬r1(x, y) ∨ A>(y) ∨ A>(x), ¬r2(x, y) ∨ A>(y) ∨ A>(x)} ]{¬J (x) ∨ A>(x) | J ∈ {A, B, C1, C2, E, F, G, H}} ΦT 0 , the Skolemization of T 0, is similar except that the atomic concepts are renamed. Finally, Π(T , C1 v C2) = ΦT ∪ ΦT 0 ∪ {C1(sk0), ¬C20(sk0)}.

Let us now look in more detail at the reason for replacing > with A>. First, remember that > is not considered as a part of NC and represents an empty conjunction. Since it is translated to true in first-order logic, it never appears in a translated formula, as can be seen in the text following Definition 5. However, our technique is only looking for the ground prime implicates. There are many other non-ground prime implicates that are generated and that we only use in the hope of finally grounding them. It would not be practical to have to sort out the non-ground PIs due to the > symbol from the rest of them. Consider the following example.

Example 8. Given Σ = {A, E, F, G} and the TBox

T = {> v ∃r1.F, C1 v ∃r2.A, A v ∃r3.G, ∃r2.E v J1, ∃r1.J1 v J0, ∃r2.> v J3, J0 u J3 v C2}

Some of the ground PIs of Π(T , C1 v C2) are as follows:

– A(sk2(sk0)), F (sk1(sk2(sk0))), G(sk3(sk2(sk0))) are positive PIs, – ¬E0(sk1(sk2(sk0))) ∨ ¬A0>(sk3(sk2(sk0))) is a negative PI, where the Skolem functions sk1, sk2, and sk3, are from the Skolemization of r1, r2, and r3 respectively in the first three axioms.

Let us take a close look at the reason why F (sk1(sk2(sk0))) is an implicate.

We observe that A(sk2(sk0)) is obtained as a consequence of the presence of

C1 v ∃r2.A in T . Thanks to the addition of A v A> to T , A>(sk2(sk0)) is also

an implicate. Finally due to the presence of the renaming of > v ∃r1.F in T , namely A> v ∃r1.F , the clause F (sk1(sk2(sk0))) is also an implicate. With a direct translation of >, we would only be able to derive F (sk1(x)) and there would be no way to obtain a ground implicate from this clause.

Similarly, it is only thanks to the presence of ∃r3.A> v A> in T that the

prime implicate ¬E0(sk1(sk2(sk0))) ∨ ¬A0>(sk3(sk2(sk0))) can be deduced. 4

Building EL hypotheses from prime implicates We use the ground prime implicates of Φ = Π(T , C1 v C2) to produce solutions to the abduction problem hT , Σ, C1 v C2i in EL. To do this, we identify subsumers of C1 and subsumees of C2 that can be generated from the ground prime implicates in Φ, and that can be matched with each other based on the Skolem terms they contain.

Definition 9 (Solution reconstruction). Let hT , Σ, C1 v C2i be an abduction problem and let Φ = Π(T , C1 v C2), and assume there are prime implicates {A1(t1), . . . , An(tn)} ⊆ PIgΣ+(Φ) and ¬B10(t01) ∨ . . . ∨ ¬Bm0(t0m) ∈ PIgΣ−(Φ) such that {ti}i∈[1,n] = {t0i}i∈[1,m]. We can then obtain a hypothesis H for the abduction problem

H = {l1(t) v l2(t) | t ∈ L and T 6|= l1(t) v l2(t)}, such that – L = {ti}i∈[1,n] = {t0i}i∈[1,m], – l1(t) = d{A | A(t) ∈ {A1(t1), . . . , An(tn)}}, and – l2(t) = d{B | B0(t) ∈ {B10(t01), . . . , Bm0(t0m)}}.

We denote by S(Φ, Σ) the set containing all such H.

Example 10. From Example 7,

T = { C1 v ∃r1.A, C1 v B,

C1 v ∃r2.F, B u ∃r1.E v C2, ∃r1.A> v A>, ∃r2.A> v A>} ]{J v A> | J ∈ {C1, C2, A, B, E, F, G}}.

Consider the prime implicates from Π(T , C1 v C2)

– {B(sk0), A(sk1(sk0))} ⊆ PIgΣ+(Φ), and – ¬B0(sk0) ∨ C0(sk1(sk0)) ∈ PIgΣ−(Φ).

From the Skolem term sk0 and sk1(sk0), we have l1(sk0) v l2(sk0) = B v B and l1(sk1(sk0)) v l2(sk1(sk0)) = A v C respectively. However, B v B is a tautology. Consequently, H = {A v C} is one possible hypothesis. Theorem 11. Given a TBox abduction problem hT , Σ, C1 v C2i, and denoting Φ the set Π(T , C1 v C2), the set S(Φ, Σ) contains only hypotheses for the abduction problem.

Proof. Let ΦT denote the Skolemization of π(T ). If ¬B10(t01) ∨ . . . ∨ ¬Bm0(t0m) ∈

PIgΣ−(Φ), then ΦT ∪ {C1(sk0), ¬C2(sk0)} |= ¬B1(t1) ∨ . . . ∨ ¬Bm(tm) because using, e.g., resolution, any inference to derive the primed disjunction can be imitated without primes. Moreover, A(t) ∈ PIgΣ+(Φ) implies A(t) ∈ PIgΣ+(ΦT ∪ {C1(sk0)}) since only non-primed clauses are relevant to entail positive literals. Thus ΦT ∪ {C1(sk0)} |= A1(t1) ∧ . . . ∧ An(tn).

By combining the two results for compatible positive and negative clauses, we obtain ΦT ∪ {C1(sk0), ¬C2(sk0)} |= π(l1(t), t) ∧ ¬π(l2(t), t) for all t ∈ L where L, l1(t) and l2(t) are as defined in Definition 9. In turn, this implies ΦT ∪ {C1(sk0), ¬C2(sk0)} |= ∃x.(π(l1(t), x) ∧ ¬π(l2(t), x)) for all t ∈ L. Thus ΦT ∪ {C1(sk0), ¬C2(sk0)} ∪ {∀x.(¬π(l1(t), x) ∨ π(l2(t), x)) for all t ∈ L}. Hence, for any hypothesis H ∈ S(Φ, Σ), we know that ΦT ∪ {C1(sk0), ¬C2(sk0)} ∪ π(H) is unsatisfiable. Consequently, because Skolemization is satisfiability-preserving, π(T ) ∪ ¬π(C1 v C2) ∪ π(H) is also unsatisfiable, hence π(T ) ∪ π(H) |= π(C1 v C2). By Theorem 6, this in turn means that T ∪ H |= C1 v C2. tu 5

Conclusion

We have introduced a technique to compute hypotheses to solve TBox abduction

problems in EL. This technique turns the input TBox into a first-order formula, of which the ground prime implicates can be used to build hypotheses answering the problem.

We have not shown the prime implicate computation step itself for two reasons. First, existing tools such as SOLAR [ 23 ] and GPiD [ 12 ] can compute prime implicates automatically in first-order logic. Second, there is an issue with the termination of such tools for problems with cyclic dependencies in the CIs, e.g., such that T |= A v ∃r.A, because in that case, the set of prime implicates may be unbounded. However, there exists only a finite number of hypotheses to be found and we conjecture that prime implicates with polynomial nesting depth of Skolem terms are sufficient for finding all relevant hypotheses. We plan to verify this conjecture and implement a prime implicate generation tool on top of SPASS [ 29 ] as the next step of this work.

An orthogonal concern that we are currently addressing is to relate the ob

tained hypotheses with connection-minimality [ 14 ], a notion we recently introduced to characterize solutions to the abduction problem in EL that we find particularly interesting, because they connect the subsumers of C1 to the subsumees of C2 in a less contrived way than other solutions. We believe that the present technique is sound and complete with respect to finding connectionminimal hypotheses, but that remains to be formally proved.

Finally, as our approach works by generating ground prime implicates start

ing from a set of ground literals, it should also be possible to use it for a mix of ABox and TBox abduction, where our background knowledge consists of a

DL knowledge base containing both a TBox and ground facts, the observation is another set of ground facts, and we are looking for hypotheses in the form of a TBox. This would have applications for TBox learning from data.

References

1. Alrabbaa , C. , Baader , F. , Borgwardt , S. , Koopmann , P. , Kovtunova , A. : Finding small proofs for description logic entailments: Theory and practice . In: Albert, E. , Kovacs , L . (eds.) LPAR- 23 : 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning . EPiC Series in Computing, vol. 73 , pp. 32 - 67 . EasyChair ( 2020 ). https://doi.org/10.29007/nhpp

2. Alrabbaa , C. , Baader , F. , Borgwardt , S. , Koopmann , P. , Kovtunova , A. : Finding good proofs for description logic entailments using recursive quality measures . In: Platzer, A. , Sutcliffe , G . (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15 , 2021 , Proceedings. Lecture Notes in Computer Science , vol. 12699 , pp. 291 - 308 . Springer ( 2021 ). https://doi.org/10.1007/978-3- 030 -79876-5 17

3. Baader , F. , Horrocks , I. , Lutz , C. , Sattler , U. : An Introduction to Description Logic . Cambridge University Press ( 2017 ). https://doi.org/10.1017/9781139025355

4. Baader , F. , Suntisrivaraporn , B. : Debugging SNOMED CT using axiom pinpointing in the description logic EL+ . In: Proc. of the 3rd Conference on Knowledge Representation in Medicine (KR-MED '08): Representing and Sharing Knowledge Using SNOMED. CEUR-WS , vol. 410 ( 2008 ), http://ceur-ws. org/ Vol- 410 /Paper01. pdf

5. Bienvenu , M. : Complexity of abduction in the EL family of lightweight description logics . In: Proceedings of KR 2008 . pp. 220 - 230 . AAAI Press ( 2008 ), http://www. aaai.org/Library/KR/2008/kr08- 022 .php

6. Calvanese , D. , Ortiz , M. , Simkus , M. , Stefanoni , G. : Reasoning about explanations for negative query answers in DL-Lite . J. Artif. Intell. Res . 48 , 635 - 669 ( 2013 ). https://doi.org/10.1613/jair.3870

7. Ceylan , I˙.I˙. , Lukasiewicz , T. , Malizia , E. , Molinaro , C. , Vaicenavicius , A. : Explanations for negative query answers under existential rules . In: Calvanese, D. , Erdem , E. , Thielscher , M. (eds.) Proceedings of KR 2020 . pp. 223 - 232 . AAAI Press ( 2020 ). https://doi.org/10.24963/kr.2020/23

8. Del-Pinto , W. , Schmidt , R.A. : ABox abduction via forgetting in ALC . In: The Thirty-Third AAAI Conference on Artificial Intelligence , AAAI 2019 . pp. 2768 - 2775 . AAAI Press ( 2019 ). https://doi.org/10.1609/aaai.v33i01. 33012768

9. Du , J. , Qi , G. , Shen , Y. , Pan , J.Z. : Towards practical ABox abduction in large description logic ontologies . Int. J. Semantic Web Inf. Syst . 8 ( 2 ), 1 - 33 ( 2012 ). https://doi.org/10.4018/jswis.2012040101

10. Du , J. , Wan , H. , Ma, H.: Practical TBox abduction based on justification patterns . In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence . pp. 1100 - 1106 ( 2017 ), http://aaai.org/ocs/index.php/AAAI/AAAI17/ paper/view/14402

11. Du , J. , Wang , K. , Shen , Y. : A tractable approach to ABox abduction over description logic ontologies . In: Brodley, C.E. , Stone , P. (eds.) Proceedings of the TwentyEighth AAAI Conference on Artificial Intelligence . pp. 1034 - 1040 . AAAI Press ( 2014 ), http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8191

12. Echenim , M. , Peltier , N. , Sellami , Y. : A generic framework for implicate generation modulo theories . In: Galmiche, D. , Schulz , S. , Sebastiani , R . (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018 , Held as Part of the Federated Logic Conference , FloC 2018 , Oxford, UK, July 14-17 , 2018 , Proceedings. Lecture Notes in Computer Science , vol. 10900 , pp. 279 - 294 . Springer ( 2018 ). https://doi.org/10.1007/978-3- 319 -94205-6 19, https://doi.org/ 10.1007/978-3- 319 -94205-6 19

13. Elsenbroich , C. , Kutz , O. , Sattler , U. : A case for abductive reasoning over ontologies . In: Proceedings of the OWLED'06 Workshop on OWL: Experiences and Directions ( 2006 ), http://ceur-ws. org/ Vol- 216 /submission 25.pdf

14. Haifani , F. , Koopmann , P. , Tourret , S. : Introducing connection-minimal abduction for EL ontologies . XLoKR workshop ( 2021 )

15. Halland , K. , Britz , K. : ABox abduction in ALC using a DL tableau . In: 2012 South African Institute of Computer Scientists and Information Technologists Conference, SAICSIT '12 . pp. 51 - 58 ( 2012 ). https://doi.org/10.1145/2389836.2389843

16. Horridge , M. : Justification Based Explanation in Ontologies . Ph.D. thesis , University of Manchester, UK ( 2011 ), https://www.research.manchester.ac.uk/portal/ files/54511395/FULL TEXT.PDF

17. Horridge , M. , Parsia , B. , Sattler , U. : Explanation of OWL entailments in protege 4 . In: Bizer, C. , Joshi , A . (eds.) Proceedings of the Poster and Demonstration Session at the 7th International Semantic Web Conference (ISWC2008) , Karlsruhe, Germany, October 28 , 2008 . CEUR Workshop Proceedings , vol. 401 . CEUR-WS.org ( 2008 ), http://ceur-ws. org/ Vol- 401 /iswc2008pd submission 47.pdf

18. Kazakov , Y. , Klinov , P. , Stupnikov , A. : Towards reusable explanation services in protege . In: Artale, A. , Glimm , B. , Kontchakov , R . (eds.) Proceedings of the 30th International Workshop on Description Logics , Montpellier, France, July 18- 21 , 2017 . CEUR Workshop Proceedings , vol. 1879 . CEUR-WS.org ( 2017 ), http: //ceur-ws. org/ Vol-1879/paper31.pdf

19. Klarman , S. , Endriss , U. , Schlobach , S.: ABox abduction in the description logic ALC . Journal of Automated Reasoning 46 ( 1 ), 43 - 80 ( 2011 ). https://doi.org/10.1007/s10817-010-9168-z

20. Koopmann , P. : Signature-based abduction with fresh individuals and complex concepts for description logics . In: Zhou, Z . (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021 , Virtual Event / Montreal, Canada, 19 - 27 August 2021 . pp. 1929 - 1935 . ijcai. org ( 2021 ). https://doi.org/10.24963/ijcai. 2021 /266

21. Koopmann , P. : Two ways of explaining negative entailments in description logics using abduction . In: Explainable Logic-Based Knowledge Representation (XLoKR 2021 ) ( 2021 )

22. Koopmann , P. , Del-Pinto , W. , Tourret , S. , Schmidt , R.A. : Signature-based abduction for expressive description logics . In: Calvanese, D. , Erdem , E. , Thielscher , M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning , KR 2020 . pp. 592 - 602 . AAAI Press ( 2020 ). https://doi.org/10.24963/kr.2020/59

23. Nabeshima , H. , Iwanuma , K. , Inoue , K. , Ray , O. : SOLAR: an automated deduction system for consequence finding . AI Commun . 23 ( 2-3 ), 183 - 203 ( 2010 ). https://doi.org/10.3233/AIC-2010-0465, https://doi.org/10.3233/AIC-2010-0465

24. Parsia , B. , Matentzoglu , N. , Gonc¸alves, R.S., Glimm , B. , Steigmiller , A. : The OWL reasoner evaluation (ORE) 2015 competition report . J. Autom. Reason . 59 ( 4 ), 455 - 482 ( 2017 ). https://doi.org/10.1007/s10817-017-9406-8

25. Pukancova´, J. , Homola , M. : Tableau-based ABox abduction for the ALCHO description logic . In: Proceedings of the 30th International Workshop on Description Logics ( 2017 ), http://ceur-ws. org/ Vol-1879/paper11.pdf

26. Pukancova´, J. , Homola , M.: The AAA ABox abduction solver . Ku¨nstliche Intell . 34 ( 4 ), 517 - 522 ( 2020 ). https://doi.org/10.1007/s13218-020-00685-4

27. Schlobach , S. , Cornet , R.: Non-standard reasoning services for the debugging of description logic terminologies . In: Gottlob, G. , Walsh , T. (eds.) Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003 ). pp. 355 - 362 . Morgan Kaufmann, Acapulco, Mexico ( 2003 ), http://ijcai.org/Proceedings/03/Papers/053.pdf

28. Wei-Kleiner , F. , Dragisic , Z. , Lambrix , P. : Abduction framework for repairing incomplete EL ontologies: Complexity results and algorithms . In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence . pp. 1120 - 1127 . AAAI Press ( 2014 ), http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/ view/8239

29. Weidenbach , C. , Schmidt , R.A. , Hillenbrand , T. , Rusev , R. , Topic , D. : System description: Spass Version 3.0 . In: Pfenning, F . (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20 , 2007 , Proceedings. Lecture Notes in Computer Science , vol. 4603 , pp. 514 - 520 . Springer ( 2007 ). https://doi.org/10.1007/978-3- 540 -73595- 3 38, https://doi.org/10.1007/978-3- 540 -73595-3 38