Signature-Based Abduction with Fresh Individuals and Complex Concepts for Description Logics

1 Introduction

Description logics (DLs) are a powerful formalism to describe knowledge bases (KBs) containing both general domain knowledge from a DL ontology and a set of facts (the ABox). Using a DL reasoner, we can then infer information that is implicit in the data, and can be logically deduced based on the ontology [Baader et al., 2017]. Sometimes it is useful to not only reason about what logically follows from a DL KB, but to reason also about what does not follow. In abduction, we are given a KB as background knowledge, in combination with a set of facts (the observation) that cannot be deduced from the background knowledge. We are then looking for the missing piece in the background knowledge (the hypothesis) that is needed to make the observation logically entailed [Elsenbroich et al., 2006]. This form of reasoning has many applications: 1) it can be used to explain why something cannot be deduced [Calvanese et al., 2013], 2) it can be used for diagnosis tasks, giving the hypothesis as possible explanation for an unexpected observation [Obeid et al., 2019], and 3) it can be used in KB repair to give hints on how to fix missing entailments [Wei-Kleiner et al., 2014].

As a simplified application example from the geology domain, assume we have observed that in an area near a canal, holes appeared in the street as a result of subsidence due to an unstable ground. A possible explanation could involve the presence of a formation of so-called evaporite below the street, which dissolves when in contact with water [Fidelibus et al., 2011]. Our background knowledge consists of a geology ontology together with data about the area. Among others, it contains the following abbreviated axioms:

1. EvaFor ⊓ ∃bord.(Wat ⊓ ¬∃lin.WatPro) ⊑ ∃aff.Dis
2. EvaFor ⊓ ∃aff.Dis ⊑ ∀abov.Unst
3. (Wat ⊔ Str) ⊓EvaFo ⊑ ⊥ 4. Wat(can) 5. Str(str)

which state that 1. an Evaporite Formation which borders to a Waterway without Water-Proof lining will be affected by Dissolution; 2. All ground above an evaporite formation affected by dissolution is Unstable; 3. waterways and Streets are not evaporite formations; 4. can is a waterway; 5. str is a street. Our observation would be that the street is unstable: Unst(a1), and a hypothesis based on our background knowledge would be

stating that there is an evaporite formation e below the street that borders with the canal, and that the canal has no lining. A team of geologists can then verify the hypothesis by analysing the canal and the ground below the street. We highlight two aspects of this hypothesis: 1) it refers to a previously unknown individual, the evaporite formation, and 2) it uses a complex (composed) DL concept (∀lin.⊥). We are interested in hypotheses like this for signature based abduction, where we are additionally given a signature Σ of abducibles-a vocabulary of names to be used within the hypothesis [Koopmann et al., 2020]. The aim of Σ is to restrict to hypotheses that have explanatory character. In the present example, we would exclude aff and Dis from Σ, as the dissolution alone would be a too shallow explanation, and Wat, because we already know the waterways in the area. Furthermore, we are looking at ABox abduction, in which observations and hypotheses are ABoxes, in contrast to TBox abduction [Du et al., 2017; Wei-Kleiner et al., 2014], KB abduction [Koopmann et al., 2020; Elsenbroich et al., 2006] or concept abduction [Bienvenu, 2008].

While there are practical approaches to ABox abduction without signature-restriction [Klarman et al., 2011; Halland and Britz, 2012; Pukancov´a and Homola, 2017], works on signature-based ABox abduction often restrict hypotheses to flat ABoxes with a given set of individuals [Ceylan et al., 2020; Du et al., 2012]-which essentially means that statements in a hypothesis can be picked from a finite set-or they restrict to rewritable DLs which have limited expressivity [Du et al., 2014; Calvanese et al., 2013]. As with DLs, we usually have the open-world semantics, in which not all individuals are known, and DLs offer much more expressivity, it is a natural next step to look also at abduction allowing for fresh individuals and complex concepts in the result. This changes the nature of the abduction problem drastically as there is now an unbounded set of axioms that may occur in a hypothesis. Problems such as "Does axiom α belong to some/every/an optimal solution?" [Calvanese et al., 2013; Ceylan et al., 2020] become less helpful while new questions become interesting, such as whether we can give bounds on the number of individuals in a hypothesis, or on the overall size of the hypothesis.

Without understanding the theoretical properties yet, practical methods for signature-based abduction that admit expressive DL concepts in the hypothesis are presented in [Koopmann et al., 2020; Del-Pinto and Schmidt, 2019]. The authors there consider hypotheses that we would call complete in the sense that they cover all hypotheses at the same time. To make this possible, solutions are represented in a very expressive DL using non-classical operators such as fixpoints and axiom disjunction. In this setting, ABox abduction can be reduced to uniform interpolation, which however may produce solutions that are triple exponentially large [Zhao and Schmidt, 2017; Lutz and Wolter, 2011]. A natural question is whether this blow-up is really necessary, or whether we can obtain smaller or simpler hypotheses if we drop the requirement of completeness and look for hypotheses in a classical DL that is sufficient to entail the observation.

Unfortunately, our results indicate that this is not the case: if we only allow for fresh individuals but not for complex concepts, hypotheses may require exponentially many assertions for DLs between EL⊥ and ALCI, while for ALCF there does not even exist a general bound. If in addition, we allow for complex concepts, we are able to explain more observations, but the explanations may become triple exponentially large in comparison to the input. Motivated by this, we also consider a variant of the abduction problem in which we are additionally given a bound on the size of the hypothesis. To summarize, our contributions are the following.

1. we investigate signature-based ABox abduction for DLs ranging from EL to ALCQI where hypotheses may use fresh individuals, complex concepts or both,
2. we give tight bounds on the size of hypotheses if they exist,
3. we analyse the computational complexity of deciding whether a hypothesis exists, and
4. we analyse the complexity of deciding whether a hypothesis of bounded size exists.

Proof details are provided in the technical report [Koopmann, 2021].

2 Description Logics and ABox Abduction

We recall the DLs relevant to this paper [Baader et al., 2017] and provide the formal definition of the abduction problem we consider in this paper.

Let NC, NR and NI be three pair-wise disjoint sets of respectively concept, role and individual names. A role R is either a role name r or an inverse role r-, where r ∈ NR. EL concepts are built according to the following syntax rule, where A ∈ NC and R ∈ NR:

More expressive DLs allow for the following additional concepts, where n ∈ N, and in brackets, we give the name of the corresponding DL:

In each case, all previous constructs are allowed in the DL as well. Using the letter I in the DL name we express that in the above, R may also be an inverse role. For example, (≥nr-.C) is an ALCQI concept but not an ALCQconcept, and ∃r.⊥ is an EL⊥ concept. Additional operators are introduced as abbreviations: C ⊔ D = ¬(¬C ⊓ ¬D) and ∀R.C = ¬∃R.¬C.

A KB is a set of axioms, that is, concept inclusions (CIs) C ⊑ D, concept assertions C(a) and role assertions r(a, b), where C, D are concepts, a, b ∈ NI and r ∈ NR. If a KB contains only concept and role assertions, it is called ABox, and if every concept assertion is of the form A(a), where A ∈ NC, flat ABox. Given a concept/axiom/KB/ABox E, we denote by sub(E) the set of (sub-)concepts occurring in E, by sig(E) the set of concept and role names occuring in E, and by ind(E) the set of individual names in E. By size(E), we denote the number of symbols required to write E down, where operators, as well as concept, role and individual names count as one, numbers are encoded in binary and the introduced abbreviations can be used.

The semantics of DLs is defined based on interpretations, which are tuples I = 〈∆I , ·I 〉 of a set ∆I of domain elements and an interpretation function ·I which maps every a ∈ NI to some aI ∈ ∆I , every A ∈ NC to some AI ⊆ ∆I , every r ∈ NR to some rI ⊆ ∆I × ∆I , satisfies (r-)I = (rI )-, and is extended to concepts as follows, where #S denotes the cardinality of the set S:

I satisfies an axiom α, in symbols I |= α, if α = C ⊑ D and C I ⊆ DI ; α = C(a) and aI ∈ C I ; or α = r(a, b) and 〈aI , bI 〉 ∈ rI . If I satisfies all axioms in a KB K, we write I |= K and call I a model of K. A KB entails an axiom/KB E, in symbols K |= E, if I |= E for every model I of K. If K has no model, it is inconsistent and we write K |= ⊥.

We can now define the main reasoning problem we are concerned with in this paper. We consider signature-based ABox abduction problems, which for convenience, we just call abduction problems from here on.

Definition 1. Let Lbe aDL. AnLabduction problem is given by a triple A = 〈K,Φ,Σ〉, with an L KB K of background knowledge, an L ABox Φ as observation, and a signature Σ ⊆ NC ∪ NR of abducibles; and asks whether there exists a hypothesis for A, i.e. an L ABox H satisfying

If we require H additionally to be flat, we speak of a flat abduction problem.

Condition A1 is required to avoid trivial solutions, since everything follows from a basic inconsistency. Condition A2 ensures the hypothesis is indeed effective, and Condition A3 is what makes this a signature-based abduction problem.

In addition, different minimality criteria can be put on the hypothesis, such as size-, subset-, semantic minimality [Calvanese et al., 2013], or completeness [Koopmann et al., 2020]. In this paper, we consider size minimality, for which the corresponding decision problem is the following.

Definition 2. A size-restricted (flat) L abduction problem is a tuple A = 〈K, Φ, Σ, n〉, where A′ = 〈K, Φ, Σ〉 is a (flat) L abduction problem and n is a number encoded in binary. A hypothesis for A is an L-ABox H which is a hypothesis for A′ and additionally satisfies size(H) ≤ n.

3 Flat ABox Abduction

We first consider flat ABox abduction: the size of hypotheses, and the complexity of deciding their existence. This problem is similar to that of query emptiness [Baader et al., 2016] which asks whether for a given set T of CIs, Boolean query q and signature Σ, there exists a flat ABox A with sig(A) ⊆ Σ, s.t. T ∪ A entails that query. Query emptiness for instance queries is essentially the special case of flat ABox abduction where the observation is of the form A(a) and the background knowledge contains only CIs. This immediately gives us lower bounds for the decision problem of flat ABox abduction. The other results in this section do not follow, but can be shown similarly as in [Baader et al., 2016]. Similar to query emptiness, flat ABox abduction only becomes interesting if the DL is powerful enough to create inconsistencies. Otherwise, we can construct a trivial hypothesis candidate as

Clearly, H satisfies A1 and A3. If it does not satisfy A2, then neither would any other ABox. Consequently, if there is a solution to the abduction problem, then H must be such a solution. This means that for EL, flat ABox abduction can always be performed in polynomial time. On the other hand, already for EL⊥, solutions may require exponentially many fresh individual names.

Theorem 1. There exists a family 〈Kn,Φ,Σ〉n>0 of flat EL⊥ abduction problems s.t. every hypothesis is of size exponential in the size of Kn.

Proof. We set Φ = A(a) and Σ = {B, r}, and let Kn use concept names X1, X1, . . ., Xn, Xn to encode an exponential counter. Kn uses this to ensure that an r-chain of distinct

2n elements from a to an instance of B entails A(a).

The only way to produce this chain of 2n elements is using 2n-1 role assertions, which establishes our lower bound.

This bound remains tight if we add expressivity up to ALCI, while we lose any bound on the size once we additionally allow concepts of the form ⩽1r.⊤.

Theorem2. If there exists a hypothesis for a flat L abduction problem A, then there exists one of size

1. polynomial in the size of A if L = EL,
2. exponential in the size of A if L = ALCI, and
3. if L = ALCF, no general upper bound based on A can be given.

Proof sketch. We already established the bound for L = EL. For ALCI, we assume there exists some hypothesis H0, based on which we build one of bounded size. For this, we pick any model I of H0 ∪K, which allows us to identify individual names a ∈ ind(H0) using at most exponentially many types tp(a) = tp(aI )I, where

We associate to every type tp(a) an individual name btp(a), and define h : ind(H0) → NI by h(a) = a if a ∈ ind(K ∪ Φ) and h(a) = btp(a) otherwise. The hypothesis H is then:

Based on I and h, one can construct a model for K ∪H, so that H satisfies A1. Because H0 satisfies A3, by construction, so does H. Finally, using the fact that h is a homomorphism from K ∪ H0 into K ∪ H s.t. for every a ∈ ind(K ∪ Φ) h(a) = a, we can show that K ∪ H |= Φ, and thus A2.

For L = ALCF, we note that if there was a bound on the size of hypotheses, we could decide the instance query emptiness problem for ALCF by iterating over all candidates, contradicting that this problem is undecidable for ALCF [Baader et al., 2016].

The proof of Theorem 2 indicates how types can be used to perform abduction, which is used in the following theorem.

Theorem 3. Flat L ABox abduction is

• P-complete for L = EL,
• EXPTIME-complete for L = EL⊥,
• CONEXPTIME-complete for L = ALCI,
• undecidable for L = ALCF.

Proof sketch. For EL, we already described amethod to compute and verify hypotheses in P. For the other DLs, we use type elimination to compute in exponential time the set TK∪Φ of types t ⊆ sub(K∪Φ) that can occur in models of K. For a type t and a set T of types, we denote by SrT (t) ⊆ T the types an r-succesor of a t-individual can have. We iterate over all assignments s : ind(K ∪ Φ) → TK∪Ψ for which we set

where I contains an additional individual name for every type and s is extended to I. If there exists a hypothesis, then the hypothesis constructed in the proof for Theorem 2 is contained in some such Hs s.t. K ∪ Hs ̸|= ⊥, so that we can directly check A1-A3 from Def. 2 on the generated Hs. A1 can be verified syntactically using the types. For EL⊥, A2 is verified in time polynomial in the size of Hs and thus in EXPTIME. For ALCI, we guess a model of K∪Hs that does not entail Φ by assigning a type to every individual and possibly adding a new element per type. If this fails, K∪Hs |= Φ.

4 Abduction with Complex Concepts

As illustrated in the introduction, abduction may only be successful if we also admit complex concepts in the hypothesis. Determining such hypotheses turns out to be more challenging than for flat hypotheses, and we cannot find a correspondence to a known problem as for flat abduction. Indeed, one might assume such a relation to uniform interpolation: given a KB K and a signature Σ, the uniform interpolant of K for Σ is a Σ ontology that captures all entailments of K within Σ [Koopmann and Schmidt, 2015]. By negating the observation, this can be used to perform complete abduction [Koopmann et al., 2020; Del-Pinto and Schmidt, 2019], that is, to compute a hypothesis that would be entailed by any other hypothesis. However, if we are interested just in computing any hypothesis rather than a complete one, this correspondence falls short, as uniform interpolants have stronger requirements than hypotheses, and the reasons for non-existence are different: namely, capturing all entailments of K in Σ in the uniform interpolant, using only names from Σ, may require infinitely many axioms in case of cyclic axioms. In contrast, for abduction, non-existence is always due to Condition A1.

We consider abduction for ALC, EL, and EL⊥, starting with the latter. In EL and EL⊥, complex concepts do not bring much benefit compared to fresh individuals: an EL⊥ concept can only state the existence of role successors, which we can also do in flat ABoxes. In fact, for EL⊥, if we allow complex concepts instead of fresh individuals , hypotheses even get more complex.

Theorem 4. There exists a family of EL⊥ abduction problems for which every hypothesis without fresh individuals is at least of double exponential size. If there exists such a hypothesis, there always exists one of at most double exponential size, whose existence can be decided in exponential time.

Proof sketch. The family of abduction problems is obtained similarly as in the proof for Theorem 1, only that we now use two roles r and s To get the corresponding upper bound, we first flatten an existing hypothesis H0 and again simplify the ABox based on the types in some model, however this time making sure the resulting flat ABox can be translated back into a complex one without fresh individuals.

The same care has to be taken when we modify the method used for Theorem 3. Specifically, we have to make sure that the hypothesis Hs that we generate for a given mapping s : ind(K ∪ Φ) → TK∪Φ does not contain cycles between fresh individuals, so that it can be translated into a hypothesis without fresh individuals. Our fresh individuals are now of the form ba,t,i, where a ∈ ind(K ∪ Φ), t ∈ T = TK∪Φ, and i ∈ J1, 2|T | K. Set ba,s(a),0 = a. Hs is then defined as:

The hardness result requires again ⊥: for EL, we can always use a flat solution as in the last section. In contrast, with more expressivity, the problem becomes even harder, even if we do admit fresh individuals. The reason is that for concepts of the form ∀r.C, fresh individuals cannot come to the rescue anymore, and disjunctions may become necessary. The following theorem is shown by a modification of a construction in [Ghilardi et al., 2006].

Theorem 5. There is a family of ALC abduction problems for which the smallest (non-flat) ABox hypotheses are triple exponential in size.

We can show that this bound is tight.

Theorem 6. Let A be an ALC abduction problem. Then, there exists a hypothesis for A iff there exists a hypothesis of triple exponential size.

To show this theorem, we use a technique similar as for Theorem 2: we take an arbitrary hypothesis, and transform it into one of triple exponential size. However, this time, a construction based on a single model is not sufficient, and we have to take into account an appropriate abstraction of several models of K ∪ H0. We thus proceed as follows:

1. we abstract the KBK∪H0 into a model abstraction,
2. we reduce the size of this abstraction,
3. based on which we construct a hypothesis H of triple exponential size.

In the model abstraction, elements are represented as nodes v ∈ V that are labeled with a set λ(v) of types with the intuitive meaning "this element may have one of the types in λ(v)". Role relations are represented using tuples 〈v1, t, r, v2〉 which are read as: if the node v1 has type t, then it has an r-successor corresponding to v2. Roughly, from a model abstraction, we can obtain a model using the following inductive procedure: 1) start with the nodes that represent individuals, 2) assign to each node a type from its label set, 3) if for those types, the node requires successor nodes, add those and continue in 2). To allow for unbounded paths in models for finite acyclic model abstractions, we further have "open" nodes whose role successors are only restricted by the TBox.

Definition 3. An interpretation abstraction for 〈K,Φ,Σ〉 is a tuple I = 〈V, λ, s, R, F 〉, where

• V is a set of nodes,
• λ : V → 2TK∪Φ maps each node to a set of types,
• partial function s : NI ↛ V assigns individuals to nodes
• R ⊆ (V ×TK∪Φ×(Σ∩NR)×V ) is the role assignment,
• and F ⊆ V is the set of open nodes.

I abstracts an interpretation I if there is a subset ∆′ ⊆ ∆I and a function h : ∆′ → V s.t. for every d ∈ ∆′ and r ∈ (Σ ∩ NR):

• I1 for all a ∈ NI, if s(a) is defined, then s(a) = h(aI )
• I2 tp(d)I ∈ λ(h(d)),
• I3 if h(d) ̸∈ F, then for every e ∈ ∆I , 〈d, e〉 ∈ rI iff e ∈ ∆′ and 〈h(d), tp(d)I, r, h(e)〉 ∈ R.

We need some additional requirements to make sure an interpretation abstraction can be represented as an ALC ABox H s.t. sig(H) ⊆ Σ. We call a node v ∈ V for which there exists a ∈ NI with s(a) = v internal node, and otherwise outgoing node. If v = s(a) for a ∈ ind(K ∪ Φ), we call v named node. A path in 〈V, λ, s, R, F 〉 is a sequence

s.t. for each i ∈ J0, n-1K, 〈vi, ti, ri, ti+1〉 ∈ R. π is cyclic if it contains a node twice, and its length is its number of nodes.

Definition 4. I = 〈V, λ, s,R, F〉 is called ALC-conform if

• D1 there is no cyclic path between outgoing nodes ,
• D2 for every internal node v, if 〈v, t, r, v′ 〉 ∈ R, then 〈v, t′ , r, v′ 〉 ∈ R for every t′ ∈ λ(v′ ), and
• D3 for every 〈v1, t, r, v2〉 ∈ R, where v2 is internal, there exists 〈v1, t, r, v′2 〉 ∈ R s.t. v′2 is outgoing.

We say that I is Σ-complete if

• D4 for every v ∈ V , and t1 ∈ λ(v), λ(v) contains every type t2 ∈ TK∪Φ s.t. λ(t1) ∩ Σ = λ(t2) ∩ Σ, and
• D5 for every 〈v1, t, r, v2〉 ∈ R and t′ ∈ TK∪Φ s.t. t ∩ Σ = t′ ∩ Σ, also 〈v1, t′ , r, v2〉 ∈ R.

D1 ensures that we can represent the outgoing paths from a node s(a) in a single assertion C(a). D2 expresses that the relations between internal nodes is independent of the type, which allows to represent them using role assertions. D3 is needed to capture allowed paths using universal role restrictions. D4 and D5 ensure that I can be captured using only names in Σ.

From here on, we fix an abduction problem A = 〈K, Φ, Σ〉. We say that I explains Φ iff some model of K is abstracted by I and every model of K that is abstracted by I entails Φ. If I is ALC-conform, Σ-complete, and explains Φ, we call it a hypothesis abstraction.

Lemma 1. Every hypothesis H for A can be translated into a hypothesis abstraction.

Now that we can translate hypotheses into an alternative representation, the next step is to decrease their size while making sure they still explain the observation. For this, we can now use similar techniques as in Theorems 2 and 4, where we now identify nodes v ∈ V based on the their label λ(v) instead of on a single type.

Lemma 2. Let I be a hypothesis abstraction. Then, I can be transformed into a hypothesis abstraction I′ = 〈V ′ , λ′ ,R′ , F ′ 〉 where, for ℓ = |TK∪Φ| · 2|TK∪Φ| , i) V ′ contains at most ℓ internal nodes, ii) every v ∈ V ′ has at most ℓ successors in R′ , and iii) every path of outgoing nodes contains at most ℓ nodes.

The final ingredient to establish Theorem 6 is the following lemma.

Lemma 3. For every ALC-conform, Σ-complete interpretation abstraction I = 〈V, λ, s,R, F〉, there exists an ABox H s.t. i) the models of K ∪ H are exactly the models of K accepted by I, ii) |ind(H)| ≤ |V |, and iii) for every a ∈ ind(H), H contains one assertion C(a), with size(C) exponentially bounded by the path lengths between outgoing nodes in I.

Unfortunately, interpretation abstractions cannot be as easily constructed by a deterministic procedure as we did for Theorems 3 and 4, as there can to be non-trivial interactions between connected internal nodes, and we only have a double exponential upper bound on their number. To decide ALC abduction, we can however guess an interpretation abstraction within the bounds of Lemma 2, and then guess assignments of types to nodes to obtain its models. We thus obtain the following theorem.

Theorem 7. ALC ABox abduction is in N2EXPTIME NP .

5 Size-Restricted Abduction

Because hypotheses can become very large, a natural requirement is to compute hypotheses of minimal or bounded size. We here obtain the following complexities.

Theorem 8. Size restricted L ABox abduction is

• NP-complete for L = EL,
• NEXPTIME-complete for L = EL⊥,
• NEXPTIME NP -complete for the flat variant and L ∈ {ALC,ALCI}, and
• in 2EXPTIME for L = ALCQI.

The upper bounds are based on guess-and-check algorithms. For EL, we exploit the fact that, by Theorem 2, we can always find a solution of polynomial size. For EL⊥, we note that the size of the hypothesis is exponentially bounded by the number of bits used for the size bound k. The NEXPTIME NP -upper bound can be obtained by a refinement of the procedure used in the proof for Theorem 3. For the double exponential upper bound, we iterate over the double exponentially many possible KBs within the size and signature bounds-independent on whether we are interested in flat or complex solutions-and then check for entailment in time exponential in the size of the current solution. The lower bounds are provided by the following lemmas.

Lemma 4. Size-restricted EL abduction is NP-hard.

Proof sketch. We reduce the NP-complete problem CNFSAT to deciding whether a given signature-based problem has a hypothesis of size at most k. Let φ = c1 ∧. . .∧cn be a CNF formula over propositional variables p1, . . . , pm. K contains the following axioms:

Φ contains P(pi) for every i ∈ J1,mK and C(ci) for every i ∈ J1, nK. Finally, Σ = {True, False}. 〈K,Φ,Σ〉 has a hypothesis of size at most 2m iff φ is satisfiable.

Lemma 5. Size restricted EL⊥ abduction is NEXPTIMEhard.

Proof sketch. The hardness follows from a reduction of the NEXPTIME-complete exponential tiling problem, which is given by a tuple 〈T, TI, te, V,H, n〉 of a set T of tile types, a sequence TI ∈ T ∗ of initial tiles, a final tile te, vertical and horizontal tiling conditions V,H ⊆ T × T , and a number n in unary encoding. A solution to this problem is then a tiling, as a function f : J1, 2n K × J1, 2n K → T assigning tiles to coordinates, s.t. the first tiles are as in TI, f(2n , 2n ) = te, and that obeys the vertical and horizontal tiling conditions [van Emde Boas, 1997].

In the reduction, concept names Start and End respectively mark the initial and the final tile. We implement two binary counters X and Y as for Theorem 1 which are decremented over the roles x and y, and encode the coordinates of the tiles. Each tile type t ∈ T is represented by a concept name At. We enforce the horizontal tiling conditions using CIs

and correspondingly for the vertical conditions. The (hidden) concept name B ̸∈ Σ is used to ensure that the hypothesis contains at least one individual per coordinate. This name is initialised by the individual satisfying Start, and then propagated in x and y direction, provided that a tiling type is associated. The observation to be explained is End(a), where End occurs in the following CI:

and the abducibles are

Without the size restriction, a valid hypothesis corresponds to a binary tree with tile types associated to each node, and tiling conditions ensured along the x- and y-successors. To make sure it forms a 2n × 2n grid, we choose the size k appropriately in a way that every coordinate can be used at most once. Valid hypotheses of size k then correspond to solutions to the tiling problem.

To present the proof idea for the NEXPTIME NP -hardness result more concisely, we introduce a new tiling problem.

Definition 5. A NEXPTIME NP -tiling problem is given by a tuple 〈T, TI, te,H1, V1,H2, V2, n〉, where 〈T, TI, te,H1, V1, n〉 is an exponential tiling problem, H2, V2 ⊆ T × T are additional tiling conditions, and for which we want to decide the existence of a valid tiling f : J1, 2n K × J1, 2n K → T for the tiling problem 〈T, TI, te, V1,H1, n〉, s.t. for no i ∈ J1, 2n K, there exists a valid tiling for the tiling problem 〈T, f(i), te, V2,H2, n〉, where f(i) denotes the ith row of the tiling f.

In other words, we have to find a tiling using conditions H1 and V1, while avoiding any rows that can be first row of any tiling for conditions H2 and V2.

Lemma 6. The NEXPTIME NP -tiling problem is NEXPTIME NP -hard.

Lemma 7. Size-restricted ALC abduction is NEXPTIME NP - hard.

Proof sketch. We modify the construction for Lemma 5 to encode the NEXPTIME NP -tiling problem. We now use 3 roles x, y, z and corresponding binary counters so that, together with the size restriction, each hypothesis will have the shape of a cube. The bottom side of this cube has to correspond to a tiling for 〈T, TI , te, V1,H1, n〉, which can be achieved using similar axioms as for Lemma 5. For nodes outside of the bottom side of the cube, we require the use a different set of concept names for the tile types, which are of the form A∗t , and for which we have the axiom T ∗ ⊑ ⊔t∈T A∗t . We use

and again require every coordinate to be assigned some tile type. For the coordinates outside the bottom side, we have to use the concept name T ∗ to assign tile types, which leaves the precise selection of the tile type to the different models of the hypothesis. We detect tiling errors in the different x × zsquares with the following axioms

and correspondingly for V2. This information is propagagated along the succeeding coordinates so that the observation End(a) is only entailed if every model of the hypothesis encodes a tiling error on each of the x × z squares.

6 Outlook

We believe that our results for complex abduction in ALC can be extended to ALCI, and that the bound for size restricted ALCQI abduction in is tight. A question is whether we can improve the N2EXPTIME NP -bound for the most general variant of our abduction problem. Apart from that, we want to investigate our setting for observations formulated as conjunctive queries, which would allow us to explain negative query answers [Calvanese et al., 2013]. Another interesting question is what happens if we allow fresh individual names for abduction with ontologies formulated using existential rules. For the EL⊥-variant, we are currently working on a practical method for computing size-minimal flat hypotheses.

Acknowledgements

Patrick Koopmann is supported by DFG grant 389793660 of TRR 248 (see https://www.perspicuous-computing.science/).