Abduction is the task of computing a suficient extension of a knowledge base (KB) that entails a conclusion not entailed by the original KB. It serves to compute explanations, or hypotheses, for such missing entailments. While this task has been intensively investigated for perfect data and under classical semantics, less is known about abduction when erroneous data results in inconsistent KBs. In this paper we define a suitable notion of abduction under repair semantics, and propose a set of minimality criteria that guides abduction towards 'useful' hypotheses. We provide initial complexity results on deciding existence of and verifying abductive solutions with these criteria, under diferent repair semantics and for the description logics DL-Lite and ℰℒ ⊥.
In the context of description logic knowledge bases, the task of abduction is prominently used to explain
missing consequences. In general, given a theory and an observation, that is a formula not entailed over
the theory, abduction asks for a hypothesis, which is a collection of statements to add to the theory
in order to entail the observation. For description logics, such hypotheses are often computed for a
knowledge base and some kind of Boolean query. This general task has been intensively investigated
for description logics in many variants, depending on whether it is about extending the TBox [
If abduction is applied to compute explanations, often minimality criteria for the hypotheses are
imposed to obtain “feasible” explanations. For example, it can be required that hypotheses are
subsetminimal to facilitate small explanations [
In practical ontology-based applications, data is rarely free of errors and thus, the data that populates the ABox in the description logic KB can easily become inconsistent. In such cases, everything would follow from the KB, but meaningful reasoning can be regained by resorting to some kind of inconsistencytolerant, i.e. non-monotonic, semantics such as repair semantics [17, 18] or defeasible semantics [19, 20, 21]. Repair semantics rely on restoring consistent versions of an inconsistent KB by removing minimal sets of conflicting ABox statements. Such a restored version is known as an ABox repair. Depending on which, of the possibly many, repairs are considered for reasoning, diferent repair semantics have been defined and investigated in the literature mainly for ontology-mediated query answering (OMQA) settings, see [22] for an overview. Three fundamental repair semantics entail a Boolean query, if it holds w.r.t. some repair (brave semantics), w.r.t. all repairs (AR semantics) or w.r.t. the intersection of all repairs (IAR semantics), respectively.
While explanations of query entailment under repair semantics have been investigated, explaining
query non-entailment under these semantics has been addressed to a much lesser extent. In particular,
ABox abduction under repair semantics has not been studied thoroughly. In [
In this paper we study ABox abduction under repair semantics. We focus on flat ABox abduction, where the hypotheses use atomic concepts only and where the observation is a Boolean instance query (BIQ). We first need to adapt the basic definitions for abduction to the inconsistency-tolerant setting (in Section. 3). Using repair semantics results in some subtle diferences in comparison to abduction under classical semantics. To address these, we make some conceptual contributions to adapt to the new setting. Since reasoning with the generated hypotheses is using repair semantics, we do not require the hypothesis itself to be consistent. This can lead to more ABox abduction results, obviously. We extend the set of common minimality criteria for hypotheses to new ones that are dedicated to limit the (efect of) conflicts.
We show also some initial complexity results for two prominent decision problems introduced for
abduction [
It turns out (in Section 4) that the existence problem considered without a signature restriction is trivial under brave semantics, but for AR semantics its complexity drops to that of the complement of brave entailment. Furthermore, deciding existence under signature restrictions keeps the same complexity of entailment for brave semantics, but for AR semantics it increases by one complexity level in the polynomial hierarchy for ℰ ℒ⊥.
The verification problem (treated in Section 5) does not become trivial for unrestricted signatures, but has the same complexity as entailment for general and ≤ -minimal hypotheses. In case subset-minimality is required for hypotheses, we show that a more heterogeneous complexity landscape unfolds. For instance, brave semantics incurs no or moderate increase in complexity depending on the DL. All of the omitted proofs and proof details can be found in the long version of the paper [26].
For a general introduction to description logics, we refer to the description logic textbook [27]. We assume familiarity with computational complexity [28], in particular with the complexity classes NL, P, NP, coNP and 2P. Additionally, DP is the class of decision problems representable as the intersection of a problem in NP and a problem in coNP. 2.1. The Description Logics Considered: ℰ ℒ⊥ and DL-Lite
::= ⊓ | ∃. | | ⊤ | ⊥, where and range over all concept and role names, respectively. ℰ ℒ⊥ TBoxes contain finitely many concept inclusions ⊑ for ℰ ℒ⊥ concepts and .
We consider the DL-Lite dialects DL-Liteℛ and DL-Litecore. In DL-Liteℛ (underlying the OWL 2 QL profile), TBoxes may contain concept inclusions of the form ⊑ and role inclusions of the form ⊑ , where , , and are generated by the following grammar: ::= | ∃, ::= | ¬, ::= | − , ::= | ¬, where and range over all concept and role names, respectively. Then DL-Litecore restricts DL-Liteℛ by disallowing role inclusions, so only concept inclusions of the above form are allowed.
We study instance queries (IQs), which consist of a (complex) concept and a variable: (). Boolean instance queries (BIQs) are IQs that use an individual name instead of a variable: ().
For the rest of the paper, the general term DL-Lite refers to either DL-Litecore or DL-Liteℛ. We do so, since all of our results apply to both DLs, as our proofs only use properties shared by both DLs: (1) entailment of atomic BIQs is NL-complete under Brave and coNP-complete under AR semantics, (2) for a TBox , subset-minimal -inconsistent ABoxes are of size 2, where is -inconsistent, if ⟨ , ⟩ |= ⊥, and (3) for a TBox and atomic BIQ , minimal -supports of are of size 1, where a -support of is an ABox with ⟨ , ⟩ |= .
If a knowledge base is inconsistent, repair semantics can “restore” consistent versions and admit meaningful reasoning again. As it is common, we consider ABox repairs. We define these as well as two common kinds of repair semantics next.
Let = ⟨ , ⟩ be an inconsistent knowledge base and be a Boolean (conjunctive) query. A repair of is a subset ℛ ⊆ such that ⟨ , ℛ⟩ ̸|= ⊥ and there is no strict superset ℛ′ ⊃ ℛ with these properties. The somewhat dual notion is a conflict or conflict set , which is a subset of the ABox that is -inconsistent and subset-minimal with this property. We denote by Conf() the set of conflicts of . We recall entailment under brave [17] and AR semantics [18]: • |=Brave if and only if there exists some repair ℛ of such that ⟨ , ℛ⟩ |= .
• |=AR if and only if ⟨ , ℛ⟩ |= for every repair ℛ of .
The complexity of query entailment under repair semantics is well understood [29]. Precisely, checking entailment of atomic BIQs under Brave semantics is NL-complete for DL-Lite and NP-complete for ℰ ℒ⊥ in combined complexity, whereas under AR semantics it is coNP-complete for both DLs.
The central task of abduction is to compute abductive hypotheses. We define these for non-entailed BIQs under repair semantics.
Definition 1. Let = ⟨ , ⟩ be an inconsistent KB, be an atomic BIQ (called an observation) and ∈ {Brave, AR} such that ̸|= . Then, a pair ⟨, ⟩ is called an -abduction problem. A solution for such a problem, called -hypothesis, is an ABox ℋ such that ⟨ , ∪ ℋ⟩ |= . An -hypothesis ℋ is called 1. flat, if ℋ contains no complex concepts; 2. over , if ℋ uses only names from signature , where is a set of concept, role and individual names; 3. conflict-confining, if Conf(⟨ , ∪ ℋ⟩) = Conf().
Note that for an -abduction problem ⟨, ⟩ we require that is inconsistent and ̸|= . So, we consider only the so-called promise problem, i.e. the problem restricted to these particular inputs. The restriction aligns with the intuition that one asks for an -hypothesis if it is already known that the knowledge base is inconsistent and the observation is not -entailed in . In contrast, if we instead assume that is consistent and is not entailed by under classical semantics, we obtain classical abduction problems. In this case, we call an ABox ℋ hypothesis for under classical semantics, if ⟨ , ∪ ℋ⟩ ̸|= ⊥ and ⟨ , ∪ ℋ⟩ |= .
While the first two properties of -hypotheses from Definition 1 are standard for abduction, the last one adapts the idea of a hypothesis not introducing any inconsistencies to the setting, where the KB is already inconsistent to begin with. It can equivalently be defined by requiring that ⟨ , ℛ ∪ ℋ⟩ ̸|= ⊥ for every repair ℛ of . Note that this property might not always be desired. We consider the following reasoning problems for a given -abduction problem.
To obtain hypotheses that are meaningful for explanation purposes, minimality criteria that yield preferred hypotheses have been defined already for abduction under classical semantics. We restate some of them and extend this set of criteria to also treat conflicts.
Definition 3. Let ∈ {Brave, AR}, ⟨, ⟩ be an -abduction problem, where = ⟨ , ⟩, and let ℋ be an -hypothesis for ⟨, ⟩. Considering ⪯ ∈ {⊆, ≤}, ℋ is called 1. ⪯-minimal, if there is no -hypothesis ℋ ′ for ⟨, ⟩ such that ℋ ′ ≺ ℋ; 2. ⪯ -minimal, if there is no -hypothesis ℋ′ for ⟨, ⟩ such that Conf(⟨ , ∪ ℋ′⟩) ≺
Conf(⟨ , ∪ ℋ⟩).
We use the term subset-minimal for ⊆ -minimal and cardinality-minimal for ≤ -minimal. For any (reasonable) combinations of repair semantics, the above properties, and minimality criteria, we consider the corresponding computational problems introduced in Definition 2.
Under certain repair semantics, already standard reasoning tasks such as query answering can behave in unexpected ways. This also holds true for abduction of ⊆ -minimal AR-hypotheses, due to reasoning being inherently non-monotonic in this case, as the following interesting efect illustrates. More precisely, the set of AR-hypotheses for a given AR-abduction problem ⟨, ⟩ does not need to be convex with respect to the subset-relation. We illustrate this by a small example KB = ⟨ , ∅⟩ and ABoxes 1 ⊊ 2 ⊊ 3 such that ⟨ , 1⟩ |=AR () and ⟨ , 3⟩ |=AR (), but ⟨ , 2⟩ ̸|=AR (). This can be achieved by defining the TBox and the ABoxes as follows: := {1 ⊓ 2 ⊑ ⊥, 1 ⊓ 2 ⊑ ⊥, 1 ⊓ 1 ⊑ , 2 ⊓ 1 ⊑ , ⊑ }, 1 := {1(), 2(), 1()}, 2 := 1 ∪ {2()}, 3 := 2 ∪ {()} This efect implies that ⊆ -minimality cannot be checked locally by only considering subsets that remove one assertion at a time. Instead, one seems to need a global check for all subsets.
In classical abduction, one further considers semantically minimal hypotheses ℋ, for which there exists no hypothesis ℋ′ such that ⟨ , ∪ ℋ⟩ |= ℋ′, but ⟨ , ∪ ℋ′⟩ ̸|= ℋ. We argue that while such a minimality criterion is natural for AR-semantics, its meaning is unclear for Brave-hypotheses. For instance, what does semantic minimality tell about two Brave-hypotheses entailing the observation, but in possibly diferent repairs? Further exploration of this minimality criterion is therefore left for future work. DL-Lite ℰℒ⊥
Brave AR Brave AR general Trivial
NL Trivial coNP signature ≤-min
NL in 2P
NP 2P
Verification
⊆-min
NL coNP
NP coNP
NL
DP DP-hard, in Π2P DP-hard, in Π2P
We study in this section the complexity of the existence problem for both ℰ ℒ⊥ and without a given signature, under brave and AR semantics. Observe that for ∈ {Brave, AR}, the existence of any -hypothesis implies the existence of a minimal one for all of the introduced minimality criteria. Therefore, we only consider the existence problem for general -hypotheses. We begin with the case where no signature is given. Further, the fact that the singleton set containing only and DL-Lite, with the observation can be a hypothesis leads to the problem degenerating to a special case of entailment, or even becoming trivial. This also lends additional motivation to study the signature-based setting next, where such trivial hypotheses can be prevented.
As we only consider atomic BIQs as observations , the set {} is an ABox and, therefore, a candidate for a hypothesis for . We study in this section how this trivial hypothesis afects the complexity of the existence problem for -hypotheses, where ∈ {Brave, AR}.
Let ⟨, ⟩ the set ℋ = {} be an -abduction problem, where = ⟨ , ⟩. In case of = Brave, it is easy to see that is a Brave-hypothesis for ⟨, ⟩ , as is contained in some repairs of ⟨ , ∪ {}⟩ . Hence, a Brave-hypothesis always exists. The case of AR semantics is slightly more interesting, as an AR-hypothesis need not exist in general, even if trivial hypotheses are allowed. Interestingly, in this case the complexity of the existence problem becomes a special case of AR entailment that has the same complexity as non-entailment under brave semantics for both DLs. In case of ℰ ℒ⊥, this means that checking existence of AR-hypotheses has the same complexity as AR entailment. In contrast, for DL-Lite this gives a complexity of coNL = NL, which is the complexity of brave entailment. Lemma 4. Let ⟨, ⟩ ̸|=Brave ¬. 1
be an AR-abduction problem. The following are equivalent: (1) there is an ARhypothesis for ⟨, ⟩ , (2) {} is an AR-hypothesis for ⟨, ⟩ , (3) {} is conflict-confining for , and (4) DL-Lite. Moreover, the problem is trivial for Brave-hypotheses in both DLs.
Theorem 5. The existence problem for AR-hypotheses is coNP-complete for ℰ ℒ⊥ and NL-complete for not conflict-confining.
Note that the equivalence of {}
being an AR-hypothesis for and {} means that this result applies both to general and conflict-confining AR-hypotheses. The set being conflict-confining a conflict-confining AR-hypothesis also implies that there is a conflict-confining Brave-hypothesis {} being remains open: There are cases where there is a conflict-confining Brave-hypothesis for (namely {} ). Still, the complexity of the existence problem for conflict-confining Brave-hypothesis , but {} is 1Here, entailment of ¬ has the usual meaning, even if negation is not in the logical language. As we just have seen, checking existence of hypotheses without additional restrictions degenerates to entailment, or even a special case of entailment, because the observation itself can be a hypothesis. A natural way to prevent this is to restrict the signature of hypotheses, that is, only consider hypothesis over some signature as defined in Definition 1.
We begin by characterizing the complexity for consistent KBs under classical semantics. It turns out that this classical abduction problem is NP-complete. Then we consider the setting with inconsistent KBs under repair semantics and prove that the NP-membership still holds under brave semantics. However, the complexity rises to 2P-complete under AR semantics.
Theorem 6. For ℰ ℒ⊥, the existence problem for hypotheses under classical semantics over a given signature is NP-complete.
The Inconsistent Case. Now we analyse the case of inconsistent KBs and repair semantics. Theorem 7. For ℰ ℒ⊥, the existence problem for -hypotheses over a given signature is (1) NP-complete for = Brave, and (2) 2P-complete for = AR.
Proof. For (1): An NP-algorithm for the problem can guess a hypothesis ℋ over the signature and, at the same time, guess a repair ℛ of the ABox. Then, verify that ⟨ , ℛ ∪ ℋ⟩ ̸|= ⊥ and ⟨ , ℛ ∪ ℋ⟩ |= in polynomial time. The NP-hardness can be shown by slightly adapting the reduction in Theorem 6, adding an artificial inconsistency over fresh concepts not in .
For (2): The following algorithm shows 2P-membership: Guess a set ℋ such that for all repairs ℛ of ⟨ , ∪ ℋ⟩, we have ⟨ , ℛ⟩ |= . This requires NP-time to guess the set ℋ and an NP-oracle to guess a repair ℛ as a counter example to the entailment, thus resulting in 2P-membership. For hardness, we reduce from the standard 2P-complete problem QBF2: Instances of QBF2 are of the form := ∃ ∀ ′, where ′ is a Boolean formula over variables = ∪ . Without loss of generality, we can assume that ′ = ¬ for some Boolean formula in CNF. The problem asks whether is valid (or true). We construct the following KB = ⟨ , ⟩, using concept names = {, ¯ | ∈ } ∪ { | ∈ } ∪ { | ∈ } ∪ { , ¯, }. The TBox contains the following sets of axioms: { ⊓ ¯ ⊑ ⊥ | ∈ } {ℓ ⊑ | ℓ ∈ , ∈ } {⊓∈ ⊑ , ⊓ ¯ ⊑ ⊥} { ⊑ , ¯ ⊑ | ∈ } {⊓∈ ⊓ ¯ ⊑ }
(ensures a valid assignment over ), (each clause is satisfied), (the formula is satisfied), (hypotheses over are assignments over ), and (confirm the above with a concept name ).
Further, let := {(), ¯() | ∈ } ∪ { ¯()} for an individual name . Finally, let := {} ∪ {, ¯ | ∈ } and := (). Now ⟨, ⟩ together with the signature is the desired abduction problem.
We first observe that ⟨, ⟩ is a valid AR-abduction problem: Obviously, |= ⊥ when is nonempty, due to both () and ¯() being present in the ABox for every ∈ . Also, ̸|=AR , as does neither involve the concept name nor any of the concept names , ¯, or for ∈ . The following claim states correctness of the reduction.
Claim 1. is true if and only if has an AR-hypothesis over the signature in .
Claim Proof. “=⇒”: Suppose is true. Then there is an assignment ⊆ Lit( ) such that for all assignments ⊆ Lit() , ¬[, ] is true. Here, Lit(·) denotes the set of literals over a given set of variables. We construct an AR-hypothesis for from . Let ℋ = {() | ∈ }. Obviously, ℋ is an ABox over . Also, it does not violate any axiom of the form ⊓ ¯ ⊑ ⊥, since is an assignment.
We prove that ⟨ , ∪ ℋ⟩ |=AR . Consider any repair ℛ of ⟨ , ∪ ℋ⟩. As ⟨ , ℛ⟩ ̸|= ⊥, ℛ does not violate any axiom of the form ⊓ ¯ ⊑ ⊥. Hence, ℛ ∩ {(), ¯() | ∈ } corresponds to (potentially partial) assignments ℛ ⊆ and ℛ over and , respectively. We first prove that ⟨ , ℛ⟩ ̸|= (). Suppose to the contrary, that ⟨ , ℛ⟩ |= (). As ℛ is consistent with , this only happens by triggering the axiom ⊓∈ ⊑ , and in turn an axiom of the form ℓ ⊑ for each clause ∈ . But this means that ℛ ∪ ℛ, and hence also ∪ ℛ, is a satisfying assignment for , which is a contradiction to ¬[, ] being true for all assignments over . Indeed, as this argument covers the case ℛ = , subset-maximality of repairs further yields that ℋ ⊆ ℛ . Moreover, subset-maximality together with the fact that ⟨ , ℛ⟩ ̸|= () yields that ¯() ∈ ℛ. Consequently, ⟨ , ℛ⟩ |= ().
“⇐=”: Suppose is false. Then, for each assignment ⊆ Lit( ) , there is an assignment ⊆ Lit() such that ¬[, ] is false or, equivalently, [, ] is true. The latter can be stated as: each clause ∈ contains some literal ℓ ∈ with ℓ ∈ ∪ .
We now prove that does not have any AR-hypothesis over in . For contradiction, assume that ℋ ⊆ { () | ∈ Lit( )} is such a hypothesis and consider any repair ℛ of ⟨ , ∪ ℋ⟩. As ℛ does not violate any axiom of the form ⊓ ¯ ⊑ ⊥, the subset ℛ := ℛ ∩ {(), ¯() | ∈ } corresponds to a potentially partial assignment ℛ over . On the other hand, as ⟨ , ℛ⟩ |= (), we also have ⟨ , ℛ⟩ |= ⊓∈ (). Therefore, ℛ contains at least one assertion from {(), ¯()} for each ∈ , i.e. that ℛ is a full assignment over . By our assumption, there is an assignment over s.t. [ ℛ, ] is true.
Let ℛ := ℛ ∪ {ℓ() | ℓ ∈ }. Obviously, ℛ does not violate any of the disjointness axioms in , as it does not contain ¯() and ℛ ∪ is an assignment over . This further means that ⟨ , ℛ⟩ ̸|= (). Furthermore, ℛ is subset-maximal: As both ℛ and are full assignments, we cannot add any assertion of the form () or ¯() for ∈ without violating one of the disjointness axioms. Also, as [ ℛ, ] is true, we have ⟨ , ℛ⟩ |= (). Hence, we also cannot add ¯() without violating the corresponding disjointness axiom. This shows that ℛ is a repair of ⟨ , ∪ ℋ⟩ that does not entail , contradicting our assumption.
This proves the correctness of the claim and establishes the theorem. ■
We now turn to DL-Lite, where we show that checking existence for Brave-hypotheses has the same complexity as Brave entailment.
Theorem 8. For DL-Lite, the existence problem for Brave-hypotheses over a given signature is NLcomplete.
Regarding AR-semantics for DL-Lite, it is easy to see that 2P-membership can be shown in the same way as for ℰ ℒ⊥ in the proof of Theorem 7. Determining the precise complexity for this case remains open for now.
The verification problem does not become quite as easy even without restricting the signature, so even if trivial hypotheses are allowed. Interestingly, we even show that in case of ⊆ -minimality the complexity goes beyond that of entailment under repair semantics in some cases. We begin with the case of general and ≤ -minimal hypotheses for ℰ ℒ⊥, where the complexity of the corresponding entailment problem is inherited.
Lemma 9. For ℰ ℒ⊥, the verification problem for -hypotheses is (1) NP-complete for = Brave, and (2) coNP-complete for = AR. This also applies to ≤-minimal hypotheses.
We prove next that the complexity of verification rises to DP-completeness for ⊆ -minimal hypotheses. The complexity gap between verifying ⊆ and ≤ hypotheses seems somewhat surprising at first. Nevertheless, the “lower” complexity of verifying ≤ -minimal hypothesis can be explained by observing that a ≤-minimal hypothesis has size one (namely, {} itself).
Theorem 10. For ℰ ℒ⊥, verification for ⊆ -minimal Brave-hypotheses is DP-complete, whereas verification for AR-hypotheses is DP-hard and in Π2P.
Proof. For membership, observe that ℋ is a ⊆ -minimal -hypothesis if and only if (1) ⟨ , ∪ ℋ⟩ |= and (2) for all subsets ℋ′ ⊊ ℋ , we have ⟨ , ∪ ℋ⟩ ̸| . In the case of Brave-hypotheses, (1) is = instance checking for ℰ ℒ⊥ and hence in NP, while (2) can be checked in coNP by universally guessing a subset ℋ′ and repair ℛ of ⟨ , ∪ ℋ′⟩ and checking that ⟨ , ℛ⟩ ̸|= in polynomial time. Hence, the problem is contained in DP. Analogous reasoning under AR semantics yields that (1) can be checked in coNP, whereas checking (2) requires an oracle to decide non-entailment under AR semantics for each ℋ′ ⊆ ℋ. This shows coNP NP-membership.
For hardness, we reduce from a combination of instance checking and its complement problem to our verification of hypotheses. Given an instance ⟨, 1, 2⟩, the problem asks whether |= 1 and ̸| 2, where ∈ {Brave, AR}. This problem is DP-complete because the first question = is NP-complete and the second question is coNP-complete under Brave semantics and vice versa under AR semantics. For the reduction, assume 1 = (), 2 = (), and = ⟨ , ⟩. We construct a KB ′, an observation , and a hypothesis ℋ as illustrated next. Let ′ := ⟨ ′, ⟩ with ′ = ∪ { ⊑ , ⊓ ⊓ ⊑ }, := (), and ℋ := {(), ()} for fresh concepts , , . The instance is a valid abduction problem, since ′ ̸|= (in particular, due to ()). Intuitively, ℋ is a Brave-hypothesis for in ′ if and only if |=Brave () and ℋ is subset-minimal if and only if ̸|=Brave (). It remains to show correctness, i.e., ℋ is a ⊆ -minimal hypothesis for in ′ if and only if |=Brave 1 and ̸|=Brave 2.
We conclude by observing that the above correctness proof works if we replace every Brave-entailment by AR-entailment.
We now turn to the case of DL-Lite. We begin by an observation on ⊆ -minimal (and ≤ -minimal) Brave-hypotheses, namely that they always have cardinality 1.
Lemma 11. For DL-Lite, if ℋ is a ⊆ -minimal or ≤ -minimal Brave-hypothesis for some Brave-abduction problem ⟨, ⟩, then |ℋ| = 1.
The next theorem establishes the complexity of the verification problem for Brave-hypotheses in DL-Lite, in the general, ≤-minimal and ⊆-minimal case.
Theorem 12. For DL-Lite, the verification problem for general, ≤ -minimal and ⊆ -minimal Bravehypotheses is NL-complete.
Finally, we turn towards the case of AR semantics.
Theorem 13. For DL-Lite, the verification problem for AR-hypotheses is (1) coNP-complete for general and ≤-minimal hypotheses, and (2) DP-hard for ⊆-minimal ones with membership in Π 2P. Proof. General hypotheses: Regarding membership, observe that the question can be answered by checking whether ⟨ , ∪ ℋ⟩ |=AR . Hence, the complexity follows from that of AR-entailment for DL-Lite. For hardness, we reuse the following reduction from unsatisfiability and AR-entailment [ 24]. Let = { 1, . . . , } over propositions = {1, . . . , }, where the are clauses. We construct = ⟨ , ⟩ using a single concept name and role names = {, , }, where = {∃ −
⊑ ¬∃ − , ∃ ⊑ ¬∃ − , ∃ ⊑ ¬∃ − , ∃ ⊑ }, and = { ( , ) | ∈ } ∪ { ( , ) | ¬ ∈ } ∪ { (, ) | ≤ }.
Moreover, let := (). It is known that |=AR () if and only if is unsatisfiable [ 24]. To show hardness of the verification problem at hand, let ℋ := { (, ) | ≤ } and ′ := ⟨ , ∖ ℋ⟩. Clearly, ℋ is an AR-hypothesis for in ′ if and only if ⟨ , ∪ ℋ⟩ |=AR if and only if is unsatisfiable.
Cardinality-minimal hypotheses: For membership, recall that for a given AR-abduction problem ⟨, ⟩ , the singleton set {} is a solution if and only if there is any solution by Lemma 4. Hence, we can use the algorithm for general hypotheses and additionally check that |ℋ| = 1, yielding coNP-membership.
For hardness, we again adapt the reduction from unsatisfiability to AR-entailment. In particular, we modify the given CNF-formula before applying the reduction to ensure that a specific singleton ABox is an AR-hypothesis if and only if the CNF-formula is unsatisfiable. Let = { 1, . . . , } over variables = {1, . . . , }. Define
′ := ∪ {+1} for 1 ≤ ≤ , ′+1 := ¬+1 ∨ +2, and ′+2 := ¬+2 and let 1 := {′1, . . . , ′
+1} and 2 := 1 ∪{′+2}. Analogously to the construction of from in the hardness proof for general hypotheses above, we construct knowledge bases = ⟨ , ⟩ from for ∈ {1, 2}. Further, define 2′ := ⟨ , 2 ∖ { (, +2)}⟩. In order to show coNP-hardness, it remains to show that ⟨2′, ()⟩ is a valid AR-abduction problem and ℋ = { (, +2)} is a (≤ -minimal) solution to it if and only if is unsatisfiable.
Subset-minimal hypotheses: We can prove Π2P-membership similar to the case of ℰ ℒ⊥ in Theorem 10. For DP-hardness, we reuse the above reduction but first introduce some terminology. Given a formula in CNF, a collection ⊆ of clauses is a minimal unsatisfiable subset (MUS) of if is unsatisfiable but ′ is satisfiable for every ′ ⊂ . It can be observed that the subset-minimal AR-hypotheses ℋ for in ′ correspond precisely to MUSes ℋ for by taking ∈ ℋ ⇐⇒ (, ) ∈ ℋ. Then, the claim follows by observing that the problem to decide if a set of clauses is a MUS is DP-hard [30]. For hardness, we reuse the reduction from above and encode a given set into the hypothesis as ℋ = { (, ) | ∈ }.
Summary. In this paper, we provided an initial study on ABox abduction under repair semantics building on the work from [23]. Our main contributions include new minimality criteria for preferred hypotheses w.r.t. inconsistent KBs and initial complexity results for the existence and the verification problem for flat ABox abduction and atomic BIQs as observations. Our results on combined complexity show that with an unrestricted signature, the complexity can be lower than for the entailment under repair semantics, while signature restrictions can make the problems computationally harder. Verification stays as hard as deciding classical entailment, but the choice of minimality criteria can increase the complexity (e.g., ⊆-minimality).
Future Work. For our initial setting considered, we have a complete picture of the complexity regarding Brave semantics, whereas the complexity analysis for AR semantics has some gaps. It seems that these gaps can be explained by the non-convex behavior of AR-hypotheses that was illustrated in Section 3. We plan to explore these efects further and complete the complexity landscape for the considered problems and more expressive formulas as observations. Moreover, the complexity when considering conflict-confining hypotheses also remains open for certain cases, even for Brave-semantics. Having established a complete picture regarding the combined complexity, we also intend to see the efect of a ifxed TBox by considering the data complexity. One can observe that several results from the current paper already transfer to the data complexity since the employed reductions result in a fixed TBox.
There are many directions for future work regarding extensions of the fairly limited initial setting
studied here. One particularly interesting direction is to explore the related problems from the literature
on abduction, such as necessity and relevance of axioms in hypotheses, which have been treated to
a certain extent in [24]. Moreover, the abduction problem with size restrictions has been considered
before in propositional logic [31, 32]. In our setting, it seems interesting to impose size restrictions for
a hypothesis but also for the corresponding set of conflicts. Additionally, the signature-based settings
considered previously only restrict concepts and roles [
We thank the anonymous reviewers for insightful comments and constructive feedback. The third author appreciates funding by DFG grant TRR 318/1 2021 – 438445824.
The author(s) have not employed any Generative AI tools. Representation and Reasoning, KR 2020, AAAI Press, 2020, pp. 592–602. URL: https://doi.org/10. 24963/kr.2020/59. [13] M. Bienvenu, Complexity of abduction in the ℰ ℒ family of lightweight description logics, in: Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning, KR 2008, AAAI Press, 2008, pp. 220–230. URL: http://www.aaai.org/Library/KR/ 2008/kr08-022.php. [14] B. Glimm, Y. Kazakov, M. Welt, Concept abduction for description logics, in: Proceedings of the 35th International Workshop on Description Logics (DL 2022) co-located with Federated Logic Conference (FLoC 2022), Haifa, Israel, August 7th to 10th, 2022, 2022. URL: https://ceur-ws.org/ Vol-3263/paper-11.pdf. [15] C. Alrabbaa, S. Borgwardt, T. Friese, A. Hirsch, N. Knieriemen, P. Koopmann, A. Kovtunova, A. Krüger, A. Popovic, I. S. R. Siahaan, Explaining reasoning results for OWL ontologies with evee, in: Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, AAAI Press, 2024. URL: https://doi.org/10.24963/kr.2024/67. [16] J. Boborová, J. Kloc, M. Homola, J. Pukancová, Towards CATS: A modular ABox abduction solver based on black-box architecture (extended abstract), in: Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings, CEURWS.org, 2024. URL: https://ceur-ws.org/Vol-3739/abstract-8.pdf. [17] M. Bienvenu, R. Rosati, Tractable approximations of consistent query answering for robust ontology-based data access, in: F. Rossi (Ed.), IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, IJCAI/AAAI, 2013, pp. 775–781. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6904. [18] D. Lembo, M. Lenzerini, R. Rosati, M. Ruzzi, D. F. Savo, Inconsistency-tolerant query answering in ontology-based data access, J. Web Semant. 33 (2015) 3–29. doi:10.1016/J.WEBSEM.2015.04. 002. [19] G. Casini, T. A. Meyer, K. Moodley, U. Sattler, I. Varzinczak, Introducing defeasibility into OWL ontologies, in: Proceedings of the 14th International Semantic Web Conference, volume 9367 of Lecture Notes in Computer Science, Springer, 2015, pp. 409–426. doi:10.1007/978-3-319-25010-6\ _27. [20] P. A. Bonatti, M. Faella, I. M. Petrova, L. Sauro, A new semantics for overriding in description logics, Artif. Intell. 222 (2015) 1–48. doi:10.1016/J.ARTINT.2014.12.010. [21] M. Pensel, A. Turhan, Reasoning in the defeasible description logic ℰ ℒ - computing standard inferences under rational and relevant semantics, Int. J. Approx. Reason. 103 (2018) 28–70. doi:10. 1016/J.IJAR.2018.08.005. [22] M. Bienvenu, A short survey on inconsistency handling in ontology-mediated query answering,
Künstliche Intell. 34 (2020) 443–451. doi:10.1007/S13218-020-00680-9. [23] J. Du, K. Wang, Y. Shen, Towards tractable and practical abox abduction over inconsistent description logic ontologies, in: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 1489–1495. URL: https://doi.org/10.1609/aaai.v29i1.9393. [24] M. Bienvenu, C. Bourgaux, F. Goasdoué, Computing and explaining query answers over inconsistent DL-Lite knowledge bases, Journal of Artificial Intelligence Research 64 (2019) 563–644. [25] T. Lukasiewicz, E. Malizia, C. Molinaro, Explanations for negative query answers under inconsistency-tolerant semantics, in: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, ijcai.org, 2022, pp. 2705–2711. doi: 10.24963/IJCAI. 2022/375. [26] A. Haak, P. Koopmann, Y. Mahmood, A.-Y. Turhan, Why not? developing abox abduction beyond repairs, CoRR abs/2507.21955 (2025). arXiv:2507.21955. [27] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
University Press, 2017. [28] N. Pippenger, Theories of computability, Cambridge University Press, 1997. [29] M. Bienvenu, C. Bourgaux, Inconsistency-tolerant querying of description logic knowledge bases, in: Reasoning Web: Logical Foundation of Knowledge Graph Construction and Query Answering