Paper deep dive
The More the Merrier: Combining Properties for ABox Abduction under Repair Semantics for ELbot
Anselm Haak, Patrick Koopmann, Yasir Mahmood, Anni-Yasmin Turhan
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 98%
Last extracted: 6/21/2026, 3:44:43 AM
Summary
This paper investigates the computational complexity of ABox abduction under repair semantics (specifically Brave and AR semantics) for the description logic EL_bot. The research focuses on the 'existence' and 'verification' problems when hypotheses are required to satisfy multiple properties simultaneously, such as signature-restriction, non-triviality, and conflict-confinement. The authors demonstrate that requiring additional properties like non-triviality or signature-restriction often does not increase the complexity of the abduction problem, and they provide specific complexity results for combinations of these properties.
Entities (8)
Relation Signals (4)
Non-triviality → isapropertyof → ABox Abduction
confidence 100% · the hypothesis should not contain the observation... a number of additional properties and minimality criteria for hypotheses have been introduced.
Conflict-confinement → isapropertyof → ABox Abduction
confidence 100% · the typical requirement of consistency of the hypothesis... we may require the hypothesis to be conflict-confining
ABox Abduction → operatesunder → Brave Semantics
confidence 100% · ABox abduction under repair semantics... for EL_bot under brave and AR semantics.
ABox Abduction → operatesunder → AR Semantics
confidence 100% · ABox abduction under repair semantics... for EL_bot under brave and AR semantics.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Abduction is a central approach to explain missing entailments from a knowledge base by providing a hypothesis, that would, if added to the knowledge base, make the missing entailment become true. Abduction under repair semantics has recently been investigated in detail, where several desirable properties and optimality criteria were considered, such as signature-restrictions and minimality in size and of introduced conflicts. Naturally, hypotheses that satisfy more than one of these properties or combine a property with an optimality criterion would be even more desirable for applications. So far, such hypotheses have not been investigated in the literature. In the present paper, we consider the ABox abduction problem for hypotheses satisfying more than one property or additional optimality criteria, for EL_bot under brave and AR semantics. Our main observation is that often requiring additional properties for hypotheses does not lead to an increase of complexity.
Tags
Links
- Source: https://arxiv.org/abs/2606.19197v1
- Canonical: https://arxiv.org/abs/2606.19197v1
Trouble viewing inline? Open PDF directly →
Full Text
117,945 characters extracted from source content.
Expand or collapse full text
[The More the Merrier: Combining Properties for ABox Abduction under Repair Semantics for ℰℒ⊥EL_ ] [orcid=0000-0003-1031-5922, email=anselm.haak@uni-paderborn.de, ] [orcid=0000-0001-5999-2583, email=p.k.koopmann@vu.nl, url=https://pkoopmann.github.io, ] [orcid=0000-0002-5651-5391, email=yasir.mahmood@uni-paderborn.de, ] [orcid=0000-0001-6336-335X, email=turhan@uni-paderborn.de ] The More the Merrier: Combining Properties for ABox Abduction under Repair Semantics for ELbot Anselm Haak Knowledge Representation Group, Paderborn University, Germany Patrick Koopmann Knowledge in Artificial Intelligence, Vrije Universiteit Amsterdam, The Netherlands Yasir Mahmood Data Science Group, Paderborn University, Germany Anni-Yasmin Turhan Abstract Abduction is a central approach to explain missing entailments from a knowledge base by providing a hypothesis, that would, if added to the knowledge base, make the missing entailment become true. Abduction under repair semantics has recently been investigated in detail, where several desirable properties and optimality criteria were considered, such as signature-restrictions and minimality in size and of introduced conflicts. Naturally, hypotheses that satisfy more than one of these properties or combine a property with an optimality criterion would be even more desirable for applications. So far, such hypotheses have not been investigated in the literature. In the present paper, we consider the ABox abduction problem for hypotheses satisfying more than one property or additional optimality criteria, for ℰℒ⊥E\!L_ under brave and AR semantics. Our main observation is that often requiring additional properties for hypotheses does not lead to an increase of complexity. keywords: Abduction semantics -tolerant reasoning 1 Introduction Explainability remains a core feature of knowledge-based AI systems, including those using description logic ontologies. Developing methods that can also practically explain decisions made by such systems is crucial in order to exploit this feature. While there is a lot of work on explaining reasoning results under classical semantics [SchlobachC03, AlrabbaaBFHKKKK24, Koopmann25], this problem is less investigated for non-classical semantics. In this paper, we consider repair-based semantics, which are a family of well-understood semantics that allow to define meaningful entailments from inconsistent knowledge bases [BienvenuB16]. As the name suggests, these semantics are based on repairs, which are maximal consistent subsets of the ABox. Depending on the chosen semantics, we may then consider those entailments that hold in at least one of the repairs (brave semantics), or only those entailments that hold in all of the repairs (AR semantics). Since inconsistencies can easily occur in realistic data, inconsistency-tolerant semantics are often indispensable. Unfortunately, they also make it more challenging to understand entailments from a user perspective. To explain why an assertion is entailed, we may need to provide explanations for the different repairs at the same time. For explaining missing entailments, the situation is even more complex: Indeed, under repair-based semantics, two things can contribute to the non-entailment of an assertion α: 1) some other assertions “block” the entailment of α, because they create a conflict with required assertions, or 2) assertions that are needed for the entailment are missing. While explanations based on Situation 1 have been investigated in detail [bienvenu2019computing, lukasiewicz2022explanations], we focus here on explanations based on Situation 2. Interestingly, no one so far considered explanations that combine Situations 1) and 2), i.e., where assertions can both be added and removed. We prefer to first fully understand abductive reasoning under repair-based semantics, and investigate more advanced notions of explanations in the future. Focusing on Situation 2, this corresponds to explaining missing entailments using abductive reasoning, which is also a typical means of explaining missing entailments under classical semantics [Elsenbroich2006, Klarman2011, Calvanese2013, du2015towards, AlrabbaaBFHKKKK24, Ceylan2020, Koopmann21a]. In particular, given a knowledge base K and an assertion α, ABox abduction is concerned with finding a set of assertions ℋH, called hypothesis, s.t. ∪ℋ⊧αK α, where usually additional properties are required for ℋH. ABox abduction is not only useful for explaining missing entailments, it can also be used for diagnosis [Elsenbroich2006, ObeidOMO19, Ceylan2020, Koopmann21a] and for repairing incomplete knowledge bases [WeiKleinerDragisicLambrix2014, du2017practical, Haifani2022]. If we replace the classical entailment relation with entailment under repair-based entailment, we obtain the notion of ABox abduction under repair-based semantics. Example 1. Consider the following excerpt from a medical ontology T on diabetes: High⊓Low⊑⊥∃glucoseLevel.High⊓OverdosedInsulin⊑DiabeticComa .High ∃glucoseLevel.High⊑GlycemicCrisis∃glucoseLevel.Low⊑GlycemicCrisis .High \, .Low GlycemicCrisis⊓Ketoacidosis⊑DiabeticComa Our ABox A contains information about a patient obtained through a glucose monitor and a finger stick sensor: glucoseLevel(patient,l)High(l)Low(l)glucoseLevel(patient,l) (l) (l) Because the two sensors provided contradictory information, the knowledge base is inconsistent. We observe that the patient passed out and want to use abduction to obtain a possible diagnosis. Since our data is contradictory, we apply repair-based semantics. Both OverdosedInsulin(patient)\\ OverdosedInsulin(patient)\ \ and Ketoacidosis(patient)\\ Ketoacidosis(patient)\ \ are hypotheses under Brave semantics, while only Ketoacidosis(patient)\\ Ketoacidosis(patient)\ \ is a hypothesis under AR semantics. Indeed, the cautious doctor should investigate this hypothesis first. conflict-confiningΣ2 P_2/ co NPΣ -restricted NP/Σ2 P_2non-trivial NP/Σ2 P_2Σ2 P_2/Σ2 P_2 NP/Σ2 P_2Σ2 P_2/Σ2 P_2 conflict-confining DP/ co NP⊆ -minimal DP/Π2 P_2non-trivial or Σ -restricted NP/ co NP≤-minimal NP/ co NP⊆c _c-minimalΠ2 P_2/ co NP DP/ co NP DP/Π2 P_2 DP/in Π2, P_2, co NP-h DP/Π2 P_2Π2 P_2/ co NPΠ2 P_2/Π2 P_2 Figure 1: Complexity results for Existence (Left) and Verification (Right) problem under combination of properties. Each node contains a property and its complexity for brave (red) and AR (blue) semantics, highlighting our earlier results [HaakKMT2026]. The edges represent the complexity when combining properties at the two end points, depicting our novel contributions. We recently proposed and investigated a range of desirable properties for abductive hypotheses under repair-based semantics. Some of these have been considered also under classical semantics, such as non-triviality (the hypothesis should not contain the observation) [Elsenbroich2006], subset and cardinality minimality [Calvanese2013], and restrictions on the concept and role names to be used (signature-restricted hypotheses) [Koopmann21a]. On the other hand, the typical requirement of consistency of the hypothesis with the knowledge base, which is also needed to avoid far-fetched explanations, makes less sense in an inconsistency-tolerant setting, where the knowledge base may already be inconsistent from the start. Instead, we may require the hypothesis to be conflict-confining [du2015towards], which means that it does not introduce any new conflicts, or at least conflict-minimal, which means it does not introduce more conflicts than necessary. In a recent conference publication [HaakKMT2026], complementing the research by du2015towards [du2015towards] that focused on conflict-confining hypotheses under IAR semantics, we analysed the computational complexity of abduction for each of these properties, considering brave and AR semantics for DL-LiteDL -Lite and ℰℒ⊥E\!L_ . In particular, we looked at the verification problem (is a given set of assertions a hypothesis satisfying the requirement), and the existence problem (is there any such hypothesis). An overview of our earlier results [HaakKMT2026] is shown in Figure˜1. This investigation considered the different properties in isolation, and left open the question of what happens if one desires more than one property to hold, for instance, if the hypothesis should be both non-trivial and conflict-confining, or subset-minimal among all the signature-restricted hypothesis. These and other combinations are very natural, which is why we have a closer look at them in this paper. This time, we focus on ℰℒ⊥E\!L_ . Specifically, we again investigate the theoretical complexity of the verification and the existence problem for hypotheses that satisfy two of the properties in Figure˜1, and that combine one property with one of the minimality requirements. 2 Preliminaries For a general introduction to description logics, we refer the reader to DBLP:books/daglib/0041477 (DBLP:books/daglib/0041477). In this paper, ABox assertions refer to concept assertions of the form A(a)A(a) and role assertions of the form r(a,b)r(a,b) for a concept name A, role name r and individuals a,ba,b. In other words, we only use concept assertions without complex concepts, which are also known as flat or simple assertions. We assume familiarity with computational complexity [DBLP:books/daglib/0092426], in particular with the complexity classes ,,, NL, P, NP, co NP, Σ2 P_2 and Π2 P_2, as well as DP, the class of decision problems representable as the intersection of a problem in NP and a problem in co NP. 2.1 Repair Semantics If a knowledge base is inconsistent, repair semantics can “restore” consistent versions and admit meaningful reasoning again. We focus here on ABox repairs and define these as well as two common kinds of repair semantics next. We will often use the following notions of consistency and inconsistency w.r.t. a TBox T. An ABox A is T-consistent, if ⟨,⟩⊧̸⊥ ,A , and T-inconsistent otherwise. Further, we say that A is a T-support of a concept assertion α, if ⟨,⟩⊧α ,A α. Let =⟨,⟩K= ,A be an inconsistent knowledge base and α be a Boolean (conjunctive) query. A repair of K is a T-consistent subset ℛ⊆R and subset-maximal with this property, i.e., there is no T-consistent subset ℛ′⊆R that is a strict superset of ℛR. The somewhat dual notion is a conflict or conflict set C, which is a T-inconsistent subset of the ABox and subset-minimal with this property. We denote by Conf()Conf(K) the set of conflicts of K. We recall entailment under Brave [BienvenuR13] and AR semantics [LLRRS-JWS-15]: • ⊧BraveαK _ Braveα iff there is a repair ℛR of K s.t. ⟨,ℛ⟩⊧α ,R α. • ⊧ARαK _ ARα iff ⟨,ℛ⟩⊧α ,R α for every repair ℛR of K. The complexity of query entailment under repair semantics is well understood [BienvenuB16]: For ℰℒ⊥E\!L_ , checking entailment of a concept assertion under Brave semantics is NP-complete in combined complexity, while it is coNP-complete under AR semantics. 2.2 ABox Abduction for Inconsistent KBs We now introduce the necessary notions for ABox abduction under repair semantics, as introduced in [HaakKMT2026]. We begin with the central definitions of abduction problems and hypotheses in this setting. Definition 2. Let =⟨,⟩K= ,A be an inconsistent KB, α a concept assertion (called an observation) and ∈Brave,ARS∈\ Brave, AR\ such that ⊧̸αK _Sα. Then, the pair ⟨,α⟩ ,α is called an S-abduction problem. A solution for such a problem, called S-hypothesis, is an ABox ℋH using only individuals occurring in K and α s.t. ⟨,∪ℋ⟩⊧α ,A _Sα. Additionally, for a set Σ (signature) containing individual, concept and role names, we define the triple ⟨,α,Σ⟩ ,α, to be a Σ -restricted S-abduction problem. A solution for such a problem is an ABox ℋH using only symbols from Σ that is an S-hypothesis for ⟨,α⟩ ,α . Note also that we do not admit fresh individuals beyond the specified signature as it is done for example in [Koopmann21a]. Abduction with fresh individuals easily becomes ExpTime-hard in ℰℒ⊥E\!L_ [Koopmann21a]. Because there are at most exponentially many repairs, the complexity is in this case dominated by the complexity of (classical) abduction, so such a setting might make our complexity analysis less insightful. To obtain hypotheses that are meaningful for explanation purposes, a number of additional properties and minimality criteria for hypotheses that yield preferred hypotheses have been introduced. For two sets S1,S2S_1,S_2 we may abbreviate |S1|≤|S2| S_1 ≤ S_2 by S1≤S2S_1≤ S_2. We next provide the definition of these properties and notions of minimality. Definition 3. Let ∈Brave,ARS∈\ Brave, AR\, ⟨,α⟩ ,α an S-abduction problem, and ⪯∈⊆,≤ ∈\ ,≤\. An ABox ℋH is 1. conflict-confining for =⟨,⟩K= ,A , provided that Conf(⟨,∪ℋ⟩)=Conf()Conf( ,A )=Conf(K). If ℋH is an S-hypothesis for ⟨,α⟩ ,α , we call it 2. non-trivial, if α∉ℋα , 3. ⪯ -minimal, if there is no S-hypothesis ℋ′H for ⟨,α⟩ ,α s.t. ℋ′≺ℋH , and 4. ⪯c _c-minimal, if there is no S-hypothesis ℋ′H for ⟨,α⟩ ,α s.t. Conf(⟨,∪ℋ′⟩)≺Conf(⟨,∪ℋ⟩)Conf( ,A ) ( ,A ). Conflict-confinement can be equivalently defined by requiring that ⟨,ℛ∪ℋ⟩⊧̸⊥ ,R for every repair ℛR of K. Note that hypotheses introducing new conflicts can be desirable, as erroneous facts might need to implicitly be replaced by new facts, leading to conflicts when considering both together. We use the terms subset-minimal for ⊆ -minimal and cardinality-minimal for ≤-minimal. Further, we also consider minimal variants of hypotheses with additional properties: For example, a ⊆ -minimal conflict-confining AR-hypothesis need only be ⊆ -minimal among all conflict-confining AR-hypotheses. We investigate the following reasoning problems for a given (Σ -restricted) S-abduction problem. Definition 4 (Reasoning Problems). Given a (Σ -restricted) S-abduction problem =⟨,α⟩ A= ,α (=⟨,α,Σ⟩ A= ,α, ), 1. the existence problem asks whether A has a solution, and 2. the verification problem asks whether a given ABox ℋH is a hypothesis for A (over Σ ). We restate the following two results that were established in [HaakKMT2026]. Lemma 5. Given a KB K and an ABox ℋH, checking whether ℋH is conflict-confining for K is coNP-complete. Lemma 6. Let ⟨,α⟩ ,α be an AR-abduction problem. The following are equivalent: 1. there is an AR-hypothesis for ⟨,α⟩ ,α , 2. α\α\is a conflict-confining AR-hypothesis for ⟨,α⟩ ,α . 3 Complexity Results for Combinations of Multiple Properties We will now establish the complexity of existence and verification of hypotheses for combinations of two of the properties of being Σ -restricted, non-trivial and conflict-confining, as well as of one of these properties together with one of the minimality criteria. Note that the combination of conflict-confining with one of the minimalities regarding the set of conflicts does not make sense, as the set of conflicts for a conflict-confining hypothesis is always minimal. Regarding the combination of Σ -restriction with other properties or minimality criteria, we immediately obtain the following general observation: any hardness result for the individual properties directly carries over to the case were Σ -restriction is required additionally. To see this, observe that one can always set Σ to the (full) signature of the given abduction problem, ensuring that Σ does not actually restrict the solutions. Observation 7. Let P be a property of hypotheses considered in this paper. Then, the existence (resp., verification) of S-hypotheses with property P can be reduced in polynomial time to the existence (resp., verification) of Σ -restricted S-hypotheses with property P for ∈Brave,ARS∈\ Brave, AR\. 3.1 Existence Here, we consider the existence problem for combinations of the three main properties of hypotheses. Note that minimality criteria are not interesting for existence, as there is a minimal hypothesis with certain properties iff there is any such hypothesis. First, we briefly motivate the combination of Σ -restriction and non-triviality. One main motivation for using Σ -restriction can be to avoid trivial hypotheses. However, a non-trivial hypothesis might still use all the symbols from the observation, just in different combinations. Consequently, we might lose relevant hypotheses if we use this trick. The following example illustrates such a situation: Example 8. Let ≔⟨,⟩K ,A be a KB with ≔A⊓B⊑C,D⊓∃r.C⊑AT \A B C,D ∃ r.C A\ and ≔B(m),r(m,n)A \B(m),r(m,n)\. Moreover, let α≔C(m)α C(m) be the observation and Σ≔C,D,m,n \C,D,m,n\ be the signature. Here, the trivial hypothesis C(m)\C(m)\ is in fact also Σ -restricted. The hypothesis ℋ1≔A(m)H_1 \A(m)\ is non-trivial but outside our signature. Moreover, ℋ2≔C(n),D(m)H_2 \C(n),D(m)\ is non-trivial and uses both C and m, that is, both the concept name and the individual from the observation. Turning to the complexity results, the combination of signature restriction and non-triviality does not affect the overall complexity, as the individual cases exhibit the same computational behavior. Corollary 9. The existence problem for non-trivial Σ -restricted S-hypotheses is (i) NP-complete, for =BraveS= Brave, and (i) Σ2 P_2-complete, for =ARS= AR. Proof. We recall the membership for the non-trivial case (Figure˜1). For Brave semantics, existence of a non-trivial Brave-hypothesis for an instance ⟨,⟩,α⟩ ,A ,α can be checked by guessing a candidate hypothesis ℋH over the signature of ⟨,α⟩ ,α , as well as a candidate repair ℛR of ⟨,∪ℋ⟩ ,A and verifying in polynomial time that ℋH is non-trivial, ℛR is a repair, and ⟨,ℛ⟩⊧α ,R α. For AR semantics, we guess a hypothesis ℋH as before, and verify that ℋH is non-trivial and ⟨,∪ℋ⟩⊧ARα ,A _ ARα. The latter is AR-entailment, which can be handled by querying an NP oracle. For the combination, note that both sketched approaches are guess-and-check algorithms, so we can simply include a check for Σ -restriction of ℋH. Hence, we get the same complexity upper bounds as for the non-trivial setting. The hardness in both cases follows from the lower bound for existence of non-trivial hypotheses combined with ˜7. ∎ Interestingly, adding signature restriction, or non-triviality, on top of conflict-confinement, yields two cases in which both semantics incur the same “higher” complexity. Theorem 10. The existence problem for conflict-confining non-trivial S-hypotheses is Σ2 P_2-complete for ∈Brave,ARS∈\ Brave, AR\. This also holds for the case of conflict-confining Σ -restricted S-hypotheses and the case of conflict-confining non-trivial Σ -restricted S-hypotheses. Proof idea. For membership, we guess a hypothesis ℋH over the signature of K and verify that ℋH is non-trivial, ⟨,∪ℋ⟩⊧α ,A _Sα, and ℋH is conflict-confining. The first check can easily be done in polynomial time, while the last two checks can be performed via NP-oracle calls, yielding Σ2 P_2-membership. In particular, S-entailment has NP (resp., coNP) complexity for =BraveS= Brave (=ARS= AR), while the complexity for checking conflict-confinement was stated in Lemma˜5. When adding Σ -restriction, we guess ℋH over the given signature Σ (instead of the signature of ⟨,α⟩) ,α ), and if we drop the requirement for non-triviality, the corresponding check is dropped. In both cases, we obtain Σ2 P_2-membership. For hardness, we first consider the case of brave semantics. The existence of conflict-confining Brave-hypotheses is Σ2 P_2-complete (Figure˜1) and we observe that the reduction easily extends to our present case. For non-trivial, the proof follows by observing that the employed reduction constructs a hypothesis that is always non-trivial (see appendix). When adding Σ -restriction (with or without non-triviality), hardness is retained due to ˜7. For AR semantics, we observe that the existence problem for non-trivial hypotheses (Figure˜1) is Σ2 P_2-complete. We argue that the reduction employed for hardness in that result extends to the combination of non-triviality with conflict-confinement. This requires us to prove that the considered hypothesis in the reduction is indeed conflict-confining. We find it convenient to present the reduction here for completeness. For hardness, we reduce from the validity problem for ∃∀∃∀-QBFs. Let Ψ=∃Y∀Zψ =∃ Y∀ Z\;ψ be an ∃∀∃∀-QBF, where ψ is in DNF, and let X=Y∪ZX=Y∪ Z. We construct a TBox T using concept names N=Ax,Ax¯∣x∈X∪C,AψN=\A_x,A_ x x∈ X\∪\C,A_ψ\. Intuitively, T expresses that for any term t∈ψt∈ψ, the conjunction of concepts corresponding to the literals in t entails the concept AψA_ψ, which represents satisfaction of ψ. To this end, we define ≔⟨,⟩K ,A , where ≔Ax⊓Ax¯⊑⊥∣x∈X∪C⊓⨅ℓ∈tAℓ⊑Aψ∣t∈ψ, \\,A_x A_ x x∈ X\,\∪ \\,C _ ∈ tA_ A_ψ t∈ψ\, \, ≔Az(m),Az¯(m)∣z∈Z \\,A_z(m),A_ z(m) z∈ Z\ for an individual name m. Now, ⟨,Aψ(m)⟩ ,A_ψ(m) is the desired abduction problem. Observe that ℋtriv≔Aψ(m)H_triv \A_ψ(m)\ is the trivial AR-hypothesis for ⟨,α⟩ ,α . However, we are considering existence of a non-trivial hypotheses here, i.e., one that does not contain Aψ(m)A_ψ(m). Intuitively, any non-trivial hypothesis corresponds to an assignment satisfying the formula ∀Zψ∀ Z\,ψ, containing assertions for all literals over Y satisfied by the assignment. It is not hard to see that adding such hypotheses to K does not introduce new conflicts, and that there is no need to include additional assertions, allowing us to prove the following claim. Claim 1. Ψ is true iff ⟨,α⟩ ,α admits a non-trivial conflict-confining AR-hypothesis. Hardness when adding Σ -restriction to either of the cases again follows from ˜7. ∎ 3.2 Verification We now turn towards verification. We first argue that the combinations of the main properties (without minimality criteria) can be handled similar as for existence. Observe that the verification problem for either signature-restricted, or non-trivial S-hypotheses admits the same complexity as S-entailment for ∈Brave,ARS∈\ Brave, AR\. Given an instance ⟨,α⟩ ,α of S-abduction problem with =⟨,⟩K= ,A , verifying that an ABox ℋH is a non-trivial S-hypothesis requires that (1) ⟨,∪ℋ⟩⊧α ,A _Sα, and (2) ℋHis non-trivial. Here, the complexity is dominated by the first check, as the second step can be performed in polynomial time. Similarly, for Σ -restriction, step (2) above can be replaced by a check that ℋH is Σ -restricted, which again takes polynomial time. Further, the same is still true when combining non-triviality with Σ -restriction. The lower bound follows from hardness of verification for (general) S-hypotheses and non-trivial S-hypotheses combined with ˜7, yielding the following corollary. Corollary 11. Verification of non-trivial S-hypotheses and of Σ -restricted S-hypotheses is (i) NP-complete for =BraveS= Brave, and (i) co NP-complete for =ARS= AR. Moreover, the same is true when combining both properties, i.e., for verification of non-trivial Σ -restricted S-hypotheses. It is already known that adding conflict-confinement increases the complexity for verification, but only for brave semantics (Figure˜1). We next prove that adding non-triviality or Σ -restriction does not increase the complexity beyond that of checking that a given ABox is a conflict-confining hypothesis. Theorem 12. Verification of non-trivial conflict-confining S-hypotheses is (i) DP-complete for =BraveS= Brave, and (i) co NP-complete for =ARS= AR. The complexity remains the same when non-triviality is replaced by Σ -restriction, and when requiring all three properties. Proof idea. The hardness applies due to the case of verification for conflict-confining hypotheses since the considered hypotheses in each case are indeed non-trivial (see appendix). Hardness when adding Σ -restriction to either of the cases again follows from ˜7. We give a bit more detail for the case of conflict-confining non-trivial hypotheses. For brevity, we only outline the proof for Brave semantics, which utilises a reduction from the combination of entailment and non-entailment under Brave semantics to verification of non-trivial conflict-confining Brave-hypotheses. Given an instance ⟨,α1,α2⟩ , _1, _2 for some inconsistent KB K, the problem asks whether ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. This problem is DP-complete because the first question is NP-complete and the second question is coNP-complete under Brave semantics: Membership follows immediately, while only using a single KB in the problem is a slight obstacle to showing hardness. To address this, reduce from the variant of the problem with two KBs by first ensuring that the first and the second part of the problem use disjoint sets of names, and then defining the new single KB as the disjoint union of both KBs. For the reduction to the abduction problem at hand, assume w.l.o.g. that α1 _1 and α2 _2 both use the same individual, but different concept names, and let α1=A(a) _1=A(a), α2=B(a) _2=B(a), with =⟨,⟩K= ,A . We consider fresh concepts C and D to construct a KB ′≔⟨′,⟩K ,A , for ′≔∪C⊓A⊑D,C⊓B⊑⊥,T ∪\C A D,C B \, an observation α≔D(a)α D(a), and a hypothesis ℋ≔C(a)H \C(a)\. It can now be shown that ℋH is a Brave-hypothesis for ⟨′,α⟩ ,α iff ⊧BraveA(a)K _ BraveA(a), and conflict-confining for ′K iff ⊧̸BraveB(a)K _ BraveB(a). Observing that α∉ℋα , we obtain the following claim, proving correctness. Claim 2. ℋH is a non-trivial conflict-confining Brave-hypothesis for α in ′K iff ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. We next prove membership in each case. Let ⟨,α⟩ ,α be an S-abduction problem with =⟨,⟩K= ,A and ℋH an ABox. We begin with Brave semantics. Observe that ℋH is a non-trivial conflict-confining Brave-hypothesis iff (1) ℋHis non-trivial, (2) ⟨,∪ℋ⟩⊧Braveα ,A _ Braveα, and (3) Conf(⟨,∪ℋ⟩)=Conf(⟨,⟩)Conf( ,A )=Conf( ,A ). Here, (1) can be easily checked in polynomial time. Moreover, (2) is instance checking for ℰℒ⊥E\!L_ under brave semantics and hence in NP, while (3) can be checked in coNP, since the complement can be checked by guessing a conflict C s.t. ∈Conf(⟨,∪ℋ⟩)C ( ,A ) and ∉Conf(⟨,⟩)C ( ,A ). Concretely, this amounts to guessing a ⊆∪ℋC such that: (a) ⊈C , (b) ⟨,⟩⊧⊥ ,C , and (c) ⟨,∖γ⟩⊧̸⊥ ,C \γ\ any γ∈Cγ∈ C. Checking whether C satisfies (a)–(c) can be done in polynomial time. Altogether, (a) and (b) together are in NP, while (c) is in coNP. Hence, the problem is contained in DP. The membership proof for brave semantics can be adapted to the cases where Σ -restriction is added as a requirement, or replaces non-triviality, by noting that checking Σ -restriction on top or instead of non-triviality can also be done in polynomial time. We now turn to membership for AR-semantics. First, check non-triviality of ℋH in polynomial time. If this is the case, ℋH is a non-trivial conflict-confining AR-hypothesis iff (1) ⟨,∪ℋ⟩⊧ARα ,A _ ARα, and (2) ℋHis conflict-confining in K, i.e., Conf(⟨,∪ℋ⟩)=Conf(⟨,⟩)Conf( ,A )=Conf( ,A ). As a result, one can guess a candidate repair ℛR and a candidate conflict C of ⟨,∪ℋ⟩ ,A simultaneously, as a counter example to ℋH being an AR-hypothesis (ℛR) and conflict-confining (C). More precisely, one needs to check that ℛR is a subset-maximal T-consistent subset of A (hence a repair) and ⟨,ℛ⟩⊧̸α ,R α, as well as that ∉Conf(⟨,⟩)C ( ,A ), but ∈Conf(⟨,∪ℋ⟩)C ( ,A ). All these checks can be performed in polynomial time. The claimed coNP-membership follows by observing that ℋH is a conflict-confining hypothesis for α in K iff both these checks return false. Membership when adding Σ -restriction to the conflict-confining and the conflict-confining non-trivial case again follows by noting that Σ -restriction can be checked separately in polynomial time. ∎ Combination of Properties with Minimality Criteria We next turn towards combinations involving minimality criteria, beginning with ⊆ -minimality. Here, the following general observation regarding our main properties is very helpful. Observation 13. The properties of being conflict-confining, non-trivial, and Σ -restricted are downwards-closed. More precisely, let ⟨,α⟩ ,α be an S-abduction problem for ∈Brave,ARS∈\ Brave, AR\, ℋH an ABox and ℋ′⊆ℋH . If ℋH is conflict-confining for K, then so is ℋ′H . Similarly, if α∉ℋα , then α∉ℋ′α , and if ℋH is an ABox over a signature Σ , then so is ℋ′H . This implies that an ABox ℋH being a ⊆ -minimal conflict-confining S-hypotheses is equivalent to ℋH being a ⊆ -minimal S-hypothesis and being conflict-confining (as a separate requirement). The same observation applies to the other two properties as well as combinations of properties. Using the established results on verification of ⊆ -minimal hypotheses and the above observation, we obtain the following complexities when additionally requiring other properties. Theorem 14. Verification of ⊆ -minimal non-trivial S-hypotheses is (i) DP-complete, for =BraveS= Brave, and (i) Π2 P_2-complete, for =ARS= AR. The complexity remains same when we replace non-triviality by Σ -restriction, and when combining both properties. Proof idea. The hardness in each case follows from the corresponding result on verification of ⊆ -minimal S-hypotheses (see appendix). Observe that the reduction in each case uses a non-trivial hypothesis, thus the hardness applies to verification of non-trivial subset-minimal hypotheses. Again, when adding Σ -restriction (either instead of or in combination with non-triviality), hardness is retained by ˜7. We outline the reduction for DP-hardness with Brave semantics as it it also used in later results. We reduce again from a combination of entailment and non-entailment under Brave semantics to verification of ⊆ -minimal Brave-hypotheses, similar to hardness under Brave semantics in the proof of Theorem˜12. Given an instance ⟨,α1,α2⟩ , _1, _2 for some inconsistent KB K, let α1=A(a) _1=A(a), α2=B(a) _2=B(a), and =⟨,⟩K= ,A . We now construct a KB ′K , an observation α, and an ABox ℋH as follows. Let ′≔⟨′,⟩K ,A with ′≔∪B⊑C,C⊓D⊓A⊑Q,T ∪\B C,C D A Q\, α≔Q(a)α Q(a), and ℋ≔C(a),D(a)H \C(a),D(a)\ for fresh concepts C,D,QC,D,Q. Intuitively, ℋH is a Brave-hypothesis for ⟨′,α⟩ ,α iff ⊧BraveA(a)K _ BraveA(a) and ℋH is ⊆ -minimal iff ⊧̸BraveB(a)K _ BraveB(a). To see the latter, note that ⊆ -minimality is violated iff D(a)\D(a)\ is also a Brave-hypothesis for ⟨′,α⟩ ,α , which is the case iff ⊧BraveB(a)K _ BraveB(a). The following claim shows correctness. Claim 3. ℋH is a ⊆ -minimal non-trivial hypothesis for ⟨′,α⟩ ,α iff ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. Membership follows from the the upper bound for verification of ⊆ -minimal S-hypotheses together with ˜13: By the observation, it is sufficient to check that ℋH is a ⊆ -minimal S-hypotheses, and separately checking that it is non-trivial or Σ -restricted. Since the latter two properties can be checked in P, we obtain the desired upper bounds. For this, note that both DP and Π2 P_2 are closed under intersection with languages from P. ∎ Verification of ⊆ -minimal conflict-confining hypotheses enjoys the same complexity for Brave-hypotheses, but the precise complexity of AR-hypotheses remains open for now. Theorem 15. Verification of ⊆ -minimal conflict-confining S-hypotheses is (i) DP-complete for =BraveS= Brave, while it is (i) in Π2 P_2 and coNP-hard for =ARS= AR. The same holds when additionally requiring non-triviality, Σ -restriction, or both. Proof idea. Membership for both semantics follows from the membership of verification of ⊆ -minimal S-hypotheses, again using ˜13: By the observation, it is sufficient to verify that ℋH is a ⊆ -minimal S-hypothesis, and separately checking that it is conflict-confining. As the latter is in coNP and both DP as well as Π2 P_2 are closed under intersection with languages from coNP, we obtain the desired upper bounds. As both non-triviality and Σ -restriction can even be checked in P, the same upper bound still holds when adding one or both of these properties. DP-hardness for Brave semantics follows due to the same complexity of verification of ⊆ -minimal Brave-hypotheses. We note that the considered hypothesis in the reduction employed for this case in Theorem˜14 is actually conflict-confining. As a result, ˜3 can be reused after replacing non-triviality by conflict-confinement. As argued, the constructed hypothesis is in fact both non-trivial and conflict-confining, thus the hardness also applies when adding non-triviality in the combination. Adding Σ -restriction can again be handled using ˜7. Finally, coNP-hardness for AR semantics follows from the reduction employed in the coNP-hardness proof for verification of conflict-confining AR-hypotheses [HaakKMT2026]. Precisely, reduce from AR-entailment as follows. Given a KB =⟨,⟩K= ,A and a concept assertion A(a)A(a), define the new KB ′=⟨′,⟩K = ,A , where ′≔∪X⊓A⊑CT ∪\X A C\, and let α≔C(a)α C(a) and ℋ≔X(a)H \X(a)\. We have ⊧ARA(a)K _ ARA(a) iff ⟨′,∪ℋ⟩⊧ARα ,A _ ARα. Furthermore, it is easy to see that ℋH is conflict-confining and minimality follows from |ℋ|=1|H|=1. Further, ℋH is non-trivial, while Σ -restriction can again be handled using ˜7, yielding hardness when adding one or both of these properties. ∎ Cardinality-minimality behaves similar to subset-minimality, if we consider either non-trivial or Σ -restricted hypotheses. It was shown in our earlier work [HaakKMT2026] that ≤-minimal S-hypotheses are of size 11, since there exists some S-hypothesis iff the (singleton) trivial hypothesis is one. This does not apply when considering ≤-minimal non-trivial (resp., Σ -restricted) hypotheses, as the trivial hypothesis is now disallowed (resp., can be disallowed). This explains the increased complexity in both cases when compared to the base case (verification of ≤-minimal S-hypotheses). Theorem 16. Verification of ≤-minimal non-trivial S-hypotheses is (i) DP-complete for =BraveS= Brave, and (i) Π2 P_2-complete for =ARS= AR. The complexity remains the same when we replace non-triviality by Σ -restriction, and when combining both properties. Proof. Brave semantics: For membership, one can guess a set ℋ′H of assertions over the signature of K such that ℋ′H is a counter-witness to ℋH being a ≤-minimal S-hypothesis for ⟨,α⟩ ,α . Precisely, ℋH is a ≤-minimal non-trivial Brave-hypothesis iff (1) it is a non-trivial Brave-hypothesis, and (2) there is no ℋ′H over the signature of K with α∉ℋ′α and |ℋ′|<|ℋ||H |<|H| s.t. ⟨,∪ℋ′⟩⊧Braveα ,A _ Braveα. Here, (1) can be verified in NP, while for (2), we guess as a counter-example both a set of assertions ℋ′H of size at most |ℋ|−1|H|-1 over the signature of K as well as a candidate repair ℛ⊆∪ℋ′R . We then verify that α∉ℋ′α , ℛR is a repair, and ⟨,ℛ⟩⊧α ,R α, which can all be checked in polynomial time. This shows that (2) can be checked in coNP, yielding DP-membership in total. The membership also applies when requiring Σ -restriction instead of (or in addition to) non-triviality, as verification of (non-trivial) Σ -restricted Brave-hypotheses is again in NP, and instead of (or in addition to) checking non-triviality ℋ′H , we can check that ℋ′H only uses names from Σ in polynomial time. For hardness, we reconsider the reduction employed in the case of verification of ⊆ -minimal Brave-hypotheses (Theorem˜14). We observe that the considered hypothesis ℋH is ⊆ -minimal iff ℋH is ≤-minimal. The reduction already applies for the non-trivial case as ℋH is non-trivial. The case of Σ -restriction can again be handled using ˜7. AR semantics: The Π2 P_2-membership can be shown similarly to DP-membership for Brave semantics above. Precisely, ℋH is a non-trivial ≤-minimal AR-hypothesis iff (1) it is a non-trivial AR-hypothesis, and (2) there is no ℋ′H over the signature of K with α∉ℋ′α and |ℋ′|<|ℋ||H |<|H| s.t. ⟨,∪ℋ′⟩⊧ARα ,A _ ARα. Here, (1) can be checked in coNP, while ℋ′H can be guessed as before. The main difference is that we do not guess a candidate repair, and instead check ⟨,∪ℋ′⟩⊧ARα ,A _ ARα using a coNP oracle. The cases obtained by replacing non-triviality by Σ -restriction or combining both can be handled in the same way as above for Brave semantics. For Π2 P_2-hardness, we reduce from the complement of the existence problem for non-trivial AR-hypotheses, which is Σ2 P_2-complete. Let ⟨,α⟩ ,α be an AR-abduction problem over some signature Σ _K and α≔C(m)α C(m). We consider Σ≔A(a)∣A,a∈Σ∪r(a,b)∣r,a,b∈ΣA_ \A(a) A,a∈ _K\∪\r(a,b) r,a,b∈ _K\ as the set of all the ABox assertions over Σ _K. It holds that ℋ⊆ΣH _ for any AR-hypothesis ℋH for ⟨,α⟩ ,α . As a result, any such hypothesis for α must have its size bounded by N=|Σ|N=|A_ |. To complete the reduction, we add fresh concept names Xi∣i≤N+1,Xi∉Σ\X_i i≤ N+1,X_i ∈ _K\, and define the new KB ′≔⟨′,⟩K ,A , where ′≔∪⨅1≤i≤N+1Xi⊑CT ∪\ _1≤ i≤ N+1X_i C\. Then, we use the observation α≔C(m)α C(m) as before and define ℋ≔Xi(m)∣i≤N+1H \\,X_i(m) i≤ N+1\,\. For correctness, we observe that ℋH is a non-trivial AR-hypothesis for ⟨′,C(m)⟩ ,C(m) of size N+1N+1, whereas any non-trivial AR-hypothesis for ⟨,α⟩ ,α has size ≤N≤ N (since |Σ|=N|A_ |=N). This implies the following equivalences: ℋH is not a ≤-minimal AR-hypothesis for ⟨′,C(m)⟩ ,C(m) iff there is a non-trivial AR-hypothesis for ⟨′,α⟩ ,α of size ≤N≤ N iff there is a non-trivial AR-hypothesis for ⟨,α⟩ ,α . This yields the mentioned Π2 P_2-hardness for the AR semantics. The case of Σ -restriction can again be handled using ˜7. ∎ Considering conflict-confinement with ≤-minimality, the complexity under AR semantics stays the same as for ≤-minimality alone, which follows from Lemma˜6. In contrast, the complexity again increases for Brave semantics. Similar to before, this comes from the fact that we do not have the trivial size bound of 11 in this case, and is closely related to existence of conflict-confining Brave-hypotheses. Theorem 17. Verification of ≤-minimal conflict-confining S-hypotheses is (i) Π2 P_2-complete for =BraveS= Brave, and (i) coNP-complete for =ARS= AR. Proof idea. For AR-semantics, Lemma˜6 implies that a given AR-hypothesis is ≤-minimal iff it is of size 11. The complexity now readily follows from coNP-completeness of AR entailment. We now turn to Brave semantics. For membership, we need to determine whether (1) ⟨,∪ℋ⟩⊧Braveα ,A _ Braveα, (2) ℋHis conflict-confining, and (3) there is no ℋ′H over the signature of K with |ℋ′|<|ℋ||H |<|H| that is conflict-confining for K and satisfies ⟨,∪ℋ′⟩⊧Braveα ,A _ Braveα. Here, one can guess the ABox ℋ′H as a counter-witness, and handle all the remaining checks needed in (1)–(3) via oracle calls. Consequently, we obtain membership in Π2 P_2. For hardness, we reduce from the complement of the existence problem for conflict-confining Brave-hypotheses. To this aim, we extend and reuse the reduction for this case from our earlier work [HaakKMT2026]. The trick we employ here (details in the appendix) is to use candidate hypothesis ℋH of very large size following a similar idea as in the proof of Theorem˜16 for the case of AR semantics. However, this trick cannot be applied as directly: We know that there might exist a conflict-confining hypothesis even though the observation itself is not conflict-confining. In this case, ℋH would also not be conflict-confining, interfering with the rest of the construction. Nevertheless, we invented a way to construct a hypothesis that avoids new conflicts [HaakKMT2026]. We apply the same strategy to our considered hypothesis ℋH here, which requires slightly changing the newly added TBox axiom in the proof of Theorem˜16. This yields the mentioned Π2 P_2-hardness. ∎ Finally, we consider ⊆c _c-minimality. Recall that the combination of ⊆c _c-minimality and conflict-confining is not interesting, since conflict-confining hypotheses are always ⊆c _c-minimal. We consider the remaining cases. Here, we have to determine whether a given non-trivial (or Σ -restricted) hypothesis is ⊆c _c-minimal among all such hypotheses. Considering AR semantics, although we know that the observation α has to be a conflict-confining AR-hypothesis in order for there to exist any AR-hypothesis by Lemma˜6, we do not know whether and how non-trivial (Σ -restricted) hypotheses create conflicts. Concretely, while it might appear counter-intuitive, AR-hypotheses are not necessarily conflict-confining. The following example highlights this observation. Example 18. Let ≔⟨,⟩K ,A where, ≔ \ A1⊓B1⊑⊥,A1⊓B2⊑⊥,A2⊓B1⊑⊥,A2⊓B2⊑⊥, A_1 B_1 , A_1 B_2 , A_2 B_1 , A_2 B_2 , A1⊓A2⊑C,B1⊓B2⊑C, A_1 A_2 C, B_1 B_2 C\, ≔ \ A1(m),B1(m). A_1(m),B_1(m)\. Now, let α≔C(m)α C(m) be our observation. Then, the ABox ℋ≔A2(m),B2(m)H \A_2(m),B_2(m)\ is not conflict-confining in K since, for example, ℋH itself is a new conflict in K. Nevertheless, ⟨,∪ℋ⟩⊧ARα ,A _ ARα, as the only repairs of ⟨,∪ℋ⟩ ,A are A1(m),A2(m)\A_1(m),A_2(m)\ and B1(m),B2(m)\B_1(m),B_2(m)\. Further, any non-trivial AR-hypothesis for ⟨,C(m)⟩ ,C(m) is a superset of ℋH, highlighting that non-trivial AR-hypotheses might need to introduce new conflicts. Theorem 19. Verification of ⊆c _c-minimal non-trivial S-hypotheses is Π2 P_2-complete for ∈Brave,ARS∈\ Brave, AR\. The complexity remains the same when we replace non-triviality by Σ -restriction or combine both. Proof. We begin with Brave semantics. For membership, one can guess as a counter-witness a set of assertions ℋ′H over the signature of ⟨,α⟩ ,α and verify that ℋ′H is a non-trivial Brave-hypothesis for α and ℋ′H admits fewer new conflicts than ℋH does. Precisely, ℋH is a ⊆c _c-minimal non-trivial Brave-hypothesis for ⟨,α⟩ ,α iff (1) ℋHis a non-trivial Brave-hypothesis for ⟨,α⟩ ,α , and (2) there is no ABox ℋ′H over the signature of ⟨,α⟩ ,α with α∉ℋ′α and ⟨,∪ℋ′⟩⊧Braveα ,A _ Braveα s.t. Conf(⟨,∪ℋ′⟩)⊊Conf(⟨,∪ℋ⟩)Conf( ,A ) ( ,A ). For (2), we can guess a counter-witness ℋ′H , while the remaining checks can be handled via oracle calls. To compare the sets of conflicts, we can check that every conflict in the first set is contained in the second and that there is a conflict in the second set that does not occur in the first, which can be checked in coNP and NP, respectively. This results in Π2 P_2-membership. For Σ -restriction, we check whether ℋH and ℋ′H only use names over Σ instead of (or in addition to) checking non-triviality. For hardness we reuse the same reduction as for the case of verification of ⊆c _c-minimal hypotheses (Figure˜1). Here, we observe that the reduction employs a non-trivial hypothesis (see appendix for details). Adding Σ -restriction can again be handled using ˜7. We now turn to AR semantics. Membership follows by the same argument as for Brave semantics, since the verification of non-trivial AR-hypotheses and the additional checks can again be handled via oracle calls after guessing a counter-witness ℋ′H . For hardness, we incorporate the idea from Example˜18 into our reduction for the existence of non-trivial conflict-confining AR-hypotheses from Theorem˜10. Let ⟨,α⟩ ,α be the AR-abduction problem constructed from an ∃∀∃∀-QBF Ψ as in the proof for Theorem˜10. We let A1,A2,B1,B2A_1,A_2,B_1,B_2 denote fresh concepts and consider the KB e≔⟨e,e⟩K_e _e,A_e as constructed in Example˜18. To complete the reduction, we set ′≔⟨′,′⟩K ,A where ′≔∪eT _e and ′≔∪eA _e and use the same observation α. Finally, we take the hypothesis ℋe≔A2(m),B2(m)H_e \A_2(m),B_2(m)\ as in the example, which creates precisely three new conflicts A1(m),B2(m)\\A_1(m),B_2(m)\, A2(m),B1(m)\A_2(m),B_1(m)\, and ℋeH_e. Then, the correctness follows from the following claim. Claim 4. Ψ is true iff ℋeH_e is not a non-trivial ⊆c _c-minimal AR-hypothesis for ⟨′,α⟩ ,α . Proof of Claim. Recall that Ψ is true iff ⟨,α⟩ ,α admits a non-trivial conflict-confining AR-hypothesis (˜1). We observe that ⟨,α⟩ ,α admits a non-trivial conflict-confining AR-hypothesis iff ⟨′,α⟩ ,α admits a non-trivial conflict-confining AR-hypothesis (the same one) iff ℋeH_e is not a ⊆c _c-minimal non-trivial AR-hypothesis for ⟨′,α⟩ ,α . Indeed, if Ψ is false, there is no AR-hypothesis over the signature of K that entails α. Hence, the only way to obtain the AR-entailment of α is via using new axioms in ′K . This renders ℋeH_e to be the only AR-hypothesis for α in ′K , and hence makes it trivially ⊆c _c-minimal. ∎ ∎ The membership in Theorem˜19 only applies to ⊆c _c-minimality and does not seem to extend to ≤c _c-minimality. While in the case of the former, the necessary comparison of the sets of conflicts introduced by ℋH and the guessed ABox ℋ′H can be handled using an NP oracle, this is not the case when we need to compare the cardinalities of these sets. Indeed, the following example illustrates that a relatively small hypothesis can trigger exponentially many new conflicts, hinting at potential #\# P-hardness of counting the number of conflicts. How this affects the complexity for ≤c _c-minimality is left for future work. Example 20. Let ≔⟨,⟩K ,A where, ≔C⊑D∪Ai⊑Xi,Bi⊑Xi∣i≤n∪D⊓X1⊓⋯⊓Xn⊑⊥, \C D\∪\\,A_i X_i,B_i X_i i≤ n\,\∪\D X_1 … X_n \, ≔Ai(m),Bi(m)∣i≤n. \\,A_i(m),B_i(m) i≤ n\,\. Now, let α≔D(m)α D(m) be our observation. Then, the ABox ℋ≔C(m)H \C(m)\ is a Brave hypothesis for ⟨,α⟩ ,α of size one. Nevertheless, ℋH triggers exponentially many new conflicts in K, each of the form C(m),Y1(m),Y2(m),…,Yn(m)\C(m),Y_1(m),Y_2(m),…,Y_n(m)\ where Yi∈Ai,BiY_i∈\A_i,B_i\ for all i. Note that K is a consistent KB to begin with. 4 Conclusion and Outlook We observe that combining basic properties (excluding minimality criteria) and potentially subset-minimality does not increase the complexity for either existence or verification of S-hypotheses in ℰℒ⊥E\!L_ : The complexity for all considered cases is governed by the highest complexity among the individual properties involved. In contrast, we often see an increase in the complexity, when combining cardinality-minimality or conflict-minimality with other properties. Observe that the hardness proofs for some of our results (e.g., Theorems 10, 14 and 15) do not use role assertions. Consequently, several of our results already hold for propositional Horn logic. Nevertheless, we leave a detailed complexity characterization for this fragment as future work. It will be interesting to complete the picture by also extending the study to conflict-minimality when considering the number of conflicts (instead of subset-minimality), and closing the gap for the case of ⊆ -minimal conflict-confining AR-hypotheses, which both remain open for now. Further, we previously also obtained complexity results for ABox abduction in the description logic DL-LiteDL -Lite [HaakKMT2026] . Preliminary work for combinations of properties in this setting shows that in some cases the complexity is again governed by the highest complexity among the individual properties, but there is a notable exception. It turns out that in case of DL-LiteDL -Lite, conflict-confining AR-hypotheses have a much simpler structure: Every conflict-confining AR-hypothesis contains a singleton AR-hypothesis, which is of course again conflict-confining. This often makes abduction problems easier when adding conflict-confinement in addition to some other property (or minimality condition) compared to the same problem without requiring conflict-confinement. It will be interesting to fully understand the complexity landscape for combinations of properties in this setting. It should be noted that in case of expressive DLs such as ℒALC and its extensions, the complexity of the considered abduction problems seems significantly less interesting. The reason is that for these DLs, entailment is often already ExpTime-complete. Consequently, the complexity of abduction tends to be dominated by the complexity of entailment. Beside considering different DLs, another important direction for the future is to consider other repair semantics. Most prominently, IAR semantics are currently missing from our study. While there has been previous work on abduction under IAR semantics, it was more practical in nature, obtaining an upper bound for one specific case in DL-LiteDL -Lite. The complexity landscape for different (combinations of) properties remains widely unexplored. References 5 Technical Appendix For constructions referenced in the main paper, we provide full proofs of the corresponding results here. The following example from our previous paper [HaakKMT2026] will be useful in some of our reductions (e.g., when translating Σ -restriction to conflict-confinement). Example 21. Let =⟨,⟩K= ,A , where =A⊓B⊑⊥,B⊓C⊑⊥,C⊓D⊑A, and =\\,A B ,B C ,C D A\,\, and =B(a),C(a), =\\,B(a),C(a)\,\, and let α=A(a)α=A(a). It is easy to see that α\α\ is a Brave-hypothesis for ⟨,α⟩ ,α , but results in a new conflict A(a),B(a)\A(a),B(a)\ of ⟨,∪α⟩ ,A∪\α\ . Hence, α\α\ is not conflict-confining in K. However, ℋ≔D(a)H \D(a)\ entails A(a)A(a) in the repair C(a),D(a)\C(a),D(a)\ and is consistent with all repairs of K. Intuitively, the only repair of ∪ℋA where α is entailed, is the one that already got rid of the conflict with α. 5.1 Constructions used for Theorem˜10 Theorem 22. The existence problem for conflict-confining Brave-hypotheses is Σ2 P_2-hard. Proof. We reduce from non-validity of ∀∃∀∃-QBFs to existence of conflict-confining Brave-hypotheses. Let Φ≔∀Y∃Z.φ ∀ Y∃ Z. , where φ is a CNF represented as a set of clauses, where clauses are sets of literals. Let X≔Y∪ZX Y∪ Z. We construct the KB =⟨,⟩K= ,A , using concept names N=Ax,Ax¯∣x∈X∪Vy∣y∈Y∪Ac∣c∈φ∪Aφ,Aφ¯,CN=\A_x,A_ x x∈ X\∪\V_y y∈ Y\∪\A_c c∈ \∪\A_ ,A_ ,C\. Intuitively, our encoding is based on a translation for the setting of Σ -restriction, but we use conflict-confinement to encode this restriction instead by using the idea from Example˜21. Precisely, we ensure that any hypothesis that uses symbols outside the intended signature Σ=Ay,Ay¯∣y∈Y∪m =\\,A_y,A_ y y∈ Y\,\∪\m\ introduces new conflicts, and is thus not conflict-confining. For this, we use additional concept names CdC_d and BdB_d. Formally, we define ≔ Cd⊓⨅y∈YVy⊓Aφ¯⊑C∪ \\,C_d _y∈ YV_y A_ C\,\∪ Cd⊓Ay⊑Vy,Cd⊓Ay¯⊑Vy∣y∈Y∪ \\,C_d A_y V_y,C_d A_ y V_y y∈ Y\,\∪ Ax⊓Ax¯⊑⊥∣x∈X∪ \\,A_x A_ x x∈ X\,\∪ Cd⊓Aℓ⊑Ac∣ℓ∈c,c∈φ∪ \\,C_d A_ A_c ∈ c,c∈ \,\∪ Cd⊓⨅y∈YVy⊓⨅c∈φAc⊑Aφ∪ \\,C_d _y∈ YV_y _c∈ A_c A_ \,\∪ Aφ⊓Aφ¯⊑⊥∪Aφ⊓Bd⊑⊥∪ \\,A_ A_ \,\∪\\,A_ B_d \,\∪ Cd⊓Bd⊑⊥∪C⊓Bd⊑⊥∪ \\,C_d B_d \,\∪\\,C B_d \,\∪ Ac⊓Bd⊑⊥∣c∈φ∪Vy⊓Bd⊑⊥ and \\,A_c B_d c∈ \,\∪\\,V_y B_d \,\ and ≔ Az(m),Az¯(m)∣z∈Z∪Aφ¯(m),Bd(m),Cd(m), \\,A_z(m),A_ z(m) z∈ Z\,\∪\A_ (m),B_d(m),C_d(m)\, where m is an individual. Finally, let ≔⟨,⟩K ,A and α≔C(m)α C(m). Axioms in each line of T encode the following intuition: (i) and (i) enforce a complete assignment over Y as a counter-example to the satisfaction of φ , (i) ensures a valid assignment over X, (iv) satisfaction of clauses via their literals, (v) satisfaction of φ , but not solely by a partial assignment over Z variables, and (vi) satisfaction of φ causes a new conflict. The remaining axioms use the idea from Example˜21 to implicitly enforce a Σ -restriction, disallowing certain assertions in any conflict-confining hypothesis. Now ⟨,α⟩ ,α is our desired abduction problem. It is a Brave-abduction problem: The KB K is inconsistent and as it contains no assertions of the form Aℓ(m)A_ (m) for any ℓ∈y,y¯ ∈\y, y\, we have ⊧̸C(m)K C(m). Claim 5. Φ is false iff ⟨,α⟩ ,α admits a non-trivial conflict-confining Brave-hypothesis. Proof of Claim. We first observe that the trivial hypothesis ℋt≔C(m)H_t \C(m)\ is not conflict-confining in K. This follows easily by considering the new conflict Bd(m),C(m)∈Conf(⟨,∪ℋt⟩)\B_d(m),C(m)\ ( ,A _t ). Therefore, we only prove the equivalence between satisfying assignments of Φ and conflict-confining Brave-hypothesis for α in K. Suppose Φ is false and let θY _Y (seen as a set of literals over Y) be an assignment over Y s.t. ∀Zφ[θY]∀ Z [ _Y] is false, where φ[θY] [ _Y] denotes the formula obtained from φ by applying the partial assignment θY _Y. Define ℋ≔Aℓ(m)∣ℓ∈θYH \\,A_ (m) ∈ _Y\,\. We now show that ℋH is a conflict-confining Brave-hypothesis for ⟨,α⟩ ,α by showing (i) ⟨,∪ℋ⟩⊧Braveα ,A _ Braveα and (i) ℋH is conflict-confining. For (i), let ℬ≔ℋ∪Cd(m),Aφ¯(m)B ∪\C_d(m),A_ (m)\. It is easy to see that ℬB is T-consistent, so there is a repair ℛ⊇ℬR of ⟨,∪ℋ⟩ ,A . Further, we have ⟨,ℬ⟩⊧C(m) ,B C(m) and therefore ⟨,ℛ⟩⊧C(m) ,R C(m). To see (i), we first observe that ℋH does not trigger any inconsistency due to an axiom of the form Ay⊓Ay¯⊑⊥A_y A_ y , as θY _Y is an assignment. Hence, ℋH is T-consistent. Next, we show that for any repair ℛ′R of K, the set ℛ′∪ℋR is T-consistent. Due to the axioms of the form Ax⊓Ax¯⊑⊥A_x A_ x , the set ℛ′∩Az(m),Az¯(m)∣z∈ZR ∩\\,A_z(m),A_ z(m) z∈ Z\,\ corresponds to a (potentially partial) assignment over Z. Since φ[θY] [ _Y] is false for all assignments over Z by assumption, we have ⟨,ℛ′∪ℋ⟩⊧̸Aφ ,R A_ by construction of T. This means that Aφ⊓Aφ¯⊑⊥A_ A_ does not trigger. The remaining disjointness axioms use the idea from Example˜21 to avoid conflicts in ⟨,ℛ′∪ℋ⟩ ,R : Due to the axiom Cd⊓Bd⊑⊥C_d B_d , we have Cd(m)∉ℛ′C_d(m) or Bd(m)∉ℛ′B_d(m) . In both cases, none of the remaining disjointness axioms can trigger, as either the assertion Bd(m)B_d(m) is missing (and not entailed) or no assertion of the form C(m)C(m), Aφ(m)A_ (m), Ac(m)A_c(m), or Vy(m)V_y(m) is entailed from ⟨,ℛ′∪ℋ⟩ ,R . Conversely, suppose that there is a conflict-confining Brave-hypothesis ℋH for ⟨,α⟩ ,α . We first argue that, w.l.o.g., ℋH only contains assertions of the form Ay(m)A_y(m) and Ay¯(m)A_ y(m). To this end, note that ℋH may only contain assertions over the individual m, since it is the only individual in ⟨,α⟩ ,α . Further, we can assume w.l.o.g. that ℋH only contains assertions using concept or role names occurring in K, as fresh concept and role names cannot help entailment of α in T. Additionally we can assume w.l.o.g. that it does not contain any assertions already present in A. Finally, we observe that all other assertions over the signature of ⟨,α⟩ ,α would introduce new conflicts, contradicting the assumption that ℋH is conflict-confining: The assertion C(m)C(m) would introduce the new conflict C(m),Bd(m)\C(m),B_d(m)\, while the assertion Aφ(m)A_ (m) would introduce the new conflict Aφ(m),Bd(m)\A_ (m),B_d(m)\. Any assertion Ac(m)A_c(m) for c∈φc∈ would introduce the new conflict Ac(m),Bd(m)\A_c(m),B_d(m)\, and any assertion Vy(m)V_y(m) for y∈Yy∈ Y would introduce the new conflict Vy(m),Bd(m)\V_y(m),B_d(m)\. Next, it is easy to see that ℋH contains exactly one of the assertions Ay(m)A_y(m) and Ay¯(m)A_ y(m) for each y∈Yy∈ Y: It contains at least one, since C(m)C(m) is entailed in some repair, and this is only possible when ⨅y∈YVy _y∈ YV_y is entailed in that repair. It contains at most one, since otherwise the axiom Ay⊓Ay¯⊑⊥A_y A_ y would lead to a new conflict. Consequently, ℋH corresponds to an assignment θY _Y over Y. Now consider an assignment θZ _Z over Z, represented as a set of literals. We now show that φ[θY∪θZ] [ _Y∪ _Z] is false. As this applies to all assignments over Z, it implies that ∀Y∃Zφ(Y,Z)∀ Y∃ Z (Y,Z) is false. Let Z≔Aℓ(m)∣ℓ∈θZ,A_Z \\,A_ (m) ∈ _Z\,\, i.e., the subset of A corresponding to assignment θZ _Z. The set ZA_Z is T-consistent, since θZ _Z is an assignment. As for all y∈Yy∈ Y we have ⟨,Z⟩⊧̸Vy(m) ,A_Z V_y(m), Z∪Aφ¯(m)A_Z∪\A_ (m)\ is T-consistent. Due to ℋH being conflict-confining, this implies that Z∪Aφ¯(m)∪ℋA_Z∪\A_ (m)\ is also T-consistent. Consequently, we have ⟨,Z∪ℋ⟩⊧̸Aφ(m) ,A_Z A_ (m), implying that φ[θY∪θZ] [ _Y∪ _Z] is false by construction of T. ∎ ∎ Theorem 23. The existence problem for non-trivial AR-hypotheses is Σ2 P_2-hard. We reduce from validity problem for ∃∀∃∀-QBFs. Let Ψ=∃Y∀Zψ =∃ Y∀ Z\;ψ be a ∃∀∃∀-QBF, where ψ is in DNF, and let X=Y∪ZX=Y∪ Z. We construct a TBox T using concept names N=Ax,Ax¯∣x∈X∪C,AψN=\A_x,A_ x x∈ X\∪\C,A_ψ\. Intuitively, T expresses that for any term t∈ψt∈ψ, the conjunction of concepts corresponding to the literals in t entails the concept AψA_ψ, which represents satisfaction of ψ. To this end, we define ≔⟨,⟩K ,A , where ≔ Ax⊓Ax¯⊑⊥∣x∈X∪ \\,A_x A_ x x∈ X\,\∪ C⊓⨅ℓ∈tAℓ⊑Aψ∣t∈ψ, \\,C _ ∈ tA_ A_ψ t∈ψ\, \, ≔ Az(m),Az¯(m)∣z∈Z, \\,A_z(m),A_ z(m) z∈ Z\, for an individual name m. Here, the first set of axioms ensures that repairs encode (potentially partial) assignments over X and the second encodes that ψ is satisfied iff at least one its terms is satisfied. Now, ⟨,Aψ(m)⟩ ,A_ψ(m) is the desired abduction problem. It is a valid abduction instance, as K is obviously inconsistent, and ⊧̸ARAψ(m)K _ ARA_ψ(m), as K does not contain the assertion C(m)C(m). Observe that ℋtriv≔Aψ(m)H_triv \A_ψ(m)\ is the trivial AR-hypothesis for ⟨,α⟩ ,α . However, we are considering existence of non-trivial hypotheses here, i.e., one that does not contain Aψ(m)A_ψ(m). See 1 Proof of Claim. (⇒ ) Let θY _Y be an assignment over Y, represented as a set of literals, witnessing that Ψ is true, i.e., f.a. assignments θZ _Z over Z, θY∪θZ⊧t _Y∪ _Z t for some t∈ψt∈ψ. Define ℋ≔C(m)∪Aℓ(m)∣ℓ∈θYH \C(m)\∪\\,A_ (m) ∈ _Y\,\. ℋH is indeed non-trivial. We next show that ℋH is in fact a conflict-confining AR-hypothesis for α in K. Consider any repair ℛR of ′≔⟨,∪ℋ⟩K ,A . Since θY _Y is an assignment, ℋH is T-consistent. Even more, no subset of ℋH is contained in any conflict of ′K and hence ℋH is conflict-confining in K. Moreover, we have ℋ⊆ℛH . Now let θZ≔ℓ∈Z∪Z¯∣Aℓ(m)∈ℛ _Z \\, ∈ Z∪ Z A_ (m) \,\. We argue that θZ _Z is a (full) assignment over Z. As ℛR is T-consistent, at most one of the assertions Ax(m)A_x(m) and Ax¯(m)A_ x(m) is in ℛR for each x∈Xx∈ X due to the first form of axioms in T. On the other hand, since ℛR is subset-maximal among the T-conistent subsets of ∪ℋA , it contains at least one of those to assertions for each x∈Xx∈ X. Hence, there is some term t∈ψt∈ψ s.t. t⊆θY∪θZt _Y∪ _Z by our assumption on θY _Y. Since ℋ⊆ℛH and by construction of T, this implies that ⟨,ℛ⟩⊧Aψ(m) ,R A_ψ(m). This proves that ′⊧ARAψ(m)K _ ARA_ψ(m), since the argument applies to all repairs ℛR of ′K . (⇐ ) Let ℋH be a non-trivial conflict-confining AR-hypothesis for ⟨,α⟩ ,α . We first argue that w.l.o.g., ℋH only contains assertions of the form Aℓ(m)A_ (m) and C(m)C(m): It can only contain assertions over individual m, as it may not use fresh individuals. W.l.o.g. it does not contain assertions using concept and role names not occuring in ⟨,α⟩ ,α or already present in A, as including these assertions in ℋH does not contribute to the entailment of Aψ(m)A_ψ(m). Finally, Aψ(m)∉ℋA_ψ(m) , as ℋH is non-trivial. It is now easy to see that C(m)∈ℋC(m) , as otherwise Aψ(m)A_ψ(m) could not be entailed. Further, ℋH contains at most one of the assertions Ay(m)A_y(m) and Ay¯(m)A_ y(m) for each y∈Yy∈ Y as ℋH is conflict-confining (containing both assertions for some y∈Yy∈ Y would create a new conflict due to Ay⊓Ay¯⊑⊥A_y A_ y ). Now, define the (potentially partial) assignment θY≔ℓ∣Aℓ(m)∈ℋ _Y \\, A_ (m) \,\ over Y. To finish the proof, we show that for each assignment θZ _Z over Z, we have θY∪θZ⊧ψ _Y∪ _Z ψ. Let ℛZ≔Aℓ(m)∣ℓ∈θY∪θZ∪C(m)R_Z \\,A_ (m) ∈ _Y∪ _Z\,\∪\C(m)\. As θY _Y and θZ _Z are assignments, it is easy to see that ℛZR_Z is a repair of ′K . Hence, we have ⟨,ℛZ⟩ ,R_Z by assumption. But this implies that ⟨,ℛZ⟩⊧Aψ(m) ,R_Z A_ψ(m) by assumption, and hence there is some term t∈ψt∈ψ, such that t⊆ℛZt _Z by construction of T. Consequently, θY∪θZ⊧ψ _Y∪ _Z ψ. Since θZ _Z is an arbitrary assignment over Z, we conclude that Ψ is true. ∎ 5.2 Constructions used for Theorem˜12 Theorem 24. Verification of conflict-confining Brave-hypotheses is DP-hard. Proof. We reduce from a combination of entailment and non-entailment under Brave semantics to verification of conflict-confining Brave-hypotheses. Given an instance ⟨,α1,α2⟩ , _1, _2 for some inconsistent KB K, the problem asks whether ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. This problem is DP-complete because the first question is NP-complete and the second question is coNP-complete under Brave semantics. For the reduction, assume w.l.o.g. that α1 _1 and α2 _2 are BIQs over the same individual, and let α1=A(a) _1=A(a), α2=B(a) _2=B(a), and =⟨,⟩K= ,A . We construct a KB ′K , an observation α, and a hypothesis ℋH next. Let ′≔⟨′,⟩K ,A with ′≔∪C⊓A⊑D,C⊓B⊑⊥,T ∪\C A D,C B \, α≔D(a)α D(a), and ℋ≔C(a)H \C(a)\ for fresh concepts C and D. The instance is a valid abduction problem, since ′K is inconsistent and ′⊧̸BraveαK _ Braveα. Intuitively, ℋH is a Brave-hypothesis for ⟨′,α⟩ ,α iff ⊧BraveA(a)K _ BraveA(a) and ℋH is conflict-confining for ′K iff ⊧̸BraveB(a)K _ BraveB(a). It remains to show correctness, which is stated in the following claim. See 2 Proof of Claim. Observe that ℋ≔C(a)H \C(a)\ is non-trivial indeed. Hence, we only prove the correctness of the claim regarding conflict-confinement. (⇒ ) Suppose ℋH is a conflict-confining Brave-hypothesis for ⟨′,D(a)⟩ ,D(a) . Notice that the only way to obtain the entailment ′⊧BraveD(a)K _ BraveD(a) is via the TBox axiom C⊓A⊑DC A D, since no axiom in K contains D. Therefore, we must have ⊧BraveA(a)K _ BraveA(a). Moreover, we have ⊧̸BraveB(a)K _ BraveB(a): Suppose to the contrary that ⊧BraveB(a)K _ BraveB(a) and let ℛR be a witnessing repair such that ⟨,ℛ⟩⊧B(a) ,R B(a). Then, we have that ⟨′,ℛ∪ℋ⟩⊧⊥ ,R , in particular due to the axiom C⊓B⊑⊥C B and the assertion C(a)C(a). Since ℛR is a repair, and hence T-consistent, there must be a conflict of ⟨′,ℛ∪ℋ⟩ ,R that is not a conflict of ⟨′,⟩ ,A . But this leads to a contradiction to our assumption that ℋH is conflict-confining for ′K . As a result, ′⊧̸BraveB(a)K _ BraveB(a) must be true. (⇐ ) Suppose ⊧BraveA(a)K _ BraveA(a) and ⊧̸BraveB(a)K _ BraveB(a). Then, ′⊧BraveA(a)K _ BraveA(a) and hence ⟨′,∪ℋ⟩⊧BraveD(a). ,A _ BraveD(a). Therefore ℋH is indeed a Brave-hypothesis for ⟨′,α⟩ ,α . To show that ℋH is conflict-confining for ′K , suppose to the contrary that there is a conflict ∈Conf(⟨′,∪ℋ⟩)C ( ,A ) such that ∉Conf(⟨′,⟩)C ( ,A ). In particular, this implies that C(a)∈C(a) since ℋ=C(a)H=\C(a)\. As a result, we have ∖C(a)⊆C \C(a)\ and C is ′T -consistent, and hence also T-consistent. But this implies that ⟨′,⟩⊧B(a) ,C B(a), since the only conflict involving C(a)C(a) is via the axiom C⊓B⊑⊥C B . Further, this means that ⟨,⟩⊧B(a) ,C B(a), as the new axioms in ′T do not help entailment of B(a)B(a). As C is T-consistent, there exists a repair ℛ⊇R of K, and we have ⟨,ℛ⟩⊧B(a) ,R B(a). Consequently, ⊧BraveB(a)K _ BraveB(a). But this is a contradiction to our assumption, so ℋH must be conflict-confining. ∎ ∎ Theorem 25. Verification of conflict-confining AR-hypotheses is coNP-hard. Proof. We reduce from AR-entailment. To achieve this, let =⟨,⟩K= ,A and A(a)A(a) be an instance of AR-entailment. Define ′≔⟨′,⟩K ,A , where ′≔∪X⊓A⊑C.T ∪\X A C\. Finally, let α≔C(a)α C(a) and ℋ≔X(a)H \X(a)\. We observe that ⊧ARA(a)K _ ARA(a) iff ⟨′,∪ℋ⟩⊧ARα ,A _ ARα. Note that ℋH is trivially conflict-confining as it uses a fresh concept name X that cannot participate in any conflict. We now turn to Brave semantics. For membership, observe that ℋH is a conflict-confining Brave-hypothesis iff (1) ⟨,∪ℋ⟩⊧Braveα ,A _ Braveα, and (2) Conf(⟨,∪ℋ⟩)=Conf(⟨,⟩)Conf( ,A )=Conf( ,A ). In the case of Brave-hypotheses, (1) is instance checking for ℰℒ⊥E\!L_ and hence in NP, while (2) can be checked in coNP by universally guessing a conflict C such that ∈Conf(⟨,∪ℋ⟩)C ( ,A ) and ∉Conf(⟨,⟩)C ( ,A ). The last check can be performed in polynomial time. Hence, the problem is contained in DP. For hardness, we reduce from a combination of entailment and non-entailment under Brave semantics to verification of conflict-confining Brave-hypotheses. Given an instance ⟨,α1,α2⟩ , _1, _2 for some inconsistent KB K, the problem asks whether ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. This problem is DP-complete because the first question is NP-complete and the second question is coNP-complete under Brave semantics. For the reduction, assume w.l.o.g. that α1 _1 and α2 _2 are BIQs over the same individual, and let α1=A(a) _1=A(a), α2=B(a) _2=B(a), and =⟨,⟩K= ,A . We construct a KB ′K , an observation α, and a hypothesis ℋH next. Let ′≔⟨′,⟩K ,A with ′≔∪C⊓A⊑D,C⊓B⊑⊥,T ∪\C A D,C B \, α≔D(a)α D(a), and ℋ≔C(a)H \C(a)\ for fresh concepts C and D. The instance is a valid abduction problem, since ′K is inconsistent and ′⊧̸BraveαK _ Braveα. Intuitively, ℋH is a Brave-hypothesis for ⟨′,α⟩ ,α iff ⊧BraveA(a)K _ BraveA(a) and ℋH is conflict-confining for ′K iff ⊧̸BraveB(a)K _ BraveB(a). It remains to show correctness, which is stated in the following claim. Claim 6. ℋH is a conflict-confining Brave-hypothesis for α in ′K iff ⊧Braveα1K _ Brave _1 and ⊧̸Braveα2K _ Brave _2. Proof of Claim. (⇒ ) Suppose ℋH is a conflict-confining Brave-hypothesis for ⟨′,D(a)⟩ ,D(a) . Notice that the only way to obtain the entailment ′⊧BraveD(a)K _ BraveD(a) is via the TBox axiom C⊓A⊑DC A D, since no axiom in K contains D. Therefore, we must have ⊧BraveA(a)K _ BraveA(a). Moreover, we have ⊧̸BraveB(a)K _ BraveB(a): Suppose to the contrary that ⊧BraveB(a)K _ BraveB(a) and let ℛR be a witnessing repair such that ⟨,ℛ⟩⊧B(a) ,R B(a). Then, we have that ⟨′,ℛ∪ℋ⟩⊧⊥ ,R , in particular due to the axiom C⊓B⊑⊥C B and the assertion C(a)C(a). Since ℛR is a repair, and hence T-consistent, there must be a conflict of ⟨′,ℛ∪ℋ⟩ ,R that is not a conflict of ⟨′,⟩ ,A . But this leads to a contradiction to our assumption that ℋH is conflict-confining for ′K . As a result, ′⊧̸BraveB(a)K _ BraveB(a) must be true. (⇐ ) Suppose ⊧BraveA(a)K _ BraveA(a) and ⊧̸BraveB(a)K _ BraveB(a). Then, ′⊧BraveA(a)K _ BraveA(a) and hence ⟨′,∪ℋ⟩⊧BraveD(a). ,A _ BraveD(a). Therefore ℋH is indeed a Brave-hypothesis for ⟨′,α⟩ ,α . To show that ℋH is conflict-confining for ′K , suppose to the contrary that there is a conflict ∈Conf(⟨′,∪ℋ⟩)C ( ,A ) such that ∉Conf(⟨′,⟩)C ( ,A ). In particular, this implies that C(a)∈C(a) since ℋ=C(a)H=\C(a)\. As a result, we have ∖C(a)⊆C \C(a)\ and C is ′T -consistent, and hence also T-consistent. But this implies that ⟨′,⟩⊧B(a) ,C B(a), since the only conflict involving C(a)C(a) is via the axiom C⊓B⊑⊥C B . Further, this means that ⟨,⟩⊧B(a) ,C B(a), as the new axioms in ′T do not help entailment of B(a)B(a). As C is T-consistent, there exists a repair ℛ⊇R of K, and we have ⟨,ℛ⟩⊧B(a) ,R B(a). Consequently, ⊧BraveB(a)K _ BraveB(a). But this is a contradiction to our assumption, so ℋH must be conflict-confining. ∎ We conclude by observing that the above reduction can be achieved in polynomial time. ∎ 5.3 Proof Details and Constructions Used for Theorem˜14 See 3 Proof of Claim. (⇒ ) Suppose ℋH is a ⊆ -minimal hypothesis for Q(a)Q(a) in ′K . Observe that the only way to obtain the entailment ′⊧BraveQ(a)K _ BraveQ(a) is via the TBox axiom C⊓D⊓A⊑QC D A Q, since no axiom in K contains Q and Q(a)∉ℋQ(a) . Therefore, ⊧BraveA(a)K _ BraveA(a), since otherwise ′⊧̸BraveA(a)K _ BraveA(a), which would imply ′⊧̸BraveQ(a)K _ BraveQ(a). Moreover, we have ⊧̸BraveB(a)K _ BraveB(a): Suppose to the contrary that ⊧BraveB(a)K _ BraveB(a). Then ′⊧C(a)K C(a) due to the axiom B⊑CB C. Consequently, D(a)\D(a)\ is a Brave-hypothesis for α in ′K , which is a contradiction to ⊆ -minimality of ℋH. (⇐ ) Suppose ⊧BraveA(a)K _ BraveA(a) and ⊧̸BraveB(a)K _ BraveB(a). Then, we also have ′⊧BraveA(a)K _ BraveA(a) and hence ⟨′,∪ℋ⟩⊧BraveQ(a), ,A _ BraveQ(a), so ℋH is a Brave-hypothesis for ⟨′,α⟩ ,α . For ⊆ -minimality, suppose to the contrary that there is a Brave-hypothesis ℋ′⊊ℋH for ⟨′,α⟩ ,α . Since D(a)D(a) cannot be entailed via any axiom in ′K , we have ℋ′=D(a)H =\D(a)\. However, this implies that ′⊧BraveC(a)K _ BraveC(a), which can only be true if ′⊧BraveB(a)K _ BraveB(a). But then ⊧BraveB(a)K _ BraveB(a), which is a contradiction. ∎ The following example shows that the set of AR-hypotheses for a given AR-abduction problem does not need to be convex. This underlies the hardness proof for verification of ⊆ -minimal AR-hypotheses presented after. Example 26. Define ≔B1⊓B2⊑⊥,C1⊓C2⊑⊥,B1⊑A,B3⊑A, \B_1 B_2 , C_1 C_2 , B_1 A, B_3 A\, ≔C1(a),C2(a), \C_1(a),C_2(a)\, ℬ1 _1 ≔B1(a),ℬ2≔ℬ1∪B2(a),ℬ3≔ℬ2∪B3(a). \B_1(a)\, _2 _1∪\B_2(a)\, _3 _2∪\B_3(a)\. and let ≔⟨,⟩K ,A . We have ℬ1⊆ℬ2⊆ℬ3B_1 _2 _3, and ℬ1B_1 and ℬ3B_3 are AR-hypotheses for ⟨,A(a)⟩ ,A(a) , while ℬ2B_2 is not. Theorem 27. Verification of ⊆ -minimal AR-hypotheses is Π2 P_2-hard. Proof. We reduce from checking whether a given Π2 _2-QBF is true. Let Φ=∀X∃Yφ(X,Y) =∀ X∃ Y (X,Y) be a Π2 _2-QBF, where X=x1,…,xnX=\x_1,…,x_n\ and Y=y1,…,ymY=\y_1,…,y_m\. Note that we can assume w.l.o.g. that ¬φ is in DNF with set of terms c1,…,ck\c_1,…,c_k\. We construct an AR-abduction problem ⟨,A(a)⟩ ,A(a) and AR-hypothesis ℋH for it s.t. ∀X∃Yφ∀ X∃ Y is true iff ℋH is a ⊆ -minimal AR-hypothesis. Equivalently, ∃X∀Y¬φ∃ X∀ Y is true iff there is some subset ℋ′⊊ℋH s.t. ℋ′H is an AR-hypothesis for ⟨,A(a)⟩ ,A(a) . The proof idea is as follows. We construct K and ℋH in such a way that that subsets ℋ′⊊ℋH encode assignments over X, and repairs of ⟨,∪ℋ′⟩ ,A range over encodings of all assignments over Y. Entailment of A(a)A(a) in ⟨,∪ℋ′⟩ ,A is then equivalent to the corresponding assignment over X∪YX∪ Y satisfying φ . Further, we use the idea from Example˜26: To ensure entailment of A(a)A(a) in ⟨,∪ℋ⟩ ,A , we use an additional axiom in T that circumvents the construction encoding Φ , but cannot be triggered in ⟨,∪ℋ′⟩ ,A for any subset ℋ′⊊ℋH . Another important component of the construction will be two disjoint concepts B1B_1 and B2B_2 that allow us to split the set of repairs in two parts: The repairs containing the assertion B1(a)B_1(a) will ensure that φ is satisfied for all assignments over Y, while the repairs containing the assertion B2(a)B_2(a) will ensure that ℋH contains a full assignment over X. We now provide the definition of K, argue that ⟨,A(a)⟩ ,A(a) is an AR-abduction problem, and define the ABox ℋH. We then provide further intuition on the components of the construction, followed by the proof of correctness. Define =⟨,⟩K= ,A , where ≔0∪1∪2T _0 _1 _2, and 0T_0, 1T_1, 2T_2 and A are defined as follows: 0≔B1⊓B2⊑⊥,B1′⊓B2⊑⊥,T_0 \\,B_1 B_2 , B_1 B_2 \,\, 1≔ _1 B1⊓⨅1≤i≤n(Tx,i⊓Fx,i)⊑A∪ \B_1 _1≤ i≤ n(T_x,i F_x,i) A \∪ B1⊓Cj⊑A∣1≤j≤k∪ \\,B_1 C_j A 1≤ j≤ k\,\∪ B1′⊓Ty,i⊓Fy,i⊑⊥∣1≤i≤m∪ \\,B_1 T_y,i F_y,i 1≤ i≤ m\,\∪ B1′⊓Tx,i⊓Cj⊑⊥∣¬xi∈cj∪ \\,B_1 T_x,i C_j x_i∈ c_j\,\∪ B1′⊓Fx,i⊓Cj⊑⊥∣xi∈cj∪ \\,B_1 F_x,i C_j x_i∈ c_j\,\∪ B1′⊓Ty,i⊓Cj⊑⊥∣¬yi∈cj∪ \\,B_1 T_y,i C_j y_i∈ c_j\,\∪ B1′⊓Fy,i⊓Cj⊑⊥∣yi∈cj \\,B_1 F_y,i C_j y_i∈ c_j\,\ 2≔ _2 B2⊓⨅1≤i≤nHAVEi⊑A∪ \B_2 _1≤ i≤ nHAVE_i A \∪ Tx,i⊑HAVEi,Fx,i⊑HAVEi∣1≤i≤n \\,T_x,i _i,\;F_x,i _i 1≤ i≤ n\,\ ≔ B1(a),B1′(a),B2(a)∪ \B_1(a),B_1 (a),B_2(a)\∪ Ty,i(a),Fy,i(a)∣1≤i≤m∪ \\,T_y,i(a),F_y,i(a) 1≤ i≤ m\,\∪ Cj(a)∣1≤j≤k. \\,C_j(a) 1≤ j≤ k\,\. First, note that ⟨,A(a)⟩ ,A(a) is an AR-abduction problem: the KB K is inconsistent, for example it has the conflict B1(a),B2(a)\B_1(a),B_2(a)\. Also, ⊧̸ARA(a)K _ ARA(a) as there is a repair ℛR of K with B2(a)∈ℛB_2(a) . By the axioms in 0T_0, we have B1(a)∉ℛB_1(a) , so A(a)A(a) cannot be entailed by the aximos in 1T_1. But there is also no assertion of the form Tx,i(a)T_x,i(a) or Fx,i(a)F_x,i(a) in ℛR, as these are not contained in A. Hence, A(a)A(a) cannot be entailed by the first axiom in 2T_2, so ⟨,ℛ⟩⊧̸A(a) ,R A(a). Now, define the AR-hypothesis ℋH for ⟨,A(a)⟩ ,A(a) by ℋ≔Tx,i(a),Fx,i(a)∣1≤i≤n. \\,T_x,i(a),F_x,i(a) 1≤ i≤ n\,\. We now provide some intuition on the construction of K and ℋH. The axioms in 0T_0 split the set of repairs into two parts: Those repairs that contain B1(a)B_1(a) and potentially B1′(a)B_1 (a), and those repairs that contain B2(a)B_2(a). The axioms in 1T_1 only affect the former repairs while those in 2T_2 only affect the latter. Regarding the encoding of φ in the construction, presence of an assertion of the form Tz,i(a)T_z,i(a) or Fz,i(a)F_z,i(a) encodes that variable z is assigned to true or false, resp. Accordingly, repairs containing B1(a)B_1(a) encode assignments over Y, due to the axioms of the form B1′⊓Ty,i⊓Fy,i⊑⊥B_1 T_y,i F_y,i , while similarly subsets of ℋH encode assignments over Z. (W.l.o.g., one can assume that ℋH contains at most one of the assertions Ty,iT_y,i and Fy,iF_y,i for each i, due to how satisfaction of φ is encoded.) Further, the assertions of the form Cj(a)C_j(a) correspond to the terms cjc_j of φ . Based on these ideas, 1T_1 ensures that for a given subset ℋ′⊊ℋH , A(a)A(a) is entailed in all repairs containing B1(a)B_1(a), iff the assignment θℋ′ _H corresponding to ℋ′H satisfies the formula ∀Zφ∀ Z : The last 44 kinds of axioms in 1T_1 ensure that Cj(a)C_j(a) conflicts with assignments that falsify cjc_j, so some Cj(a)C_j(a) only remains in all repairs (yielding entailment of A(a)A(a)), if at least one term of φ[θℋ′] [ _H ] is satisfied by each assignment over Z. This construction is circumvented for the full set ℋH: Here, entailment of A(a)A(a) is ensured via the first axiom in 1T_1. On the other hand, 2T_2 ensures that each AR-hypothesis ℋ′⊊ℋH of ⟨,A(a)⟩ ,A(a) contains at least one of the assertions Ty,i(a)T_y,i(a), Fy,i(a)F_y,i(a) (using the repairs containing B2(a)B_2(a)). The full proof of correctness is now split into three parts, namely the proof that ℋH is an AR-hypothesis for ⟨,A(a)⟩ ,A(a) and the two directions of the equivalence that there is an AR-hypothesis ℋ′⊊ℋH of ⟨,A(a)⟩ ,A(a) iff Φ is false, shown in Claims 7, 8 and 9. Claim 7. ℋH is an AR-hypothesis for ⟨,A(a)⟩ ,A(a) . Proof of Claim. Consider any repair ℛR of ⟨,∪ℋ⟩ ,A . We consider two cases. Case “B1(a)∈ℛB_1(a) ”. By the axioms in 0T_0, we have B2(a)∉ℛB_2(a) , so A(a)A(a) cannot be entailed by the first axiom in 2T_2. If we have Cj(a)∈ℛC_j(a) for some j, A(a)A(a) is entailed by the axiom B1⊓Cj⊑AB_1 C_j A. Otherwise, the only remaining disjointness axioms that could trigger are those of the form B1′⊓Ty,i⊓Fy,i⊑⊥B_1 T_y,i F_y,i , which do not affect the concepts of the form Tx,iT_x,i or Fx,iF_x,i. Hence, by maximality of repairs, we have Tx,i(a),Fx,i(a)∈ℛT_x,i(a),F_x,i(a) f.a. 1≤i≤n1≤ i≤ n. Consequently, A(a)A(a) is entailed by the first axiom in 1T_1. Case “B1(a)∉ℛB_1(a) ”. First note that B1′(a)∉ℛB_1 (a) : Otherwise, we would have B2(a)∉ℛB_2(a) by the axioms in 0T_0. But then, B1(a)∈ℛB_1(a) by maximality of repairs, as B1B_1 does not occur in any disjointness axioms in 1T_1 or 2T_2. As B1′(a)∉ℛB_1 (a) , none of the disjointness axioms in 1T_1 can trigger, so we only need to consider those in 2T_2. Hence, we have B2(a),Tx,i(a),Fx,i(a)∈ℛB_2(a),T_x,i(a),F_x,i(a) for all 1≤i≤n1≤ i≤ n by maximality of repairs. Consequently, A(a)A(a) is entailed via the axioms of the form Tx,i⊑HAVEi(a)T_x,i _i(a) and Fx,i⊑HAVEi(a)F_x,i _i(a) as well as the axiom B2⊓⨅1≤i≤nHAVEi⊑AB_2 _1≤ i≤ nHAVE_i A. ∎ Claim 8. If ∀X∃Yφ(X,Y)∀ X∃ Y (X,Y) is false, then there is a subset ℋ′⊊ℋH s.t. ℋ′H is an AR-hypothesis for ⟨,A(a)⟩ ,A(a) . Proof of Claim. In this case, there is an assignment sXs_X over X s.t.f.a. assignments sYs_Y over Y, there is conjunction term cjc_j in ¬φ with sX∪sY⊧cj.s_X∪ s_Y c_j. Define ℋ′=Tx,i(a)∣sX(xi)=1∪Fx,i(a)∣sX(xi)=0.H =\\,T_x,i(a) s_X(x_i)=1\,\∪\\,F_x,i(a) s_X(x_i)=0\,\. Consider any repair ℛR of ⟨,∪ℋ′⟩ ,A . Similar to the above proof of claim, we distinguish two cases based on whether B1(a)∈ℛB_1(a) . Case “B1(a)∈ℛB_1(a) ”. By the axioms in 0T_0, we have B2(a)∉ℛB_2(a) , so A(a)A(a) cannot be entailed by the first axiom in 2T_2. If we have B1′(a)∉ℛB_1 (a) , then none of the disjointness axioms in 1T_1 can trigger, so there is some Cj(a)∈ℛC_j(a) by maximality of repairs and we get the entailment of A(a)A(a) via the axiom B1⊓Cj⊑AB_1 C_j A. Otherwise, the disjointness axioms of the form B1′⊓Ty,i⊓Fy,iB_1 T_y,i F_y,i ensure that ℛR contains at most one of the assertions Ty,i(a)T_y,i(a) and Fy,i(a)F_y,i(a) for each 1≤i≤m1≤ i≤ m. Hence, the present assertions in ℛR correspond to the assignment sℛs_R over Y defined by sℛ(yi)≔1,if Ty,i(a)∈ℛ0,if Fy,i(a)∈ℛ.s_R(y_i) cases1,&if T_y,i(a) \\ 0,&if F_y,i(a) . cases By our assumption, there is some cjc_j s.t. sX∪sℛ⊧cjs_X∪ s_R c_j. By construction of 1T_1, this means that Cj(a)C_j(a) is not in conflict with any of the assertions in ℋ′H or any of the assertions Ty,i(a)T_y,i(a) or Fy,i(a)F_y,i(a) remaining in ℛR. Hence, A(a)A(a) is entailed by the axiom B1⊓Cj⊑AB_1 C_j A. Case “B1(a)∉ℛB_1(a) ”. First note that B1′(a)∉ℛB_1 (a) by the same argument as in the previous proof of claim. As B1′(a)∉ℛB_1 (a) , none of the disjointness axioms in 1T_1 can trigger. Hence, we have B2(a)∈ℛB_2(a) by maximality of repairs. Further, by maximality of repairs and the fact that sXs_X is an assignment over X, we have Tx,i(a)∈ℛT_x,i(a) or Fx,i(a)∈ℛF_x,i(a) for each 1≤i≤n1≤ i≤ n. Consequently, A(a)A(a) is entailed via the axioms of the form Tx,i⊑HAVEiT_x,i _i and Fx,i⊑HAVEiF_x,i _i as well as the axiom B2⊓⨅1≤i≤nHAVEi⊑AB_2 _1≤ i≤ nHAVE_i A. ∎ Claim 9. If there is a subset ℋ′⊊ℋH s.t. ℋ′H is an AR-hypothesis for ⟨,A(a)⟩ ,A(a) , then ∀X∃Yφ(X,Y)∀ X∃ Y (X,Y) is false. Proof of Claim. By assumption we have ⟨,∪ℋ′⟩⊧ARA(a) ,A _ ARA(a). First, note that ℋ′∪B2(a)H ∪\B_2(a)\ is T-consistent. Hence, there is a repair ℛR of ⟨,∪ℋ′⟩ ,A with ℋ′∪B2(a)⊆ℛH ∪\B_2(a)\ . By the axioms in 0T_0, we have B1(a)∉ℛB_1(a) . Hence, A(a)A(a) cannot be entailed using axioms in 1T_1, so it must be entailed by the axiom B2⊓⨅1≤i≤nHAVEi⊑AB_2 _1≤ i≤ nHAVE_i A. This means that we have Tx,i(a)∈ℛT_x,i(a) or Fx,i(a)∈ℛF_x,i(a) for each 1≤i≤n1≤ i≤ n. As these assertions do not occur in A, they must be contained in ℋ′H . Define the assignment sℋ′s_H over X by sℋ′(xi)≔1,if Tx,i(a)∈ℋ′0,otherwises_H (x_i) cases1,&if T_x,i(a) \\ 0,&otherwise cases and consider any assignment sYs_Y over Y. As sYs_Y is a function, the set sY≔ _s_Y B1(a),B1′(a)∪ℋ′∪ \B_1(a),B_1 (a)\ ∪ Ty,i(a)∣sY(yi)=1∪Fy,i(a)∣sY(yi)=0 \\,T_y,i(a) s_Y(y_i)=1\,\∪\\,F_y,i(a) s_Y(y_i)=0\,\ is T-consistent, so there are repairs containing all assertions in sYA_s_Y. In these repairs, A(a)A(a) cannot be entailed by the axioms in 2T_2, since B2(a)B_2(a) is in conflict with B1(a)B_1(a). Further, it cannot be entailed by the first axiom in 1T_1, as ℋ′⊊ℋH . Hence, there is some index j s.t. Cj(a)C_j(a) is not in conflict with any of the assertions in sYA_s_Y. (Otherwise, there is a repair ℛR among these that does not contain any of the assertions of the form Cj(a)C_j(a), meaning that ⟨,ℛ⟩⊧̸A(a) ,R A(a).) In particular, this is also true for the subset sY′⊆sYA_s_Y _s_Y defined by sY′≔sY∖Fx,i(a)∣1≤i≤n,Tx,i(a)∈sY′.A_s_Y _s_Y \\,F_x,i(a) 1≤ i≤ n,T_x,i(a) _s_Y \,\. But the assertions of the forms Tx,i(a)T_x,i(a), Fx,i(a)F_x,i(a), Ty,i(a)T_y,i(a) and Fy,i(a)F_y,i(a) present in sY′A_s_Y correspond to the assignment sℋ′∪sYs_H ∪ s_Y, so this means that cjc_j is not falsified by sℋ′∪sYs_H ∪ s_Y by construction of 1T_1. Consequently, sℋ′∪sY⊧¬φs_H ∪ s_Y . As sYs_Y was picked arbitrarily, this means that ∃X∀Y¬φ(X,Y)∃ X∀ Y (X,Y) is true and ∀X∃Yφ(X,Y)∀ X∃ Y (X,Y) is false. ∎ Combined, the three above claims show that ∀X∃Yφ(X,Y)∀ X∃ Y (X,Y) is true iff ℋH is a ⊆ -minimal AR-hypothesis for ⟨,A(a)⟩ ,A(a) , finishing the hardness proof. ∎ 5.4 Proof details for Theorem˜15 To see that ˜3 still applies when we replace non-triviality by conflict-confinement, observe that ℋ≔C(a),D(a)H \C(a),D(a)\ is indeed conflict-confining since no axiom in ′T causes a new conflict involving either of the two (or both) assertions. 5.5 Proof details for Theorem˜17 (Π2 P_2-hardness for Brave semantics) We reuse the translation from ∀∃∀∃-QBFs as in Section˜5.1 and define ≔⟨,⟩K ,A , where: ≔ Cd⊓⨅y∈YVy⊓Aφ¯⊑C∪ \\,C_d _y∈ YV_y A_ C\,\∪ Cd⊓Ay⊑Vy,Cd⊓Ay¯⊑Vy∣y∈Y∪ \\,C_d A_y V_y,C_d A_ y V_y y∈ Y\,\∪ Ax⊓Ax¯⊑⊥∣x∈X∪ \\,A_x A_ x x∈ X\,\∪ Cd⊓Aℓ⊑Ac∣ℓ∈c,c∈φ∪ \\,C_d A_ A_c ∈ c,c∈ \,\∪ Cd⊓⨅y∈YVy⊓⨅c∈φAc⊑Aφ∪ \\,C_d _y∈ YV_y _c∈ A_c A_ \,\∪ Aφ⊓Aφ¯⊑⊥∪Aφ⊓Bd⊑⊥∪ \\,A_ A_ \,\∪\\,A_ B_d \,\∪ Cd⊓Bd⊑⊥∪C⊓Bd⊑⊥∪ \\,C_d B_d \,\∪\\,C B_d \,\∪ Ac⊓Bd⊑⊥∣c∈φ∪Vy⊓Bd⊑⊥ and \\,A_c B_d c∈ \,\∪\\,V_y B_d \,\ and ≔ Az(m),Az¯(m)∣z∈Z∪Aφ¯(m),Bd(m),Cd(m), \\,A_z(m),A_ z(m) z∈ Z\,\∪\A_ (m),B_d(m),C_d(m)\, Let N=|Y|N=|Y|. We now introduce fresh concept names Xi∣i≤N+1\X_i i≤ N+1\ and add additional axioms to obtain a new KB ′≔⟨′,⟩K ,A with ′≔∪Cd⊓⨅1≤i≤N+1Xi⊑CT ∪\C_d _1≤ i≤ N+1X_i C\. Finally, let α≔C(m)α C(m) as before and take ℋ≔Xi(m)∣i≤N+1H \X_i(m) i≤ N+1\. For correctness, we observe that ℋH is a conflict-confining Brave-hypothesis for C(m)C(m) of size N+1N+1, whereas any conflict-confining Brave-hypothesis for ⟨,α⟩ ,α has size ≤N≤ N without loss of generality (since N=|Y|N=|Y|. This implies the following equivalences: ℋH is not a ≤-minimal conflict-confining Brave-hypothesis for ⟨′,C(m)⟩ ,C(m) iff there is a conflict-confining Brave-hypothesis for ⟨′,α⟩ ,α of size ≤N≤ N iff there is a conflict-confining Brave-hypothesis for ⟨,α⟩ ,α . Claim 10. Φ is false iff ℋH is not a ≤-minimal conflict-confining Brave-hypothesis for ⟨′,α⟩ ,α . Proof of Claim. The claim follows by observing that Φ is false iff ⟨,α⟩ ,α admits a conflict-confining Brave-hypothesis (˜5) iff ⟨′,α⟩ ,α admits a conflict-confining Brave-hypothesis iff ℋH is not a conflict-confining cardinality-minimal Brave hypothesis for ⟨′,α⟩ ,α . Observe that XiX_i for i≤N+1i≤ N+1 are fresh names not in K, hence ℋH is conflict-confining. In other words, ℋH alone can not trigger any conflict in ′K . Moreover, even though entailing C(m)C(m) in ′K triggers a conflict due to C⊓Bd⊑⊥C B_d , this is not a new conflict as Cd(m),Bd(m)\C_d(m),B_d(m)\ is already a conflict in K (and hence also in ′K ). ∎ 5.6 Proof details for Theorem˜19 Theorem 28. Verification of ⊆c _c-minimal non-trivial Brave-hypotheses is Π2 P_2-hard. Proof. We reuse the construction from the hardness proof in Section˜5.1. Let Φ be a ∀∃∀∃-QBF, and =⟨,⟩K= ,A be the KB obtained Φ using that construction. We add new axioms and assertions to K to obtain the KB ′≔⟨,′⟩K ,A as follows: ′ ≔∪Cd⊓X⊑C,X⊓Y⊑⊥, and ∪\C_d X C,X Y \, and ′ ≔∪Y(m) ∪\Y(m)\ Then, we let α≔C(m)α C(m) as before and take ℋ≔X(m)H \X(m)\. Here, ℋH induces exactly one more conflict in ′K , namely X(m),Y(m)\X(m),Y(m)\. For correctness, it is easy to see that there is a conflict-confining Brave-hypothesis for ⟨,C(m)⟩ ,C(m) iff there is such a hypothesis for ⟨′,C(m)⟩ ,C(m) . Furthermore, the letter is equivalent to ℋH not being a ⊆c _c-minimal hypothesis for ⟨′,C(m)⟩ ,C(m) , sincce existence ℋH introduces exactly one new conflict for ′K , while a conflict-confining Brave-hypothesis introduces no new conflicts. Thus the correctness follows due to the proof of Claim 5. This yields the mentioned Π2 P_2-hardness. ∎