=Paper= {{Paper |id=Vol-477/paper-26 |storemode=property |title=Query Answering over DL ABoxes: How to Pick the Relevant Symbols |pdfUrl=https://ceur-ws.org/Vol-477/paper_29.pdf |volume=Vol-477 |dblpUrl=https://dblp.org/rec/conf/dlog/BaaderBLW09 }} ==Query Answering over DL ABoxes: How to Pick the Relevant Symbols== https://ceur-ws.org/Vol-477/paper_29.pdf
             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