Data Complexity of Reasoning in Very Expressive Description Logics

1 Introdcution

Description logics (DLs) [Baader et al., 2003] are state-ofthe-art knowledge representation formalisms with applications in many areas of computer science. Very expressive DLs such as SHIQ are interesting mainly due to their high expressivity combined with the clearly defined model-theoretic semantics and known formal properties, such as the computational complexity of reasoning. In particular, the combined complexity of checking satisfiability of a SHIQ knowledge base KB is EXPTIME-complete in |KB| [Schild, 1991; Tobies, 2001].

EXPTIME-completeness is a rather discouraging result since |KB| can be large in practice. However, similar to a database, KB consists of a schema part T , called the TBox, and a data or fact part A, called the ABox. For applications with a fixed schema but varying data part, data complexity, measured in the size of A only, provides a more precise performance estimate.

Here, we assume that the ABox of KB is extensionally reduced, i.e. it involves only roles and (possibly negated) atomic concepts. Thus, the terminological knowledge is strictly separated from assertional knowledge, so |A| is the measure of "raw" data. For such a KB, we show that checking KB satisfiability is NP-complete in |A|, and that instance checking is co-NP-complete in |A|. Since this might still lead to intractability, we identify Horn-SHIQ, a fragment of SHIQ analogous to the Horn fragment of first-order logic. Namely, Horn-SHIQ provides existential and universal quantifiers, but does not provide means to express disjunctive information. We show that, for Horn-SHIQ, the basic

Ulrike Sattler

Dept. of Computer Science Univ. of Manchester, UK sattler@cs.man.ac.uk

reasoning problems are P-complete in |A|. To develop an intuition and to provide a more detailed account of these results, we compare them with similar results for (variants of) datalog [Dantsin et al., 2001].

Our results are important since they provide a formal justification for hoping to provide tractable algorithms for very expressive description logics. Furthermore, Horn-SHIQ subsumes DL-lite [Calvanese et al., 2004], a logic aiming to capture most constructs of ER and UML formalisms, while providing polynomial algorithms for satisfiability checking and conjunctive query answering (assuming an unbounded knowledge base, but a bound on the query size). HornSHIQ additionally allows qualified existential quantification, conditional functionality and role inclusions, while allowing for a reasoning algorithm that runs in time polynomial in the size of data.

In [Schaerf, 1994], the complexity of concept subsumption was contrasted with combined and data complexity of instance checking for various fragments of ALC. This work provides a lower bound for the data complexity of reasoning in SHIQ.

2 Preliminaries

Description Logics. Given a set of role names NR, a SHIQ role is either some R ∈ NR or an inverse role Rfor R ∈ NR. A SHIQ RBox R is a finite set of role inclusion axioms R ⊑ S and transitivity axioms Trans(R), for R and S SHIQ roles. For R ∈ NR, we set Inv(R) = R- and Inv(R-) = R, and assume that R ⊑ S ∈ R (Trans(R) ∈ R) implies Inv(R) ⊑ Inv(S) ∈ R (Trans(Inv(R)) ∈ R). A role R is said to be simple if Trans(S) /∈ R, for each S ⊑∗ R, where ⊑∗ is the reflexive-transitive closure of ⊑.

Given a set of concept names NC, the set of SHIQ concepts is the minimal set such that each A ∈ NC is a SHIQ concept and, for C and D SHIQ concepts, R a role, S a simple role and n a positive integer, then ¬C, C ⊓ D, ∀R.C and ≥ nS.C are also SHIQ concepts. We use ⊤, ⊥, C1 ⊔ C2, ∃R.C, and ≤ nS.C as abbreviations for A ⊔ ¬A, A ⊓ ¬A, ¬(¬C1 ⊓ ¬C2), ¬∀R.¬C, and ¬(≥ (n+1)S.C), respectively. Concepts that are not concept names are called complex. A literal concept is a possibly negated concept name.

A TBox T is a finite set of concept inclusion axioms of the form C ⊑ D. An ABox A is a finite set of axioms C(a), R(a, b), and (in)equalities a ≈ b and a ̸≈ b. A knowledge base KB is a triple (R, T ,A). KB is extensionally reduced if all ABox axioms of KB contain only literal concepts.

The semantics of KB is given by translating it into firstorder logic by the operator π from Table 1. The main inference problem is checking KB satisfiability, i.e. determining if a first-order model of π(KB) exists. An individual a is an instance of a concept C w.r.t. KB if π(KB) |= πy(C, a), which is the case iff KB ∪ {¬C(a)} is unsatisfiable.

The logic ALCHIQ is obtained by disallowing transitivity axioms in SHIQ RBoxes, and ALC is obtained by disallowing RBoxes, inverse roles and number restrictions. A logic L is between logics L1 and L2 if it contains at least the primitives from L1 and at most the primitives from L2.

We measure the size of concepts by their length, and assume unary coding of numbers, i.e. |≤ nR.C| = n+1+|C|, and use |R(a, b)| = |(¬)A(a)| = 3.

Disjunctive Datalog. A datalog term is a constant or a variable, and a datalog atom has the form A(t1, . . . , tn) or t1 ≈ t2, where ti are datalog terms. A disjunctive datalog program with equality P is a finite set of rules of the form A1 ∨ ... ∨ An ← B1, ...,Bm where Ai and Bj are datalog atoms. Each rule is required to be safe, i.e. each variable occurring in the rule must occur in at least one body atom. A fact is a rule with m = 0. For the semantics, we take a rule to be equivalent to a clause A1 ∨...∨An ∨¬B1 ∨...∨¬Bm. We consider only Herbrand models, and say that a model M of P is minimal if there is no model M ′ of P such that M ′ ⊊ M. A ground literal A is a cautious answer of P (written P |=c A) if A is true in all minimal models of P . First-order entailment coincides with cautious entailment for positive ground atoms.

Reducing KB to Disjunctive Datalog. The results in this paper are based on our algorithm from [Hustadt et al., 2004b]. For a SHIQ knowledge base KB, this algorithm computes a positive disjunctive datalog program with equality DD(KB) which is equisatisfiable with KB.

A minor obstacle in computing DD(KB) are the transitivity axioms which, in their clausal form, do not contain a literal in which all variables of a clause occur. Such clauses are known to be difficult to handle, so KB is preprocessed into an equisatisfiable ALCHIQ knowledge base Ω(KB). Roughly speaking, a transitivity axiom Trans(S) is replaced with axioms of the form ∀R.C ⊑ ∀S.(∀S.C), for each R with S ⊑∗ R and C a concept occurring in KB. This transformation is polynomial, so in the rest of this paper w.l.o.g. we assume KB to be an ALCHIQ knowledge base.

The next step is to translate Ω(KB) into clausal first-order logic. Assuming π is defined as in Table 1, π(Ω(KB)) is transformed into a set of clauses Ξ(KB) using structural transformation to avoid an exponential blowup [Nonnengart and Weidenbach, 2001]. Roughly speaking, the structural transformation introduces a new name for each complex subformula of π(Ω(KB)). A specialized version of the structural transformation is presented in detail in Section 4.

A core property of Ξ(KB) is that it only contains clauses of one of the forms given in Table 2; such clauses are called ALCHIQ-clauses. For a term t, P(t) denotes a disjunction of the form (¬)P1(t) ∨ . . . ∨ (¬)Pn(t), and P(f (x)) denotes a disjunction of the form P1(f1(x)) ∨ . . . ∨Pn(fm(x)) (notice that this allows each Pi(fi(x)) to contain positive and negative literals).

Next, the RBox and TBox clauses of Ξ(KB) are saturated by basic superposition [Bachmair et al., 1995; Nieuwenhuis and Rubio, 1995]-a clausal equational theorem proving calculus. Due to space limitations, we are unable to present the rules of basic superposition; it can be considered to be an optimized version of the well-known paramodulation calculus. Let Γ be the saturated set of clauses. In this key step, all non-ground consequences of KB are computed. In [Hustadt et al., 2004b], we have shown the following key property: (♠) an application of a basic superposition inference rule to ALCHIQ-clauses produces an ALCHIQ-clause. The proof examines all inference rules and clause types.

Furthermore, by examining the types of clauses from Table 2, one can show the following property: (♣) for a finite KB, the number of ALCHIQ-clauses unique up to variable renaming is exponential in |KB|. The proof is a straightforward counting exercise since the number of variables and the depth of functional terms in ALCHIQ-clauses are bounded.

Each inference step can be carried out in polynomial time, so by (♠) and (♣), after at most exponentially many steps, all ALCHIQ-clauses are derived, and saturation terminates.

Satisfiability of Ξ(KB) can be decided by further saturating Γ ∪ Ξ(A) by basic superposition. Since Γ contains all non-ground consequences of Ξ(KB), all remaining inferences will produce only ground clauses, and will not involve clauses of type 4 and 6. These inferences can be simulated in a disjunctive datalog program by transforming Γ into a function-free clause set, and by introducing new constants playing the role of ground functional terms, as described next.

We define an operator λ transforming Γ as follows: (i) each functional term f(a) is replaced with a new, globally unique constant af ; (ii) each term f(x) is replaced with a new, globally unique variable xf ; (iii) for each variable in a clause introduced in step (ii), λ appends a literal ¬Sf(x, xf), where Sf is a new predicate unique for the function symbol f; (iv) if some variable x occurs in a positive, but not in a negative literal in a clause, then the literal ¬HU(x) is appended to the clause; (v) for each function symbol f and each constant a from Ξ(KB), the facts Sf(a, af), HU(a) and HU(af) are added. The set of (function-free) clauses obtained by applying λ to Γ ∪ Ξ(A) is denoted with FF(KB). An example of applying λ to a clause of type 5 is shown below.

Now each remaining ground inference by basic superposition in Γ∪Ξ(A) can be simulated by a sound inference step in FF(KB), and vice versa [Hustadt et al., 2004b], so KB and FF(KB) are equisatisfiable. Since FF(KB) does not contain functional terms and all its clauses are safe, each clause can be rewritten into a positive disjunctive rule; let DD(KB) be the resulting set of rules. The following theorem summarizes the properties of DD(KB):

Theorem 1 ([Hustadt et al., 2004b]). For KB an ALCHIQ knowledge base, the following claims hold: (i) KB is unsatisfiable iff DD(KB) is unsatisfiable; (ii) KB |= α iff DD(KB) |=c α, for α of the form A(a) or S(a, b), A a concept name, and S a simple role; (iii) KB |= C(a) iff DD(KB∪{C ⊑ Q}) |=c Q(a), for C a complex concept, and Q a new concept name; (iv) the number of rules in DD(KB) is at most exponential in |KB|, the number of literals in each rule is at most polynomial in |KB|, and DD(KB) can be computed in time exponential in |KB|.

3 Data Complexity of Reasoning in SHIQ

For an extensionally reduced SHIQ knowledge base KB, an upper bound for the data complexity follows from the reduction of KB to DD(KB). Before presenting the details, we first discuss the intuition behind this result.

By Theorem 1, |DD(KB)| is exponential in |KB|. However, a closer inspection of the reduction algorithm reveals that the exponential blowup is caused by the rules obtained by saturating ALCHIQ-clauses of types 1 - 7, which correspond to TBox and RBox, but not to ABox clauses. Hence, the size of the rules of DD(KB) is exponential in the size of TBox and RBox; however, the size of the facts in DD(KB) is linear in the size of the ABox. Therefore, data complexity of checking satisfiability of DD(KB) corresponds to data complexity of checking satisfiability of a positive disjunctive datalog program, and is thus in NP. Intuitively, this is due to nice property of SHIQ that TBox and RBox reasoning does not "interfere" with ABox reasoning, i.e. all non-ground consequences of KB can be computed without taking the ABox into account. Notice that this result holds even for binary number coding.

Lemma 1 (Membership). For KB an extensionally reduced SHIQ knowledge base, satisfiability of KB can be decided in non-deterministic polynomial time in |A|.

Proof. Let c be the number of constants, f the number of function symbols in the signature of Ξ(KB), and s the number of facts in Ξ(KB) (which is equal to the number of facts in A). By definition of λ, the number of constants in DD(KB) is bounded by ℓ1 = c + cf (cf accounts for constants of the form af ), and the number of facts in DD(KB) is bounded by ℓ2 = s + c + 2cf (c accounts for facts of the form HU (a), one cf accounts for facts of the form Sf (a, af ), and the other cf accounts for facts of the formHU(af)). All function symbols are introduced by skolemizing TBox concepts ∃R.C and ≥ nR.C. Since |T | and |R| are constant, f is also a constant, so both ℓ1 and ℓ2 are linear in |A|.

Hence, |DD(KB)| can be exponential in |KB| only because the non-ground rules in DD(KB) are obtained from exponentially many clauses of types 1 - 7. Since these clause types do not contain ABox clauses, the number of clauses obtained after saturation is obviously exponential in |T | + |R| only. Since we assume that the latter is constant, both the number of rules in DD(KB) and their length are bounded by constants, so |DD(KB)| is polynomial in |A|, and can be computed fromKB in time polynomial in |A|.

As KB and DD(KB) are equisatisfiable, the data complexity of checking satisfiability of KB follows from the data complexity of checking satisfiability of DD(KB), which is NP-complete [Dantsin et al., 2001]: assuming DD(KB) contains r rules and at most v variables in a rule, the number of literals in a ground instantiation ground(DD(KB)) is bounded by r · ℓv1 + ℓ2 (in each rule, each variable can be replaced in ℓ1 possible ways). Assuming r and v are constants, ℘ = |ground(DD(KB))| is polynomial in |A|. Satisfiability of ground(DD(KB)) can be checked by nondeterministically generating an interpretation of size at most ℘, and then checking whether it is a model. Both tasks can be performed in polynomial time, so the overall algorithm is obviously non-deterministically polynomial in |A|.

The hardness of the satisfiability checking problem follows from [Schaerf, 1994, Lemma 4.2.7]. Actually, the lemma shows co-NP-hardness of instance checking, by a reduction of satisfiability of 2-2-CNF propositional formulae. The reduction produces an extensionally reduced ABox and a single TBox axiom, so it applies in our case as well. Hence, we immediately obtain the following result:

Theorem 2. Let KB be an extensionally reduced knowledge base in any logic between ALC and SHIQ. Then (i) deciding KB satisfiability is data complete for NP and (ii) deciding whether KB |= (¬)C(a) with |C| bounded is data complete for co-NP.

4 AHorn Fragment of SHIQ

Horn logic is a well-known fragment of first-order logic where formulae are restricted to clauses containing at most one positive literal. The main limitation of Horn logic is its inability to represent disjunctive information; however, its main benefit is the existence of practical refutation procedures. Furthermore, data complexity of query answering in Horn logic without function symbols is P-complete [Dantsin et al., 2001], which makes it appealing for practical usage.

Following this idea, in this section we identify a Horn fragment of SHIQ, where disjunction is traded for P-complete data complexity. Roughly speaking, in Horn-SHIQ, only axioms of the form bigsqcap Ci ⊑ D are allowed, where each Ci has the form A or ∃R.A, and D has the form A, ⊥, ∃R.A, ∀R.A, ≥ nR.A or ≤ 1R. Whereas such a definition succinctly demonstrates the expressivity of the fragment, in general it is too restricting: e.g., the axiomA1⊔A2 ⊑ ¬B is not Horn, but it is equivalent to Horn axioms A1 ⊓B ⊑ ⊥ and A2 ⊓B ⊑ ⊥. Similarly, a non-Horn axiom A ⊑ ∃R.(∃R.B) can be transformed into Horn axioms A ⊑ ∃R.Q and Q ⊑ ∃R.B by introducing a new name Q for the subconcept ∃R.B. To avoid dependency on such obvious syntactic transformations, we give a rather technical definition of Horn-SHIQ.

We first adapt the notions of positions and polarity in firstorder formulae to DL. A position p is a finite sequence of integers; the empty position is denoted with ǫ. If a position p1 is a proper prefix of a position p2, then and p1 is above p2, and p2 is below p1. For a concept α, the subterm at a position p, written α|p, is defined as follows: α|ǫ = α; (¬D)|1p = D|p; (D1 ◦ D2)|ip = Di|p for ◦ ∈ {⊓, ⊔} and i ∈ {1, 2}; α|1 = R and α|2p = D|p for α = ♦R.D and ♦ ∈ {∃, ∀}; and α|1 = n, α|2 = R and α|3p = D|p for α = ⊲⊳ nR.D and ⊲⊳ ∈ {≤,≥}. A replacement of a subterm of α at position p with a term β is defined in the standard way and is denoted as α[β]p. For a concept α and a position p such that α|p is a concept, the polarity of α|p in α, denoted as pol(α, p), is defined as follows:

Intuitively, pol(α, p) equals 1 if α|p occurs in α under an even number of explicit and implicit negations, and -1 otherwise.

Definition 1. In Table 3, we define two mutually recursive functions pl+ and pl-, where sgn(0) = 0 and sgn(n) = 1 for n > 0. For a concept C and a position p of a subconcept in C, let pl(C, p) = pl+(C|p) if pol(C, p) = 1, and let pl(C, p) = pl-(C|p) if pol(C, p) = -1.

A concept C is a Horn concept if pl(C, p) ≤ 1 for each position p of a subconcept in C (including the empty position ǫ). An extensionally reduced ALCHIQ knowledge base KB is Horn if, for each axiom C ⊑ D ∈ KB, the concept ¬C⊔D is Horn. An extensionally reduced SHIQ knowledge base KB is Horn if Ω(KB) is Horn.

It is easy to see that, for a concept C without complex subconcepts, pl+(C) yields the maximal number of positive literals in clauses obtained by clausifying ∀x : πy(C, x). To clausify a concept C containing a complex subconcept at a position p, one should consider if C|p occurs in C under positive or negative polarity. E.g., in ¬(¬A ⊓ ¬B) the concepts A and B occur effectively positive, and ⊓ is effectively ⊔. Hence, pl+(C|p) (pl-(C|p)) counts the number of positive literals used to clausify C|p, provided that C|p occurs in C under positive (negative) polarity. The function sgn(·) takes into account that C|p will be replaced in C by structural transformation with only one concept name, even if clausification of C|p produces more than one positive literal. E.g., to clausify C = ∀R.(D1 ⊔ D2), the structural transformation replaces D1 ⊔D2 with an new concept name Q, yielding C′ = ∀R.Q; then clausifying C′ produces a clause with only one positive literal. Now a concept C is Horn if the maximal number of positive literals obtained by clausifying subconcepts of C is at most one.

If a concept C has a complex subconcept at position p, special care has to be taken in introducing a new name α for C|p. Consider the Horn concept C = ∀R.D1 ⊔ ∀R.¬D2. To apply structural transformation to C, one might replace ∀R.D1 and ∀R.¬D2 with new concept names Q1 and Q2, yielding concepts ¬Q1 ⊔ ∀R.D1, ¬Q2 ⊔ ∀R.¬D2 and Q1 ⊔ Q2. The problem with such a straight-forward application of structural transformation is that a Horn concept C was reduced to a nonHorn concept Q1 ⊔ Q2, so the structural transformation destroyed Horn-ness. To remedy this, we modify the structural transformation to replace each C|p with a literal concept α such that clausifying α and C|p requires the same number of positive literals. In the above example, this would mean that ∀R.D1 should be replaced with Q1, but ∀R.¬D2 should be replaced with ¬Q2, yielding concepts ¬Q1 ⊔ ∀R.D1, Q2 ⊔ ∀R.¬D2 and Q1 ⊔ ¬Q2, which are all Horn.

Although transitivity axioms are translated by π into Horn clauses, recall that the algorithm from Section 2 replaces them with axioms of the form ∀R.C ⊑ ∀S.(∀S.C). Now pl+(∃R.¬C ⊔ ∀S.(∀S.C)) = 1 + pl+(C), so if pl+(C) > 0, Ω(KB) is not a Horn knowledge base. Hence, the presence of transitivity axioms can make a knowledge base non-Horn.

Definition 2. Let C be a concept and Λ a function mapping C to the set of positions p ̸= ǫ of subconcepts of C such that C|p is not a literal concept and, for all positions q below p, C|q is a literal concept. Then Def(C) is defined recursively as follows, where α = Q if pl(C, p) > 0, and α = ¬Q if pl(C, p) = 0, with Q a new atomic concept, and ¬(¬Q) = Q:

• Def(C) = {C} if Λ(C) = ∅, or
• if Λ(C) ̸= ∅, then choose some p ∈ Λ(C) and let

Let Cls(ϕ) denote the set of clauses obtained by clausifying a formula ϕ in the standard way and let

For an ALCHIQ knowledge base KB, Ξ(KB) is the smallest set of clauses such that: (i) for each role name R ∈ NRa , Cls(π(R)) ⊆ Ξ(KB); (ii) for each RBox or ABox axiom α in KB, Cls(π(α)) ⊆ Ξ(KB); (iii) for each TBox axiom C ⊑ D in KB, Cls(¬C ⊔ D) ⊆ Ξ(KB).

By [Nonnengart and Weidenbach, 2001], ∀x : πy(C, x) and ∧D∈Def(C) ∀x : πy(D, x) are equisatisfiable, so Ξ(KB) and π(KB) are equisatisfiable as well.

Lemma 2. For a Horn-SHIQ knowledge base KB, each clause from Ξ(KB) contains at most one positive literal.

Proof. We first show the following property (*): for a Horn concept C, all concepts in Def(C) are Horn concepts. The proof is by induction on the recursion depth in Def. The induction base for Λ(C) = ∅ is obvious. Consider an application of Def(C), where C is a Horn concept and p a position of a subconcept of C, such that C|p is not a literal concept and, for each position q below p, C|q is a literal concept. Observe that in all cases, we have pl+(α) = pl(C, p) and pl+(¬α) = 1 - pl(C, p). We now consider two cases, depending on pol(C, p):

• pol(C, p) = 1. Now we have pl+(¬α ⊔ C|p) = pl+(¬α) + pl+(C|p) = pl+(¬α) + pl(C, p) = 1. Furthermore, pl(C, p) = pl(C[α]p, p), so C[α]p is Horn.
• pol(C, p) = -1. Now we have pl+(¬α ⊔ ¬C|p) = pl+(¬α) + pl-(C|p) = pl+(¬α) + pl(C, p) = 1. Furthermore, pl(C, p) = pl(C[¬α]p, p), so C[¬α]p is Horn.

Hence, each application of the operator Def decomposes a Horn concept C into two simpler Horn concepts, so (*) holds. Furthermore, for each C|p or ¬C|p in the definition of Def, each immediate subconcept is a literal.

For D ∈ Def(C), by definition of π from Table 1, it is easy to see that pl+(D) gives the maximal number of positive literals occurring in a clause from Cls(∀x : πy(D, x)). Thus, if C is a Horn concept, all clauses from Cls(C) contain at most one positive literal. Finally, clauses obtained by translating RBox and ABox axioms of Ω(KB) also contain at most one positive literal.

As stated by the following lemma, a basic superposition inference, when applied to Horn premises, produces a Horn conclusion. The full proof of the lemma is given in [Hustadt et al., 2004a].

Lemma 3. If all premises of an inference by basic superposition contain at most one positive literal, then inference conclusions also contain at most one positive literal.

Proof. (Sketch) Consider a resolution inference with clauses A ∨ C and ¬B ∨ D, where all literals in C are negative and at most one literal in D is positive. Obviously, the number of positive literals in the conclusion Cσ ∨ Dσ is equal to the number of positive literals in D. Similarly, consider a paramodulation inference from a clause s ≈ t ∨ C into a clause A ∨ D, where all literals in C and D are negative. Obviously, the conclusion Aσ[tσ]p ∨ Cσ ∨ Dσ has only one positive literal. Similar considerations hold for a paramodulation into a negative literal.

By Lemma 2 and 3, if KB is a Horn-SHIQ knowledge base, then DD(KB) is a non-disjunctive program. This is enough for the following result:

Theorem 3. For KB an extensionally reduced Horn knowledge base in any logic between ALC and SHIQ, deciding KB (un)satisfiability, and deciding whether KB |= (¬)C(a) with |C| bounded, is P-complete in |A|.

Proof. Membership in P is a consequence of the fact that DD(KB) is a non-disjunctive program, whose satisfiability can be checked in polynomial time [Dantsin et al., 2001].

For hardness, consider the well-known P-complete problem of deciding whether a path from a node a1 to a node an in a graph G exists [Papadimitriou, 1993]. For a graph G, let KBG be a knowledge base containing the assertions edge(a, b) and edge(b, a) for each edge 〈a, b〉 in G, the axioms C(a1) and ¬C(an), and the TBox axiom C ⊑ ∀edge.C. Obviously, a1 is reachable from an if and only if KBG is unsatisfiable, thus implying P-completeness of unsatisfiability checking. The other inference problems can be reduced to unsatisfiability as usual.

5 Discussion

To better understand the results from the previous two sections, we contrast them with well-known results for (disjunctive) datalog [Dantsin et al., 2001]. Since datalog has been successfully applied in practice, this analysis gives interesting insights into the practical applicability of DLs.

Interestingly, the data complexity of datalog variants and of corresponding SHIQ fragments coincide. Namely, without disjunctions, a SHIQ knowledge base and a datalog program always have at most one model, which can be computed in polynomial time. With disjunctions, several models are possible, and this must be dealt with using reasoning-by-cases. Intuitively, one needs to "guess" a model, which increases data complexity to NP.

The key difference between datalog and DLs is revealed by considering the effects that various parameters have on the complexity. For a datalog program P and a ground atom α, checking whether P |= α can be performed in time O(|P |v ), where v is the maximal number of distinct variables in a rule of P [Vardi, 1995]. Namely, the problem can be solved by grounding P , i.e. by replacing, in each rule of P , all variables with individuals from P in all possible ways. The size of the grounding is bounded by |P|v , and propositional Horn logic is P-complete, giving the above estimate. Now in general, v is linear in |P|, so the size of the grounding is exponential; thus, the combined complexity of datalog coincides with the combined complexity of SHIQ. However, in practical applications v is usually small, so it makes sense to assume it is bounded. Under this assumption, datalog actually exhibits polynomial behavior.

By an analogy, one might try to limit the length of concepts in axioms or the number of variables. For the former, structural transformation can be used to polynomially reduce "long" axioms with complex concepts to "short" axioms with just elementary concepts. For the latter, we note that DLs are closely related to the two-variable fragment of first-order logic: e.g., ALC concepts correspond to first-order formulae with only two variables regardless of nesting (see, e.g., [Baader et al., 2003, ch. 4]). Therefore, the number of variables in DL axioms is "intrinsically" bounded (assuming a bound on the numbers occurring in number restrictions). Hence, neither restriction actually reduces complexity.

We summarize our discussion as follows: assuming a bound on the axiom length, but not on the number of axioms, satisfiability checking in datalog is (non-deterministically) polynomial, but in DLs it is exponential. The reason for this is that DLs such as ALC provide existential and universal quantification and general inclusion axioms, which can be used to succinctly encode models with paths of exponential length. The saturation step eliminates function symbols introduced by existential quantification, but it also incurs an exponential blowup in the program size to account for such paths. Hence, although combined complexity of both datalog and DLs is exponential, the reasons for this are different.

In [Baader et al., 2003, ch. 5] two sources of complexity in DLs have been identified: OR-branching caused by the existence of several possible models, and AND-branching caused by the existence of paths within a model. Our results show that OR-branching is not so "bad" as AND-branching: the former incurs "only" an increase to NP, whereas the latter incurs an increase in complexity to EXPTIME.

6 Conclusion

In many application of DLs, the TBox can be assumed to be rather stable - like a database schema - whereas the ABox is varying and possibly very large - like a database extension. Hence, we study the complexity of reasoning in expressive DLs measured in the size of the ABox. In particular, we show that checking satisfiability of a SHIQ knowledge base is NP-complete, and that checking unsatisfiability and instance checking are co-NP-complete in the size of the ABox. Furthermore, we identify Horn-SHIQ, a fragment of SHIQ which, analogously to Horn logic, does not allow to represent disjunctive knowledge, and for which the basic reasoning problems are P-complete in the size of theABox.

Our results indicate that reasoning with large ABoxes may be feasible if the TBox is not "too" large and if we stay within Horn-SHIQ. To verify these assumptions, we are currently implementing our algorithms and plan to conduct a thorough performance analysis.

Acknowledgments

We thank Enrico Franconi for a stimulating discussion which lead us to the results presented in this paper.