An abductive diference between two quantified ABoxes consists of the knowledge that needs to be added to the first to make the second entailed. We describe a generic construction of such diferences and show that all minimal abductive diferences can be computed in exponential time. Moreover, we present first results when ontologies are taken into account. Abduction in logic aims at explaining observations by computing the missing parts that need to be added to the knowledge base in order to make the observation entailed [1]. This problem has received considerable attention, specifically for concept abduction [2, 3], ABox abduction [4-10], TBox abduction [11, 12], general purpose methods [13-17], and other aspects [18, 19]. We consider the problem of abduction with quantified ABoxes (qABoxes), which are ABoxes with existentially quantified variables. These variables stand for “anonymous individuals” that do not have specific names and are only described by their properties and relations to other individuals. More specifically, we assume a knowledge base consisting of a qABox and an ontology, and further an observation in form of another qABox - the goal is to compute an explanation, which is a qABox that needs to be added to the knowledge base to make the observation entailed. Of particular interest are those explanations that contain only a minimal amount of additional knowledge, which we call minimal. For example, the qABox ∃ ∅. {tom : Cat, jerry : Mouse} has no variables and expresses that Tom is a cat and Jerry is a mouse. Further consider as observation the qABox ∃ {}. {tom : Cat, (tom, ) : chases, : Mouse}, which has one variable and expresses that Tom is a cat that chases a mouse. Without an ontology, there are two minimal explanations. Since it is already known in the first qABox that Tom is a cat, this part of the observation must not be included in any minimal explanation. Moreover, it could be that Tom is specifically chasing Jerry, which is already known to be a mouse - the according minimal explanation is ∃ ∅. {(tom, jerry) : chases}. The other minimal explanation is ∃ {}. {(tom, ) : chases, : Mouse}. When we additionally take the ℰℒ ontology {Cat ⊑ ∃ chases. Mouse} into account, which expresses that every cat chases some mouse, then the only minimal explanation is the empty qABox. Without ontology, there might be exponentially many minimal explanations and, by means of a generic construction, we show that all minimal explanations can be computed in exponential time. With an ontology, there might exist infinitely many minimal explanations, even in ℰℒ.
The Description Logic ℰℒ. We recall the DL ℰℒ, on which all other DLs in the ℰℒ family are based. In order to structurally describe the domain of interest, we fix a signature consisting of individuals, atomic concepts, and roles. Concepts are built by ::= ⊤ | | ⊓ | ∃ . where ranges over all atomic concepts and over all roles. We call ⊤ the top concept, ⊓ the conjunction of and , and ∃ . the existential requirement on with intent . An ontology is a finite set of concept inclusions (CIs) ⊑ involving concepts , . An assertion box (ABox) is a finite set of concept assertions (CAs) : and role assertions (RAs) (, ) : involving individuals , , concepts , and roles . A knowledge base (KB) consists of an ABox and an ontology.
ℰℒ has a model-based semantics. An interpretation ℐ consists of a non-empty set Dom(ℐ), called domain, and an interpretation function · ℐ that sends every individual to an element ℐ of the domain, every atomic concept to a subset ℐ of the domain, and every role to a binary relation ℐ on the domain. The interpretation function is extended to all concepts as follows: ⊤ℐ := Dom(ℐ), ( ⊓ )ℐ := ℐ ∩ ℐ , and (∃ . )ℐ := { | there is such that (, ) ∈ ℐ and ∈ ℐ }. An interpretation ℐ satisfies (or is a model of) a CI ⊑ if ℐ ⊆ ℐ , a CA : if ℐ ∈ ℐ , and a RA (, ) : if (ℐ , ℐ ) ∈ ℐ . Furthermore, ℐ is a model of an ontology if ℐ satisfies all CIs in , a model of an ABox if ℐ satisfies all CAs and RAs in , and a model of a KB ∪ if ℐ is a model of and .
If and are any of the syntatic objects defined above, then we say that entails , written |= , if every model of is a model of . We often write |= instead of ∪ |= , and then we say that entails w.r.t. . Furthermore, we say that a concept is subsumed by a concept w.r.t. an ontology , written ⊑ , if |= ⊑ . We further say that and are equivalent, written ≡ , if they entail each other. Entailment, equivalence, and subsumption in ℰℒ can be decided in polynomial time [20].
Quantified ABoxes. A quantified ABox (qABox) ∃ . consists of a finite set of variables and an ABox , called matrix, in which variables may be used in place of individuals. Since the variables are existentially quantified, they are “anonymous individuals” whose names are not exposed. Each variable in and each individual (in the signature, but not necessarily occurring in the matrix) is an object of ∃ . , and Obj(∃ . ) is the set of all objects of ∃ . . A KB can now also consist of a qABox and an ontology. A qABox is in normal form if only atomic concepts are used in the assertions. Each qABox can be transformed into normal form by representing complex concepts by the use of variables — e.g. ∃ ∅. { : ( ⊓ ∃ . ), : ⊤} has the normal form ∃ {}. { : , (, ) : , : }. Throughout this paper we assume all qABoxes are in normal form. The union of two qABoxes is ∃ . ∪ ∃ . ℬ := ∃ ( ∪ ). ( ∪ ℬ) where w.l.o.g. ∩ = ∅ (otherwise variables need to be renamed). Over signatures consisting of constants, unary predicates, and binary predicates only, relational structures with constants, databases with nulls, primitive-positive (pp) formulas in first-order logic, conjunctive queries (CQs), and qABoxes are syntatic variants of each other, i.e. semantically the same, but used for diferent purposes or in diferent fields of research.
Consider an interpretation ℐ and a qABox ∃ . . A variable assignment sends each variable in to an element of the domain of ℐ. The extended interpretation ℐ[] coincides with ℐ but its interpretation function · ℐ[] additionally maps every variable according to . We say that ℐ is a model of ∃ . if there is a variable assignment such that ℐ[] is a model of .
Entailment between two qABoxes is an NP-complete problem, but whether a qABox entails an ABox can be decided in polynomial time. Without an ontology, ∃ . ℬ |= ∃ . if. there is a homomorphism from ∃ . to ∃ . ℬ, which is a function ℎ that sends each individual to itself and each variable in to an object of ∃ . ℬ such that applying ℎ within any assertion in yields an assertion in ℬ. More formally, a homomorphism from ∃ . to ∃ . ℬ is a mapping ℎ : Obj(∃ . ) → Obj(∃ . ℬ) that fulfills the following conditions: (H1) ℎ() = for each individual , (H2) if : ∈ , then ℎ() : ∈ ℬ, (H3) if (, ) : ∈ , then (ℎ(), ℎ()) : ∈ ℬ.
With an ontology , entailment can be decided by first saturating ∃ . ℬ by means of (i.e. compute the chase or the universal model) and then checking for a homomorphism from ∃ . to the saturation [21, 22].
We start with a general definition of abductive diferences for qABoxes.
Definition 1. Consider an observation in form of a qABox ∃ . and further consider a KB consisting of a qABox ∃ . ℬ and an ontology . An abductive diference (or explanation) of ∃ . w.r.t. ∃ . ℬ and is a qABox ∃ . such that ∃ . ℬ ∪ ∃ . |= ∃ . . Moreover, ∃ . is minimal if there is no other abductive diference ∃ ′. ′ with ∃ . |= ∃ ′. ′ but ∃ ′. ′ ̸|= ∃ . .
In the above definition the ontology can be any finite set of first-order formulas without free variables (i.e. first-order sentences). If the given KB consisting of ∃ . ℬ and is inconsistent (i.e. has no model and thus entails everything), then the empty qABox is the only minimal explanation. Non-trivial minimal explanations can only be obtained when the observation does not already follow from the KB, in which case the KB must be consistent. Obviously, ∃ . is always an abductive diference but in general not a minimal one since parts of ∃ . might already occur in ∃ . ℬ, as the following example shows.
Example 2. W.r.t. the KB ∃ ∅. {tom : Cat, jerry : Mouse}, the observation ∃ {}. {tom : Cat, (tom, ) : chases, : Mouse} has two minimal explanations: ∃ {}. {(tom, ) : chases, : Mouse} and ∃ ∅. {(tom, jerry) : chases}.
The next example illustrates that, without an ontology, there can be at least exponentially many minimal explanations. A matching upper bound will be proven in Section 4, viz. that, up to equivalence, the set of all minimal explanations can be computed in exponential time.
Example 3. For each number ≥ 1 , consider the observation ∃ {1, . . . , }. {1 : 1, . . . , : , (1, 2) : , (2, 3) : , . . . , (−1 , ) : } and the KB ∃ ∅. {(, ) : , (, ) : , (, ) : , (, ) : }. Then, in order to obtain a minimal explanation, we can choose between : and : for each ∈ {1, . . . , }, i.e. every qABox ∃ ∅. {1 : 1, . . . , : } with ∈ {, } is a minimal explanation. Thus there are at least 2 minimal explanations. (There might be further minimal explanations not considered here.)
The third example below shows that an ontology can enforce infinitely many non-equivalent minimal explanations.
Example 4. The observation {alice : Human} has infinitely many minimal explanations w.r.t. the KB consisting of the ℰℒ ABox {bob : Human} and the ℰℒ ontology {∃ hasParent. Human ⊑ Human}. For each number > 0, the qABox ∃ {1, . . . , }. {(alice, 1) : hasParent, (1, 2) : hasParent, · · · , (−1 , ) : hasParent, (, bob) : hasParent} is a minimal abductive diference. Also the observation itself is a minimal explanation. At the same time this example shows that, in general, the size of minimal abductive diferences is not bounded.
We first consider the case without ontology and show how the set of all minimal explanations can be computed in exponential time, up to equivalence. This case is relevant when no ontology is used in the application, but also serves as a foundation for the general case (see Lemma 12 for details). Recall from Example 2 that the computation of minimal explanations must take into account the parts of the observation that are already entailed by the KB. These parts can be pinpointed by means of so-called partial homomorphisms.
In order to understand partial homomorphisms, consider an observation ∃ . , a KB ∃ . ℬ, and an explanation ∃ . . By Definition 1 the observation is entailed by the union of the KB and the explanation, and so there is a homomorphism ℎ from ∃ . to ∃ . ℬ ∪ ∃ . . When we now restrict ℎ to all objects that are mapped to objects of the KB, i.e. we consider the partial function : Obj(∃ . ) →↦ Obj(∃ . ℬ) where () := ℎ() if ℎ() ∈ Obj(∃ . ℬ) and () is undefined otherwise, then this restriction pinpoints the part of the observation that is already known in the KB. Since to construct the union of the KB and the explanation their variable sets and are made disjoint, assertions in involving objects mapped to variables in must be present in ℬ (since these variables occur only in ℬ), but those assertions in involving objects mapped to individuals can be in ℬ or (since individuals can occur in ℬ as well as ). Thus, the partial homomorphism is only required to preserve assertions in involving an object that sends into , see the precise definition below.
Definition 5. A partial homomorphism from a qABox ∃ . to another qABox ∃ . ℬ is a partial function : Obj(∃ . ) →↦ Obj(∃ . ℬ) that satisfies the following: (PH1) () = for each individual , (PH2) if : ∈ such that ∈ Dom() and () ∈ ,1 then () : ∈ ℬ,2 (PH3) if (, ) : ∈ s.t. ∈ Dom() and () ∈ , then ∈ Dom() and ((), ()) : ∈ ℬ, (PH4) if (, ) : ∈ s.t. ∈ Dom() and () ∈ , then ∈ Dom() and ((), ()) : ∈ ℬ. We say that is trivial if Dom() ∩ = ∅.
On the other hand, the remaining part of the observation, which is mapped by the homomorphism ℎ to the explanation, is the unknown part. This means that we can take the partial homomorphism and extend it to a homomorphism to the union of the KB and the explanation. Motivated by this, we will next develop a canonical construction of explanations. To this end, we exploit the partial homomorphism to define a so-called -diference ∃ . ∖ ∃ . ℬ (see Definition 6), which is specifically defined so that can be extended to a homomorphism from the observation to the union of the KB and this -diference. It then follows that this -diference is an explanation as well (see Lemma 7). This construction is canonical in the sense that the -diference is entailed by the initially considered explanation (see Lemma 8).
Definition 6. Let be a partial homomorphism from ∃ . to ∃ . ℬ, where w.l.o.g. ∩ = ∅. The -diference ∃ . ∖ ∃ . ℬ is the qABox with variable set ∖ Dom() and matrix { () : | : ∈ , ∈ Dom(), and () : ̸∈ ℬ }3 ∪ { ((), ()) : | (, ) : ∈ , , ∈ Dom(), and ((), ()) : ̸∈ ℬ }, where the partial function : Obj(∃ . ) →↦ Obj(∃ . ) is defined by • () := for each ∈ ∖ Dom(), • () := () for each ∈ Dom() such that () an individual, • () is undefined for each ∈ Dom() such that () is a variable (in ).
The -union ∃ . ℬ ∪ ∃ . is ∃ . ℬ ∪ (∃ . ∖ ∃ . ℬ).
Simply put, the -diference consists of those assertions in the observation that are not already present in the KB. To account for objects mapped to individuals by the partial homomorphism , each occurrence of such an object must be replaced by the respective individual (), but the remaining variables occurring in these assertions need not be renamed — this is achieved by means of the mapping . In particular, we have ∈ Dom() if. ̸∈ Dom() or () ̸∈ , the union of Dom() and Dom() equals Obj(∃ . ), and the intersection of Dom() and Dom() consists of all objects such that () is an individual, but for these and coincide. We will furthermore see in Lemma 7 below that extending by yields a homomorphism from the observation to the union of the KB and the -diference.
Obviously, the size of the -diference is bounded by the size of the observation since every assertion in the former is obtained from an assertion in the latter. It follows that each -diference has polynomial size. In the case where is trivial, we have ∃ . ∖ ∃ . ℬ = ∃ . ( ∖ ℬ) and thus ∃ . ℬ ∪ ∃ . = ∃ . ℬ ∪ ∃ . , i.e. the set-theoretic union coincides with the -union. 1Note that then ∈ . 2We denote the domain of by Dom(), which is the set of all elements for which is defined. 3If () is no individual, then () : cannot be in ℬ anyway since and are disjoint.
Lemma 7. For each partial homomorphism from ∃ . to ∃ . ℬ, the -diference an abductive diference of ∃ . w.r.t. ∃ . ℬ. ∃ . ∖ ∃ . ℬ is Proof. We need to verify that the -union entails ∃ . . To this end, we extend to a (non-partial) homomorphism from ∃ . to ∃ . ℬ ∪ ∃ . . Since Dom()∪Dom() = Obj(∃ . ) and () = () for each ∈ Dom() ∩ Dom(), the union ∪ is a function from Obj(∃ . ) to Obj(∃ . ℬ ∪ ∃ . ). It remains to show that ∪ is a homomorphism. (H1) For each individual , we have () = by (PH1). Moreover, Definition 6 yields () = () and thus ( ∪ )() = . (H2) Let : ∈ .
• If ∈ Dom() and () ∈ , then (): ∈ ℬ by (PH2) and thus the matrix of ∃ . ℬ ∪ ∃ . contains ( ∪ )() : .
• If ∈ Dom() and () ̸∈ , then () is an individual and thus equals (). According to the definition of the -diference, () : is either in ℬ or in the matrix of the -diference, and thus contained in the matrix of the -union.
• If ̸∈ Dom(), then cannot be an individual and thus ∈ . It follows that ∈ Dom() and () = . The definition of the -diference ensures that the matrix of the -union contains () : . (H3) Similar for (, ) : ∈ .
• If ∈ Dom() and () ∈ , then ∈ Dom() and ((), ()) : ∈ ℬ by (PH3) and thus the matrix of ∃ . ℬ ∪ ∃ . contains (( ∪ )(), ( ∪ )()) : .
• Analogously for ∈ Dom() and () ∈ by (PH4).
• If , ∈ Dom() and (), () ̸∈ , then () and () are individuals and thus equal to () and, respectively, (). According to the definition of the -diference, ((), ()) : is either in ℬ or in the matrix of the -diference, and thus contained in the matrix of the -union.
• If , ̸∈ Dom(), then , cannot be individuals and thus , ∈ . It follows that , ∈ Dom() where () = and () = . The definition of the -diference ensures that the matrix of the -union contains ((), ()) : .
• Assume ∈ Dom() and () ̸∈ , i.e. () is an individual. Further let ̸∈ Dom(), i.e. cannot be an individual and thus ∈ . It follows that , ∈ Dom() where () = () and () = . Since ∈ and ∩ = ∅, the matrix ℬ cannot contain ((), ()) : and so this assertion is contained in the matrix of the -diference, and therefore also in the matrix of the -union.
• The remaining case with ̸∈ Dom(), ∈ Dom(), and () ̸∈ is analogous. Lemma 8. Every abductive diference entails a -diference.
Proof. Consider an abductive diference ∃ . , i.e. ∃ . ℬ ∪ ∃ . |= ∃ . and so there is a homomorphism ℎ from ∃ . to ∃ . ℬ ∪ ∃ . . W.l.o.g. let the variable sets , , be pairwise disjoint. First, we obtain a partial homomorphism by restricting ℎ to all objects of ∃ . mapped to some object of ∃ . ℬ, i.e. we verify that the partial function with () := ℎ() whenever ℎ() ∈ Obj(∃ . ℬ) is a partial homomorphism. (PH1) Since each individual is an object of ∃ . ℬ, we have () = ℎ() = . (PH2) Let : ∈ with ∈ Dom() and () ∈ . Since () = ℎ(), ℎ() : ∈ ℬ ∪ , and ∩ = ∅, we infer that () : ∈ ℬ. (PH3) Assume (, ): ∈ with ∈ Dom() and () ∈ . For () = ℎ(), (ℎ(), ℎ()): ∈ ℬ ∪, and ∩ = ∅, it follows that ℎ() is an object of ∃ . ℬ and ((), ℎ()): ∈ ℬ. Thus ∈ Dom() where () = ℎ(), and ((), ()) : ∈ ℬ. (PH4) Consider (, ) : ∈ with ∈ Dom() and () ∈ . Similarly as in the previous case we infer that ℎ() is an object of ∃ . ℬ and (ℎ(), ()) : ∈ ℬ, and further that ∈ Dom() where () = ℎ(), hence ((), ()) : ∈ ℬ.
Next, we show that there is a homomorphism from the -diference to ∃ . . We already know that ℎ is a homomorphism from ∃ . to ∃ . ℬ ∪ ∃ . , and further that the -diference is obtained from a sub-qABox of ∃ . by replacing, for every object with () an individual, each occurrence of by ().
This replacement is formally done by the mapping , i.e. the objects in the -diference have the form () as per Definition 6. We infer that ℎ(()) = ℎ() for each variable ∈ ∖ Dom() and ℎ(()) = ℎ(()) = () = ℎ() for each ∈ Dom() with () an individual. Thus, if an assertion () : is in the -diference, then : is in , and thus ℎ() : is in ℬ ∪ , and similarly for the other assertions ((), ()) : . It follows that the restriction of ℎ to the objects of the -diference is a homomorphism from the -diference to ∃ . ℬ ∪ ∃ . .
It remains to show that this restriction of ℎ is already a homomorphism to ∃ . . For each variable ∈ ∖ Dom(), we have ℎ(()) = ℎ() (see above) and ℎ() ̸∈ Obj(∃ . ℬ) (by definition of ), and thus ℎ() must be a variable of ∃ . , i.e. ℎ() ∈ . Moreover, for each object ∈ Dom() with () an individual, we have ℎ(()) = ℎ(()) = () = (). (H2) Thus, every assertion () : in the -diference is mapped by ℎ to the assertion () : , which must be contained in since ℎ(()) ∈ if ∈ ∖ Dom(), and otherwise Definition 6 ensures that this assertion is not in ℬ. (H3) Each assertion ((), ()) : in the -diference is treated similarly. If or is in ∖ Dom(), then ℎ(()) ∈ or, respectively, ℎ(()) ∈ , and thus ℎ must map this assertion to one in . Otherwise, Definition 6 ensures that ℎ does not map this assertion to one in ℬ, hence ℎ must map it to one in . (H1) Every individual is an object of the -diference and we have ℎ() = by (H1). Thus also the considered restriction of ℎ sends to itself.
The important corollary to the previous lemma is that the set of all -diferences contains all minimal explanations, up to equivalence.
Proposition 9. Every minimal abductive diference of ∃ . w.r.t. ∃ . ℬ is equivalent to a -diference ∃ . ∖ ∃ . ℬ for some partial homomorphism from ∃ . to ∃ . ℬ.
Proof. Let ∃ . be a minimal abductive diference. By Lemma 8 there is a partial homomorphism such that its -diference is entailed by ∃ . . Moreover, the -diference is also an abductive diference by Lemma 7. Since ∃ . is minimal, it follows that, in the opposite direction, also ∃ . is entailed by the -diference. Thus, ∃ . is equivalent to the -diference.
We can finally formulate our main result regarding the computation of minimal explanations. Example 3 yields that the below complexity result cannot be improved in general.
Theorem 10. Consider an observation ∃ . and a KB ∃ . ℬ. Up to equivalence, each minimal explanation has polynomial size and the set of all minimal explanations can be computed in exponential time. Proof. By Proposition 9 every minimal explanation is equivalent to a -diference, and each -diference has polynomial size, which yields the first claim. Further recall from Lemma 7 that every -diference is an explanation. Thus, it sufices to compute all minimal -diferences to obtain, up to equivalence, all minimal explanations. A procedure that computes them all works as follows.
1. Enumerate all partial functions from Obj(∃ . ) to Obj(∃ . ℬ), which are exponentially many and each of them has polynomial size. 2. Retain only the partial homomorphisms. To this end, check whether each partial function satisfies
Definition 5, which can be done in polynomial time for a single function. 3. Compute all -diferences from the partial homomorphisms as per Definition 6, which needs polynomial time for one -diference. 4. Retain only the minimal -diferences. For this purpose, consider all pairs of -diferences, determine which entails which, and remove the one that entails but is not entailed by the other. Since every -diference has polynomial size and qABox entailment is NP-complete, identifying all minimal explanation terminates in exponential time. 4.1. Computing Partial Homomorphisms with Query Answering Systems We have seen in Theorem 10 that we obtain all minimal explanations from the exponentially many partial homomorphisms. Instead of enumerating all partial homomorphisms in the naïve manner as in the proof of that theorem, we can rather reuse existing algorithms and implementations for enumerating (non-partial) homomorphisms, viz. by employing of-the-shelf query answering systems.
To this end, we extend the given KB ∃ . ℬ to a qABox ∃ * . ℬ* such that there is a correspondence between the partial homomorphisms from the observation ∃ . to the KB ∃ . ℬ and the (ordinary) homomorphisms from ∃ . to ∃ * . ℬ* . We achieve this by adding further assertions to which all parts of the observation can be mapped that are not mapped by the partial homomorphisms since they are missing from the KB. More specifically, we add all possible concept and role assertions involving individuals, and we further add a fresh variable * that is asserted to “everything” in the sense that we add all possible concept and role assertions involving this new variable * and possibly any individual (see this precise definition below).
Then, we identify the observation ∃ . with the conjunctive query to be answered (but we treat all variables in as answer variables, i.e. we drop the existential quantification) and further we identify ∃ * . ℬ* with the database over which the query is to be evaluated. Therefore each certain answer represents a homomorphism from ∃ . to ∃ * . ℬ* and vice versa.
Lemma 11. Consider qABoxes ∃ . and ∃ . ℬ, and define ∃ * . ℬ* by * := ∪ {*} and ℬ* := ℬ ∪ { : | is an individual and is a atomic concept } ∪ { (, ) : | , are individuals and is a role } ∪ { (, *) : , (*, ) : | is an individual and is a role } ∪ { * : | is a atomic concept } ∪ { (*, *) : | is a role }. 1. If is a partial homomorphism from ∃ . to ∃ . ℬ, then ℎ with ℎ() := () for each ∈ Dom() and ℎ() := * otherwise is a homomorphism from ∃ . to ∃ * . ℬ* . 2. If ℎ is a homomorphism from ∃ . to ∃ * . ℬ* , then with () := ℎ() for each with ℎ() ̸= * and () undefined otherwise is a partial homomorphism from ∃ . to ∃ . ℬ.
Proof. Let : ∃ . →↦ ∃ . ℬ be a partial homomorphism. We verify that ℎ as defined above is a homomorphism. (H1) Since () = for each individual , we also have ℎ() = . (H2) Consider an assertion : in . We distinguish two cases.
• Assume ∈ Dom(), and thus ℎ() = (). If ℎ() is a variable (in ), then (PH2) ensures that ℎ() : is in ℬ, and thus also in ℬ* . Otherwise, ℎ() is an individual, and so ℬ* contains ℎ() : by definition.
• In the remaining case we have ℎ() = *, and ℬ * contains ℎ() : by definition. (H3) Let (, ) : be an assertion in .
• Assume ∈ Dom(), i.e. ℎ() = (), and further let ℎ() be a variable (in ). Then (PH3) ensures that (ℎ(), ℎ()) : is in ℬ, and thus also in ℬ* . Similarly, if ∈ Dom() and ℎ() ∈ , then (ℎ(), ℎ()) : ∈ ℬ ⊆ ℬ * by (PH4).
• Moreover, if , ∈ Dom() and ℎ(), ℎ() are individuals, then (ℎ(), ℎ()) : ∈ ℬ* by definition of ℬ * .
• Now let ∈ Dom(), ̸∈ Dom(), and ℎ() an individual. Then ℎ() = * and so the definition of ℬ* ensures that (ℎ(), ℎ()) : is in ℬ* . The case where ̸∈ Dom(), ∈ Dom(), and ℎ() an individual is analogous.
• In the remaining case we have , ̸∈ Dom() and thus ℎ() = * = ℎ() . Then ℬ* contains (ℎ(), ℎ()) : by definition.
Regarding the second statement, let ℎ : ∃ . → ∃ . ℬ be a homomorphism. We show that as defined above is a partial homomorphism. (PH1) For each individual , we have ℎ() = , and so () = ℎ(), i.e. () = . (PH2) Let : be in where ∈ Dom() and () ∈ . The first assumption yields that ℬ* contains ℎ() : , the second yields () = ℎ() ̸= * , and thus the third implies that () : is already in ℬ. (PH3) Assume contains (, ) : where ∈ Dom() and () ∈ . By the first assumption ℬ* contains (ℎ(), ℎ()) : , the second implies () = ℎ() ̸= * , and so by the third we conclude that ℬ contains ((), ℎ()) : . Moreover, it follows that ℎ() ̸= * and thus ∈ Dom() where () = ℎ(), i.e. ((), ()) : ∈ ℬ. (PH4) Analogous to the previous case. 5. The Case with ℰℒ Ontologies and ℰℒ ABox Observations We now turn our attention to the case with an ontology . According to Example 4 there can be infinitely many minimal explanations of an observation, even when is an ℰℒ ontology and the observation is an ℰℒ ABox. A closer look at this example reveals that all these explanations are obtained from “premises” of the observation, i.e. from qABoxes entailing the observation w.r.t. . The following lemma shows that this is true in general for all ontologies consisting of first-order sentences. Lemma 12. Consider a qABox ∃ . as observation and a KB composed of a qABox ∃ . ℬ and an ontology consisting of first-order sentences. Every minimal abductive diference of ∃ . w.r.t. ∃ . ℬ and is equivalent w.r.t. to a -diference ∃ ′. ′ ∖ ∃ . ℬ for some ∃ ′. ′ with ∃ ′. ′ |= ∃ . and some partial homomorphism from ∃ ′. ′ to ∃ . ℬ.
Proof. Let ∃ . be a minimal abductive diference of ∃ . w.r.t. ∃ . ℬ and , i.e. ∃ . ℬ ∪ ∃ . |= ∃ . , and define ∃ ′. ′ := ∃ . ℬ ∪ ∃ . . Clearly, we have ∃ ′. ′ |= ∃ . .
Obviously, ∃ . ℬ ∪ ∃ . |= ∃ ′. ′ and so ∃ . is also an abductive diference of ∃ ′. ′ w.r.t. ∃ . ℬ (and the empty ontology). According to Lemma 8 there is a partial homomorphism from ∃ ′. ′ to ∃ . ℬ such that the -diference ∃ ′. ′ ∖ ∃ . ℬ is entailed by ∃ . . By Lemma 7, this -diference is an abductive diference of ∃ ′. ′ w.r.t. ∃ . ℬ (and the empty ontology), and thus also of ∃ . w.r.t. ∃ . ℬ and . Since ∃ . |= ∃ ′. ′ ∖ ∃ . ℬ yields ∃ . |= ∃ ′. ′ ∖ ∃ . ℬ and ∃ . is minimal, we conclude that ∃ . and ∃ ′. ′ ∖ ∃ . ℬ are equivalent w.r.t. .
We conclude that enumerating a superset of all minimal explanations w.r.t. an ontology can be “reduced” to enumerating minimal explanations without ontology. More specifically, since the set of qABoxes is countable, we can enumerate all “premises” of the observation when entailment w.r.t. the ontology is decidable, and thus the above lemma allows us to enumerate a superset that contains all minimal explanations. However, using this approach only allows us to exclude a non-minimal explanation as soon as a strictly entailed explanation has been enumerated, i.e. non-minimality is semi-decidable. Future research should consider this problem in more detail, possibly for restricted classes of ontologies only.
For an ℰℒ ontology and an observation in form of an ℰℒ ABox, the minimal explanations have a special form, as the below lemma shows.
Lemma 13. Given an ℰℒ ABox as observation and a KB consisting of a qABox ∃ . ℬ and an ℰℒ ontology , every minimal abductive diference of w.r.t. ∃ . ℬ and is equivalent w.r.t. to a -diference 4 ′ ∖ ∃ . ℬ where is a partial homomorphism from ′ to ∃ . ℬ and the ABox ′ consists of • a CA : ′ with ′ ⊑ for each CA : in with ∃ . ℬ ̸|= : , • and each RA (, ) : in that is not in ℬ.
Proof. Consider an observation in form of an ℰℒ ABox , a KB consisting of a qABox ∃ . ℬ and an ℰℒ ontology , and further let ∃ . be a minimal abductive diference of w.r.t. ∃ . ℬ and . We build the ABox ′ as follows.
• Let : be a CA in . By assumption, we have ∃ . ℬ ∪ ∃ . |= : . Lemma 22 in [23] yields a concept ′ with ∃ . ℬ ∪ ∃ . |= : ′ and ′ ⊑ . We add : ′ to ′, but only if : is not already entailed by ∃ . ℬ w.r.t. since otherwise it need not be explained. • Now let (, ) : be a RA in . The assumption yields that ∃ . ℬ ∪ ∃ . |= (, ) : , and thus ℬ or contains this RA. In the former case the RA need not be explained, and in the latter case we add the RA to ′.
By construction we have ∃ . ℬ ∪ ∃ . |= ′, and thus ∃ . is an abductive diference of ′ w.r.t. ∃ . ℬ (and the empty ontology). By identifying ′ with an equivalent qABox, Lemma 8 yields a partial homomorphism : ′ →↦ ∃ . ℬ such that ∃ . |= ′ ∖ ∃ . ℬ. According to Lemma 7, ′ ∖ ∃ . ℬ is an abductive diference of ′ w.r.t. ∃ . ℬ (and the empty ontology), and thus also of w.r.t. ∃ . ℬ and . Since ∃ . |= ′ ∖ ∃ . ℬ implies ∃ . |= ′ ∖ ∃ . ℬ and ∃ . is minimal, we conclude that ∃ . and ′ ∖ ∃ . ℬ are equivalent w.r.t. .
Last, we can also employ saturations to construct abductive diferences, but not in a complete manner since in Example 4 there is a minimal explanation that cannot be constructed from the saturation. In particular, the saturation equals the ABox already, from which we can only obtain the observation itself as a minimal p-diference.
Lemma 14. For each partial homomorphism from ∃ . to the saturation of ∃ . ℬ w.r.t. , the -diference is an abductive diference of ∃ . w.r.t. ∃ . ℬ and .
Proof. We denote the saturation by sat(∃ . ℬ). By Lemma 7, the -diference is an abductive diference of ∃ . w.r.t. sat(∃ . ℬ), i.e. sat(∃ . ℬ) ∪ (∃ . ∖ sat(∃ . ℬ)) |= ∃ . . Since ∃ . ℬ |= sat(∃ . ℬ), it follows that ∃ . ℬ ∪ (∃ . ∖ sat(∃ . ℬ)) |= ∃ . .
After these first steps regarding abduction with quantified ABoxes, it would be interesting to investigate in more details how exactly ontologies or restricted classes of ontologies can be treated when computing minimal explanations. In order to alleviate the problem of infinitely many minimal explanations, practically motivated metrics should be used to restrict and compare explanations. In ℰℒ, a further approach to this problem would be using weaker entailment relations. For instance, instead of comparing quantified ABoxes regarding their models we could compare them regarding the ℰℒ CAs and RAs they 4Technically, this -diference ′ ∖ ∃ . ℬ rather is ∃ ′′. ′′ ∖ ∃ . ℬ where ∃ ′′. ′′ is a qABox equivalent to ′. Such a qABox always exists as explained in the preliminaries. entail (IRQ-entailment [24]). In Example 4, then only the explanations with ∈ {0, 1} would be be minimal, as would be the observation itself. Yet another alternative to identifying practically useful explanations would be to employ some form of user interaction, especially when only one explanation is needed in the application.
In order to verify their applicability, it would be interesting to implement the presented results and empirically evaluate them on real-world datasets.
This work has been supported by Deutsche Forschungsgemeinschaft (DFG) in Project 389792660 (TRR 248: Foundations of Perspicuous Software Systems) and in Project 558917076 (Construction and Repair of Description-logic Knowledge Bases) as well as by the Saxon State Ministry for Science, Culture, and Tourism (SMWK) by funding the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI).
The author has not employed any Generative AI tools. [8] Jianfeng Du, Kewen Wang, Yi-Dong Shen. A Tractable Approach to ABox Abduction over Description Logic Ontologies. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada. 2014, pp. 1034–1040. doi:10.1609/AAAI.V28I1.8852. [9] Jianfeng Du, Guilin Qi, Yi-Dong Shen, Jef Z. Pan. Towards Practical ABox Abduction in Large Description Logic Ontologies. In: Int. J. Semantic Web Inf. Syst. 8.2 (2012), pp. 1–33. doi:10.4018/JSWIS.2012040101. [10] Szymon Klarman, Ulle Endriss, Stefan Schlobach. ABox Abduction in the Description Logic ℒ.
In: J. Autom. Reason. 46.1 (2011), pp. 43–80. doi:10.1007/S10817-010-9168-Z. [11] Ken Halland, Arina Britz, Szymon Klarman. TBox Abduction in ℒ Using a DL Tableau. In: Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014. 2014, pp. 556–566. URL: https://ceur-ws.org/Vol-1193/paper_42.pdf. [12] Thomas Hubauer, Stefen Lamparter, Michael Pirker. Automata-Based Abduction for Tractable Diagnosis. In: Proceedings of the 23rd International Workshop on Description Logics (DL 2010), Waterloo, Ontario, Canada, May 4-7, 2010. 2010. URL: https://ceur-ws.org/Vol-573/paper_27.pdf. [13] Fajar Haifani. On a notion of abduction and relevance for first-order logic clause sets. PhD thesis.
Saarland University, Saarbrücken, Germany, 2022. URL: https://publikationen.sulb.uni-saarland. de/handle/20.500.11880/35608. [14] Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, Renate A. Schmidt. Signature-Based Abduction for Expressive Description Logics. In: Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020. 2020, pp. 592–602. doi:10.24963/KR.2020/59. [15] Sophie Tourret. Abduction in first order logic with equality. (Prime implicate generation in equational logic). PhD thesis. Grenoble Alpes University, France, 2016. URL: https://tel.archives-ouvertes.fr/ tel-01366458. [16] Ángel Nepomuceno-Fernández, Fernando Soler-Toscano, Atocha Aliseda-Llera. Abduction via C-tableaux and delta-resolution. In: J. Appl. Non Class. Logics 19.2 (2009), pp. 211–225. doi:10.3166/JANCL.19.211-225. [17] Meghyn Bienvenu. Complexity of Abduction in the ℰ ℒ Family of Lightweight Description Logics. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference, KR 2008, Sydney, Australia, September 16-19, 2008. 2008, pp. 220–230.
URL: http://www.aaai.org/Library/KR/2008/kr08-022.php. [18] Christoph Wernhard. Abduction in Logic Programming as Second-Order Quantifier Elimination.
In: Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings. 2013, pp. 103–119. doi:10.1007/978-3-642-40885-4_8. [19] Reinhard Pichler, Stefan Woltran. The Complexity of Handling Minimal Solutions in Logic-Based Abduction. In: ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings. 2010, pp. 895–900. doi:10.3233/978-1-60750-606-5-895. [20] Franz Baader, Sebastian Brandt, Carsten Lutz. Pushing the ℰℒ Envelope. In: IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005. 2005, pp. 364–369. URL: http://ijcai.org/Proceedings/05/Papers/0372.pdf. [21] Franz Baader, Patrick Koopmann, Francesco Kriegel. Optimal Repairs in the Description Logic ℰℒ Revisited. In: Logics in Artificial Intelligence - 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings. 2023, pp. 11–34. doi:10.1007/978-3-031-43619-2_2. [22] Franz Baader, Francesco Kriegel. Pushing Optimal ABox Repair from ℰℒ Towards More Expressive Horn-DLs. In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, KR 2022, Haifa, Israel, July 31 - August 5, 2022. 2022. doi:10.24963/kr.2022/3. [23] Carsten Lutz, Frank Wolter. Deciding inseparability and conservative extensions in the description logic ℰℒ. In: J. Symb. Comput. 45.2 (2010), pp. 194–228. doi:10.1016/J.JSC.2008.10.007. [24] Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah. Optimal ABox Repair w.r.t. Static ℰℒ TBoxes: From Quantified ABoxes Back to ABoxes. In: The Semantic Web - 19th International Conference, ESWC 2022, Hersonissos, Crete, Greece, May 29 - June 2, 2022, Proceedings. 2022, pp. 130–146. doi:10.1007/978-3-031-06981-9_8.