Query Answering over DL ABoxes: How to Pick the Relevant Symbols Franz Baader1 , Meghyn Bienvenu2 , Carsten Lutz3 , and Frank Wolter4 1 TU Dresden, Germany, baader@inf.tu-dresden.de 2 Universität Bremen, Germany, meghyn@informatik.uni-bremen.de 3 Universität Bremen, Germany, clu@informatik.uni-bremen.de 4 University of Liverpool, UK, wolter@liverpool.ac.uk 1 Introduction One of the main applications of description logics (DLs) is ontology-based data access: a conceptual model of a domain is formalized using a DL TBox, and this formalization is exploited to obtain complete answers when querying data stored in an ABox. The current availability of professional and comprehensive ontologies for the bio-medical domain such as SNOMED CT, NCI, and Galen allows an easy and inexpensive adoption of this approach in bio-medical applications such as querying electronic medical records [1]. In such applications, it is typical that an “off-the-shelf” ontology such as SNOMED CT is used together with ABoxes that derive from the actual application. Since ontologies such as SNOMED CT are huge, containing more than 400.000 concept names and embracing various areas such as anatomy, diseases, medication, and even social context and geographic location, it is usually the case that many symbols (concept or role names) defined in the ontology are excluded from the signature Σ used to formulate ABoxes in the given application. Such an excluded symbol S may be linked to the symbols in Σ via the TBox and thus still be relevant for querying Σ-ABoxes, but it may also be completely unrelated to Σ and thus never contribute to deriving certain answers to queries posed against Σ-ABoxes. Clearly, symbols of the latter kind are not relevant for formulating queries in the considered application. The aim of this paper is (i) to propose a notion of ABox relevance of a symbol that describes when a symbol S is relevant for ABoxes formulated in a given signature Σ, with a given background TBox T in place; and (ii) to study the computational complexity of deciding ABox relevance. This decision problem is of interest for a variety of reasons. First, knowing which symbols are relevant for ABox querying is useful for the construction of meaningful queries because non-relevant symbols can be discarded. When working with TBoxes that have more than 400.000 concept names such as SNOMED CT, support of this type is clearly indispensable. Second, the set of relevant symbols can be used to guide module extraction [2–4]. Recall that module extraction is the problem of extracting a subset M from a TBox T so that M can be used instead of T in a particular application. In most cases, the extraction of M is guided by a signature Σ that is of interest for the application and about which the module should “say the same” as the original TBox. If the targeted application is query answering, it is natural to use as the signature Σ the set of symbols that are relevant for ABoxes formulated in the desired ABox signature. With the right notion of ‘module’ at hand, the extracted module can then be used instead of the original TBox for query answering. Note that our notion of relevance is based on an ABox signature instead of on a concrete ABox. The rationale behind this is that, in typical applications, the ABox changes frequently which makes it unrealistic to assume that the set of relevant symbols is re-computed after every ABox modification, not to speak of the rather costly module extraction. The notion of ABox relevance depends on the query language used. In this paper, we study instance queries as the simplest kind of query commonly used, and conjunctive queries due to their recent popularity in the DL community [5– 13]. After introducing preliminaries in Section 2, we present our notion of ABox relevance along with some basic observations in Section 3. We then analyze the complexity of deciding relevance in the EL family of DLs in Section 4, showing that it ranges from polynomial to ExpTime-complete. Results on the ALC fam- ily of DLs are given in Section 5, showing in particular that ABox relevance is decidable in ALC and ALCI, but relevance regarding instance queries is unde- cidable in ALCF and relevance regarding conjunctive queries is undecidable in ALCF I. Some proofs are deferred to the full version [14]. 2 Preliminaries We consider various DLs throughout the paper and use standard notation for syntax, semantics, and DL names, see [15]. In particular, we use NC and NR to denote the sets of concept names and role names, C, D to denote (potentially) composite concepts, A, B for concept names, r, s for role names, and a, b for individual names. When we speak of a TBox, we mean a set of concept inclu- sions (CIs) C v D. An ABox is a set of concept assertions A(a) and ¬A(a) and role assertions r(a, b). To distinguish this kind of ABox from ABoxes that admit composite concepts in concept assertions, we sometimes use the term lit- eral ABox. We use Ind(A) to denote the set of individual names used in the ABox A. As usual in the context of query answering, we adopt the unique name assumption (UNA). We study two query languages: (i) the set IQ of instance queries, which take the form A(v); and (ii) the set CQ of conjunctive queries (CQs), which take the form ∃v.ϕ(v, u) where ϕ is a conjunction of atoms of the form A(t) and r(t, t0 ) with t, t0 terms, i.e., variables or individual names. Note that we disallow composite concepts in instance queries and conjunctive queries, which is a realistic assumption for many applications. Also note that instance queries can only be used to query concept names, but not role names. This is the traditional definition, which is due to the fact that role assertions in an ABox can only be implied by an ABox if they are explicitly contained in it (and thus querying is trivial). Given a TBox T , an ABox A, and a (conjunctive or instance) query q with k answer variables v1 , . . . , vk , we write T , A |= q[a1 , . . . , ak ] if the tuple (a1 , . . . , ak ) of individual names is a certain answer to q w.r.t. A and T (defined in the usual way). We use certT ,A (q) to denote the set of all certain answers to q w.r.t. A and T . We use the term symbol to refer to a concept name or role name, signature to refer to a set of symbols, and sig(q) to denote the set of symbols used in the query q. Given a signature Σ, a Σ-ABox (resp. Σ-concept) is an ABox (resp. concept) using symbols from Σ only. 3 The ABox Relevance Problem The following definition describes the set of symbols ΣTL that can meaningfully be used in a query posed against ABoxes that are formulated in the signature Σ, with the TBox T in the background. Definition 1. Let T be a TBox, Σ a signature, and L ∈ {IQ, CQ} a query language. A symbol S is L-relevant for Σ given T if there exists a Σ-ABox and L-query q such that A is consistent w.r.t. T , S ∈ sig(q), and certT ,A (q) 6= ∅. The L-extension of Σ given T is the following signature: ΣTL := Σ ∪ {S ∈ NC ∪ NR | S is L-relevant for T and Σ}. For example, the concept name A is both IQ- and CQ-relevant for Σ = {r} given T = {∃r.> v A}, as witnessed by the query q = A(v) and Σ-ABox {r(a, b)} since certT ,A (q) = {a}. Note that ΣTIQ can never include any role names since role names cannot occur in an instance query. We are interested in deciding L- relevance for L ∈ {IQ, CQ}: given a TBox T , a signature Σ and a symbol S, decide whether S ∈ ΣTL . Clearly, this problem can be used to compute the signature ΣTL . It should not be surprising that, in general, we need not have ΣTIQ = ΣTCQ . For example, if T = {A v ∃r.B} and Σ = {A}, then B ∈ / ΣTIQ , but B ∈ ΣTCQ . For the former, it suffices to note that certT ,A (B(v)) = ∅ for all Σ-ABoxes A. For the latter, note that certT ,A (∃v.B(v)) = {()} when A = {A(a)} (and where () is the empty tuple representing a positive answer to the Boolean query). The following lemma, which is independent of the DL in which TBoxes are formulated, shows that we can always concentrate on CQs of such a simple form. It is an easy consequence of the fact that, since composite concepts are disallowed, CQs are purely positive, existential, and conjunctive. Lemma 1. A ∈ NC (resp. r ∈ NR ) is CQ-relevant for Σ given T iff there is an ABox A with certT ,A (∃v.A(v)) 6= ∅ (resp. certT ,A (∃v, v 0 .r(v, v 0 )) 6= ∅). Lemma 1 allows us to consider only queries of the form ∃v.A(v) and ∃v, v 0 .r(v, v 0 ) when dealing with CQ-relevance. From now on, we do this without further notice. Answering conjunctive queries is typically more difficult than answering in- stance queries, both regarding the computational complexity and the required algorithms [7, 9]. Thus, it may be a little surprising that, as stated by the fol- lowing result, CQ-relevance can be polynomially reduced to IQ-relevance. The converse is, in general, not known. In Section 4, we will see that it holds in the EL family of DLs. Theorem 1. In any DL with (qualified) existential restrictions, CQ-relevance can be polynomially reduced to IQ-relevance. Proof (sketch). Let T be a TBox, Σ a signature, B a concept name that does not occur in T and Σ, and s a role name that does not occur in T and Σ. Then 1. A is CQ-relevant for Σ given T iff B is IQ-relevant for Σ∪{s} given the TBox T 0 = T ∪ TB ∪ {A v B}, where TB = {∃r.B v B | r = s or r occurs in T }; 2. r is CQ-relevant for Σ given T iff B is IQ-relevant for Σ ∪ {s} given the TBox T 0 = T ∪ TB ∪ {∃r.> v B}, where TB is as above. The proofs of Points 1 and 2 are similar and we concentrate on Point 1. First suppose that A is CQ-relevant for Σ given T . Then there is a Σ-ABox A such that T , A |= ∃v.A(v). Choose an a0 ∈ Ind(A) and set A0 := A∪{s(a0 , b) | b ∈ Ind(A)}. Using the fact that T , A |= ∃v.A(v) and the definition of A0 and T 0 , it can be shown that T 0 , A0 |= B(a0 ). For the converse direction, suppose that B is IQ- relevant for Σ ∪ {s} given T 0 . Then there is a Σ ∪ {s}-ABox A0 such that T 0 , A0 |= B(a) for some a ∈ Ind(A0 ). Let A be obtained from A0 by removing all assertions s(a, b). Using the fact that T 0 , A0 |= B(a) and the definition of A0 and T 0 , it can be shown that T , A |= ∃v.A(v). t u In some proofs, it will be convenient to drop the UNA. The following lemma states that this can be done w.l.o.g. in ALCI (and all its fragments such as EL and ALC) because the certain answers and thus also the notion of L-relevance does not change. The lemma is easily proved using the fact that, in ALCI, we can easily convert a model I for an ABox and a TBox that violates the UNA into a model I 0 that satisfies the UNA by “duplicating points” and such that I and I 0 are bisimilar. Lemma 2. Let T be an ALCI-TBox, A an ABox, and q ∈ L. Then certT ,A (q) is identical with and without UNA. An analogous statement fails, e.g., for ALCF. To see this, take T = {> v (≤ 1 r) t A} and Σ = {r}. Then A is IQ- and CQ-relevant with UNA due to the ABox {r(a, b), r(a, b0 )}, but it is not relevant without UNA. 4 The EL Family We study ABox relevance in the EL family of lightweight DLs [16]. In particular, we show that ABox relevance in plain EL can be decided in polynomial time, whereas it is ExpTime-complete in ELI and EL⊥ . It is interesting to contrast these results with the complexity of subsumption and instance checking, which can be decided in polynomial time in the case of EL and EL⊥ and are ExpTime- complete in ELI. Throughout this section, we assume that the UNA is not imposed. This can be done w.l.o.g. due to Lemma 2. Since DLs of the EL family do not offer negation, it may be deemed unnatural to define ABox relevance based on literal ABoxes, which admit negation. However, as the following lemma demonstrates, there is actually no difference between defining ABox relevance based on literal ABoxes and positive ABoxes, in which all concept assertions are of the form A(a) with A a concept name. This holds for both IQ- and CQ-relevance. The proof is via canonical models. Lemma 3. For every ELI ⊥ TBox T , literal ABox A consistent w.r.t. T , and conjunctive query q, we have certT ,A (q) = certT ,A− (q), where A− is the restric- tion of A to assertions of the form A(a) and r(a, b). We now state the announced converse of Theorem 1. The proof proceeds by showing that A is IQ-relevant for Σ given T iff B is CQ-relevant for Σ ∪ {X} given the TBox T 0 = T ∪ {A u X v B}, where B and X are concept names that do not occur in T . Theorem 2. In ELI ⊥ , IQ-relevance can be polynomially reduced to CQ-rele- vance. Theorem 2 allow us to choose freely between IQ and CQ when proving lower and upper bounds for relevance in the EL family of DLs. Note that, by the example given in Section 2, these two notions do not coincide even in EL. Theorem 3. In EL, IQ-relevance and CQ-relevance can be decided in PTime. Proof. We consider IQ-relevance. Let T be an EL-TBox and Σ a signature. Define the total Σ-ABox as AΣ := {A(aΣ ) | A ∈ Σ} ∪ {r(aΣ , aΣ ) | r ∈ Σ}. Claim. For all concept names A, A is IQ-relevant for Σ given T iff T , AΣ |= A(aΣ ); Since the instance problem can be solved in polynomial time in EL [16], Theo- rem 3 is an immediate consequence of the claim. The “if” direction of the above claim is trivial. For the “only if” direction, let A be IQ-relevant for Σ given T . By Lemma 3, there is a positive Σ-ABox A such that T , A |= A(a0 ) for some a0 ∈ Ind(A). Let I be a model of T and AΣ . We have to show that aI0 ∈ AI . Modify I by setting bI := aIΣ for all individual names b. It is easy to verify that I is a model of the positive ABox A and of T . Since T , A |= A(a0 ), we have aI0 ∈ AI as required. t u Note that we need very little for the proof of Theorem 3 to go through: it suffices that AΣ is consistent with every TBox and that the DL in question is monotone. It follows that for all DLs of this sort, deciding IQ- and CQ-relevance has the same complexity as subsumption/instance checking (whose complexity coincides for almost every DL). The upper bound is obtained as in the proof of Theorem 3, based on instance checking. For the lower bound, note that C is subsumed by D w.r.t. T iff B is IQ-/CQ-relevant for T ∪ {A v C, D v B} and the signature {A}, where A, B ∈ / sig(C, D, T ). We thus obtain the following result for the DL ELI, in which subsumption and instance checking are ExpTime-complete [17]. Theorem 4. In ELI, IQ-relevance and CQ-relevance are ExpTime-complete. The simplest extension of EL in which the total ABox AΣ is not consistent w.r.t. every TBox is EL⊥ . Here, deciding relevance is significantly harder than deciding subsumption/instance checking (which can be decided in polynomial time). We start by proving an NP lower bound for a very simple fragment of EL⊥ : let L be the DL that admits only CIs of the form A u A0 v B and A u B v ⊥, with A, A0 , and B concept names. This is a fragment of EL⊥ , but also of those variants of DL-Lite that admit conjunction on the left-hand side of CIs [8]. Theorem 5. In L, IQ-relevance and CQ-relevance are NP-hard. Proof. Reduction from SAT. Let ϕ be a propositional formula in NNF using variables v0 , . . . , vn and sub(ϕ) the set of subformulas of ϕ. Define a TBox T as the union of the following: – Avi u A¬vi v ⊥ for all i ≤ n; – Aϑ u Aχ v Aψ for all ψ = ϑ ∧ χ ∈ sub(ϕ); – Aϑ v Aψ , Aχ v Aψ for all ψ = ϑ ∨ χ ∈ sub(ϕ). Let Σ = {Avi , A¬vi | i ≤ n}. It can be verified that Aϕ is IQ-relevant for Σ given T iff ϕ is satisfiable. t u For full EL⊥ , Theorem 5 can be improved to an ExpTime lower bound. The idea is to make use of an existing ExpTime lower bound for deciding conservative extensions in EL/EL⊥ established in [18]. To implement this, we first establish a technical proposition. Its proof is similar to Lemma 22 (i) in [18] and given in the full paper. Proposition 1. If a concept name B is IQ-relevant for a signature Σ given an EL⊥ -TBox T , then there is a Σ-concept C such that C is satisfiable w.r.t. T and T |= C v B. We now prove the lower bound. Theorem 6. In EL⊥ , IQ-relevance and CQ-relevance are ExpTime-hard. Proof. We consider IQ-relevance. The following result can be established by carefully analyzing the reduction underlying Theorem 36 in [18]: given an EL⊥ - TBox T , a signature Σ, and a concept name B, it is ExpTime-hard to decide if there exist a Σ-concept C such that C is satisfiable w.r.t. T and T |= C v B. Thus it suffices to show that the following conditions are equivalent, for any EL⊥ -TBox T , signature Σ, and concept name B: 1. there exists a Σ-concept C such that C is satisfiable w.r.t. T and T |= C v B; 2. there exists a Σ-ABox A such that (T , A) is consistent and (T , A) |= B(a) for some a ∈ Ind(A). The implication from Point 1 to Point 2 is trivial and the reverse direction is established by Proposition 1. t u To prove a matching upper bound for Theorem 6, we first establish a proposition that constrains the shape of ABoxes to be considered when deciding relevance in EL⊥ . Here and in what follows, an ABox A is tree-shaped if 1. the directed graph (Ind(A), {(a, b) | r(a, b) ∈ A for some r ∈ NR }) is a tree and 2. for all a, b ∈ Ind(A), there is at most one role name r such that r(a, b) ∈ A. The following is a simple consequence of Proposition 1. Proposition 2. A concept name A is IQ-relevant for a signature Σ given an EL⊥ -TBox T iff there is a tree-shaped ABox A such that A is consistent w.r.t. T and T , A |= A(a0 ), with a0 the root of A. For the upper bound, we use non-deterministic bottom-up automata on finite, ranked trees. Such an automaton is a tuple A = (Q, F, Qf , Θ), where Q is a finite set of states, F is a ranked alphabet, Qf ⊆ Q is a set of final states, and Θ is a set of transition rules of the form f (q1 , . . . , qn ) → q, where n ≥ 0, f ∈ F is of rank n, and q1 , . . . , qn , q ∈ Q. Note that transition rules for symbols of rank 0 replace initial states. Automata work on finite, node-labeled, ordered trees T = (V, E, `), where V is a finite set of nodes, E ⊆ V × V is a set of edges, and ` is a node-labeling function the maps each node v ∈ V with i successors to a symbol `(v) ∈ F of rank i. We assume an implicit total order on the successors of each node. A run of the automaton A on T is a map ρ : V → Q such that – ρ(ε) ∈ Qf , with ε ∈ V the root of T ; – for all v ∈ V with `(v) = f and where v has (ordered) successors v1 , . . . , vn , n ≥ 0, we have that f (ρ(v1 ), . . . , ρ(vn )) → ρ(v) is a rule in ∆. An automaton A accepts a tree T if there is a run of A on T . We use L(A) to denote the set of all trees accepted by A. It can be computed in polynomial time whether L(A) = ∅. Theorem 7. In EL⊥ , IQ-relevance and CQ-relevance are ExpTime-complete. Proof. Let T be an EL⊥ -TBox, Σ a signature, and A0 a concept name such that it is to be decided whether A0 is IQ-relevant for Σ given T . W.l.o.g., we may assume that A0 occurs in T . We use sub(T ) to denote the set of all subconcepts of concepts occurring in T and set Γ := Σ ∪ sub(T ). A Σ-type is a finite set t of concept names that occur in Σ and such that u t is satisfiable w.r.t. T . A Γ -type is a subset t of Γ such that u t is satisfiable w.r.t. T . Given a Γ -type t, we use clT (t) to denote the set {C ∈ Γ | T |= u t v C}. We use ex(T ) to denote the number of concepts of the form ∃r.C that occur in T (possibly as a subconcept). Define an automaton A = (Q, F, Qf , ∆) as follows: – F = {ht, r1 , . . . , rn i | t a Σ-type, i < ex(T )} with ht, r1 , . . . , rn i of rank n; – Q is the set of Γ -types; – Qf = {q ∈ Q | A0 ∈ q}; – ∆ consists of all rules f (q1 , . . . , qn ) → q with f = ht, r1 , . . . , rn i such that q = clT (t ∪ {∃r.C ∈ sub(T ) | r = ri and C ∈ qi for some i with 1 ≤ i ≤ n}. In the full version of this paper, we show that L(A) 6= ∅ iff A0 is IQ-relevant for Σ given T . Since A is single-exponentially large in |T | and the emptiness problem can be decided in polynomial time in the size of the automaton, we obtain a single-exponential-time procedure for deciding relevance in EL⊥ . t u 5 Expressive DLs We establish some first results for ABox relevance in ALC and its extensions. For ALCI, we prove decidability of IQ- (and thus also CQ-) relevance, and a NExpTimeNP upper bound; for ALCF, we prove undecidability of IQ-relevance. 5.1 ABox Relevance in ALC and ALCI The NExpTimeNP upper bound is based on the following theorem, which places an upper bound on the size of ABoxes that we need to consider. Theorem 8. Let T be an ALCI-TBox. If A ∈ NC is IQ-relevant for T w.r.t. propositional ABoxes, then there is a literal Σ-ABox A such that A is consistent w.r.t. T , T , A |= A(a) for some a ∈ Ind(A), and |Ind(A)| ≤ 2|T |+|Σ| . Proof. We do not make the UNA. We consider only the case A ∈ NC , as the case r ∈ NR is analogous. Assume that A is IQ-relevant for Σ given T . Then there is a literal Σ-ABox A such that A is consistent w.r.t. T and T , A |= A(a0 ) for some a0 ∈ Ind(A). Let I be a model of A and T , and let J be the filtration of I w.r.t. Γ = cl(T ) ∪ {A, ¬A | A ∈ Σ}, i.e., define an equivalence relation ∼ ⊆ ∆I × ∆I by setting d ∼ e iff {C | C ∈ Γ ∧ d ∈ C I } = {C | C ∈ Γ ∧ e ∈ C I } and set ∆J := {[d] | d ∈ ∆I } AJ := {[d] | d ∈ AI } rJ := {([d], [e]) | ∃d0 ∈ [d], e0 ∈ [e] : (d0 , e0 ) ∈ rI } aJ := [aI ] Clearly, |∆J | ≤ 2|T |+|Σ| . It is routine to prove that J is a model of T . Define an ABox AJ = {A(a[d] ) | A ∈ Σ ∧ [d] ∈ AJ } ∪ {¬A(a[d] ) | A ∈ Σ ∧ [d] ∈ (¬A)J } ∪ {r(a[d] , a[e] ) | r ∈ Σ ∧ ([d], [e]) ∈ rJ }. Clearly, J is a model of AJ . Thus, AJ is consistent w.r.t. T . It remains to show that T , AJ |= A(a[aI0 ] ). Let J 0 be a model of AJ and T . Define a model I 0 from 0 0 J 0 by setting aI = (a[aI ] )J for all a ∈ Ind(A). It is readily checked that I 0 is 0 0 0 a model of A and T , and thus a0 ∈ AI , implying aJ [aI ] ∈ AJ as required. t u 0 It is interesting to note that the bound from Theorem 8 is tight. To see this, let T := { A v ¬P0 u · · · u ¬Pn−1 ∃r.(P0 u · · · u Pi ) v ¬Pi ∃r.(P0 u · · · u Pi−1 u ¬Pi ) v Pi ∃r.((¬P0 t · · · t ¬Pi−1 ) u Pi ) v Pi ∃r.((¬P0 t · · · t ¬Pi−1 ) u ¬Pi ) v ¬Pi P0 u · · · u Pn−1 v X } and Σ = {A, r}. Then X is relevant for T and Σ, but the smallest witness ABox is an r-chain of length 2n whose last element is an instance of A. Note that an ABox that has the form of a cycle of length < 2n is inconsistent w.r.t. T . We now use Theorem 8 to prove membership in NExpTimeNP . Theorem 9. In ALCI, IQ-relevance and CQ-relevance are in NExpTimeNP . Proof. We show the result for IQ-relevance; the upper bound for CQ-relevance follows by Theorem 2. Consider the following nondeterministic algorithm: Step 1: Guess a Σ-ABox A such that |Ind(A)| = 2|T |+|Σ| . Step 2: Use an oracle to verify that A is consistent with T . Reject if not. Step 3: For each a ∈ Ind(A), use an oracle to check whether A ∪ {¬A(a)} is consistent with T . Accept if for some a ∈ Ind(A) the ABox A ∪ {¬A(a)} is in- consistent with T . Otherwise reject. If the algorithm accepts, then we have found a Σ-ABox A consistent with T which implies some assertion A(a), i.e. A is IQ-relevant for Σ given T . Con- versely, if A is IQ-relevant, then by Theorem 8, there must be some Σ-ABox A with at most 2|T |+|Σ| individuals which is consistent with T and such that T , A |= A(a) for some a ∈ Ind(A). We create a new Σ-ABox from A as follows: A0 = A ∪ {>(bi ) | 1 ≤ i ≤ 2|T |+|Σ| − |Ind(A)|}. By construction, A0 has precisely 2|T |+|Σ| individuals, is consistent with T , and is such that A0 , T |= A(a). If A0 is guessed in Step 1, the algorithm accepts. We remark that in Steps 2 and 3 of the algorithm, we test the consistency of literal ABoxes that are exponentially larger than the TBox T . Because of this, the standard precompletion approach to deciding ABox consistency w.r.t. a TBox requires only nondeterministic polynomial time (rather than the usual deterministic single-exponential time). This means that we can use an NP-oracle in Steps 2 and 3, yielding membership in NExpTimeNP . t u We conjecture that IQ- and CQ-relevance are actually NExpTimeNP -complete, but leave the lower bound open for now. 5.2 Relevance in ALCF and ALCF I We show that the simple addition of functional roles to ALC leads to unde- cidability of IQ-relevance, and that the further addition of inverse roles leads to undecidability of CQ-relevance. Both proofs are by reduction of the tiling problem of finite (but unbounded) rectangles. An instance of this problem is given by a triple (T, H, V ) with T a non-empty, finite set of tile types includ- ing an initial tile Tinit to be placed on the lower left corner and a final tile Tfinal to be placed on the upper right corner, H ⊆ T × T a horizontal match- ing relation, and V ⊆ T × T a vertical matching relation. A tiling for (T, H, V ) is a map f : {0, . . . , n} × {0, . . . , m} → T such that n, m ≥ 0, f (0, 0) = Tinit , f (n, m) = Tfinal , (f (i, j), f (i+1, j)) ∈ H for all i < n, and (f (i, j), f (i, j +1)) ∈ v for all i < m. It is undecidable whether a tiling problem has a tiling. For the reduction to IQ-relevance in ALCF, let (T, H, V ) be an instance of the tiling problem with T = {T1 , . . . , Tp }. We construct a signature Σ and a TBox T such that (T, H, V ) has a solution iff a selected concept name A is IQ-relevant for Σ given T . More precisely, the ABox A witnessing IQ-relevance has the form of an n × m-rectangle together with a tiling for (T, H, V ). W.l.o.g., we concentrate on solutions where Tfinal occurs nowhere else than in the upper right corner. The ABox signature is Σ = {T1 , . . . , Tp , x, y} where T1 , . . . , Tp are used as concept names and x and y are functional role names representing horizontal and vertical adjacency of points in the rectangle. In T , we additionally use the concept names U, R, A, Y, Z, C, where U and R mark the upper and right border of the rectangle, A is the concept name used in the instance query, and Y , Z, and C are used for technical purposes explained below. More precisely, T is defined as the union of the following CIs, for all (Ti , Tj ) ∈ H and (Ti , T` ) ∈ V : Tfinal v Y u U u R ∃x.(Tj u Y u U ) u Ti v U u Y ∃y.(T` u Y u R) u Ti v R u Y (∃x.∃y.Z u ∃y.∃x.Z) t (∃x.∃y.¬Z u ∃y.∃x.¬Z) v C ∃x.(Tj u Y u ∃y.Y ) u ∃y.(T` u Y u ∃x.Y ) u C u Ti v Y Y u Tinit v A U v ∀y.⊥ R v ∀x.⊥ ∃y.¬R v ¬R ∃x.¬U v ¬U t Ts u Tt v ⊥ 1≤s