Finite Lattices Do Not Make Reasoning In ALCI Harder Stefan Borgwardt and Rafael Peñaloza {stefborg,penaloza}@tcs.inf.tu-dresden.de Theoretical Computer Science, TU Dresden, Germany Abstract. We consider the fuzzy logic ALCI with semantics based on a finite residuated lattice. We show that the problems of satisfiability and subsumption of concepts in this logic are ExpTime-complete w.r.t. gen- eral TBoxes and PSpace-complete w.r.t. acyclic TBoxes. This matches the known complexity bounds for reasoning in crisp ALCI. 1 Introduction OWL 2, the current standard ontology language for the semantic web, is based on the crisp description logic (DL) SROIQ(D). As a crisp logic, it is not well suited to express vague or imprecise concepts, such as HighTemperature, that can be found in numerous domains; prominently, in the biomedical area. Fuzzy extensions of DLs have been studied for over a decade, and the litera- ture on the topic is very extensive (see [15] for a survey). However, most of those approaches are based on the very simple Zadeh semantics where conjunction is interpreted as the minimum, with truth values ranging over the interval [0, 1] of rational numbers. The last lustrum has seen a shift towards more general se- mantics for treating vagueness. On the one hand, the use of continuous t-norms as the underlying interpretation function for conjunction was proposed in [14]. On the other hand, [18] allows lattice-based truth values, but still restricts to Zadeh-like semantics. Most of the work since then has focused on t-norm-based semantics over the unit interval; yet, ontologies are usually restricted to be unfoldable or acyclic [4– 6]. Indeed, very recently it has been shown that general concept inclusion axioms (GCIs) can cause undecidability even in fuzzy DLs based on ALC [2, 3, 9, 11]. These results motivate restricting the logics, e.g. to finitely-valued semantics. If one considers the Lukasiewicz t-norm over finitely many values, then rea- soning is decidable even for very expressive DLs, as shown in [7] through a reduction to crisp reasoning. When restricted to ALC without terminological axioms, concept satisfiability is PSpace-complete as in the crisp case [10].1 In the presence of general TBoxes, this problem becomes ExpTime-complete [8, 9], again matching the complexity of the crisp case, even if arbitrary (finite) lattices and t-norms are allowed. However, the complexity of subsumption of concepts 1 The paper [10] considers a syntactic variant of fuzzy ALC with only one role. was left as an open problem, as the standard reduction used in crisp DLs does not work with general t-norm semantics. In this paper, we improve these complexity results to the fuzzy logic ALCI L over finite lattices with general and acyclic TBoxes. More precisely, we show that in this logic, concept satisfiability is ExpTime-complete w.r.t. general TBoxes, and PSpace-complete w.r.t. acyclic TBoxes. Moreover, the same complexity bounds also hold for deciding subsumption between concepts. 2 Preliminaries We will first give a short introduction to residuated lattices, which will be used for defining the semantics of our logic.2 Afterwards, we recall some results from automata theory that will allow us to obtain tight upper bounds for the com- plexity of deciding satisfiability and subsumption of concepts. 2.1 Residuated Lattices A lattice is an algebraic structure (L, ∨, ∧) over a carrier set L with two binary operations join ∨ and meet ∧ that are idempotent, associative, and commutative and satisfy the absorption laws `1 ∨ (`1 ∧ `2 ) = `1 = `1 ∧ (`1 ∨ `2 ) for all `1 , `2 ∈ L. L induces the ordering `1 ≤ `2 iff `1 ∧ `2 = `1 for all `1 , `2 ∈ L. L is called distributive if ∨ and ∧ distribute over each other, finite if L is finite, and bounded if it has a minimum and a maximum element, denoted as 0 and 1, respectively. W is complete if joins and meets of arbitrary subsets T ⊆ L, denoted It V by t∈T t and t∈T t respectively, exist. Every finite lattice is also bounded and complete. Whenever it is clear from the context, we will simply use the carrier set L to represent the lattice (L, ∨, ∧). A De Morgan lattice is a bounded distributive lattice extended with an in- volutive and anti-monotonic unary operation ∼, called (De Morgan) negation, satisfying the De Morgan laws ∼(`1 ∨`2 ) = ∼ `1 ∧∼ `2 and ∼(`1 ∧`2 ) = ∼ `1 ∨∼ `2 for all `1 , `2 ∈ L. A residuated lattice is a lattice L extended with two binary operators ⊗ (called t-norm) and ⇒ (called residuum) such that ⊗ is associative, commuta- tive, and has 1 as its unit and for every `1 , `2 , `3 ∈ L, `1 ⊗` W 2 ≤ `3 iff `2 ≤ `1 ⇒ `3 holds. In a complete residuated lattice L, `1 ⇒ `2 = {x | `1 ⊗ x ≤ `2 }.3 A simple consequence of this is that for every `1 , `2 ∈ L, (i) 1 ⇒ `1 = `1 , and (ii) `2 ≤ `2 iff `1 ⇒ `2 = 1. Additionally, the t-norm ⊗ is always monotonic. In a residuated De Morgan lattice L, one can define the t-conorm ⊕ as `1 ⊕ `2 := ∼(∼ `1 ⊗ ∼ `2 ). For example, the meet operator `1 ∧ `2 defines a t-norm; its t-conorm is `1 ∨ `2 . 2 For a more comprehensive view on residuated lattices, we refer the reader to [13, 12]. 3 We could also define the operator ⇒ using this supremum, even if the complete lattice L is not residuated without affecting the results from Section 4. In the following section, we will describe the fuzzy description logic ALCI L , whose semantics uses the residuum ⇒ and the negation ∼. We emphasize, how- ever, that the reasoning algorithm presented in Section 4 can be used with any choice of operators, as long as these are computable. In particular this means that our algorithm could also deal with other variants of fuzzy semantics, e.g. so-called Zadeh semantics [8, 18]. 2.2 PSpace Automata To obtain upper bounds for the complexity of reasoning in ALCI L , we will make a reduction to the emptiness problem of looping automata on infinite trees. These automata receive as input the (unlabeled) infinite k-ary tree K ∗ for K := {1, . . . , k} with k ∈ N. The nodes of this tree are represented as words in K ∗ : the empty word ε represents the root node, and ui represents the i-th successor of the node u. A path is a sequence v1 , . . . , vm of nodes such that v1 = ε and each vi+1 is a direct successor of vi . Definition 1 (looping automaton). A looping automaton (LA) is a tuple A = (Q, I, ∆) where Q is a finite set of states, I ⊆ Q a set of initial states, and ∆ ⊆ Q × Qk the transition relation. A run of A is a mapping r : K ∗ → Q assigning states to each node of K ∗ such that r(ε) ∈ I and for every u ∈ K ∗ we have (r(u), r(u1), . . . , r(uk)) ∈ ∆. The emptiness problem for LA is to decide whether a given LA has a run. The emptiness of LA can be decided in polynomial time using a bottom-up approach [19]. Alternatively, one can use a top-down approach, which relies on the fact that if there is a run, then there is also a periodic run. To speed up the top-down search, one wants to find the period of a run as early as possible. This motivates the notion of blocking automata. Definition 2 (m-blocking). Let A = (Q, ∆, I) be a looping automaton. We say that A is m-blocking for m ∈ N if every path v1 , . . . , vm of length m in a run r of A contains two nodes vi and vj (i < j) such that r(vj ) = r(vi ). Clearly, every looping automaton is m-blocking for every m > |Q|. However, the main interest in blocking automata arises when one can find a smaller bound on m. One way to reduce this limit is through a so-called faithful family of functions. Definition 3 (faithful). Let A = (Q, ∆, I) be a looping automaton on k-ary trees. The family of functions fq : Q → Q for q ∈ Q is faithful w.r.t. A if for all q, q0 , q1 , . . . , qk ∈ Q, – if (q, q1 , . . . , qk ) ∈ ∆, then (q, fq (q1 ), . . . , fq (qk )) ∈ ∆, and – if (q0 , q1 , . . . , qk ) ∈ ∆, then (fq (q0 ), fq (q1 ), . . . , fq (qk )) ∈ ∆. The subautomaton AS = (Q, ∆S , I) of A induced by this family has the transi- tion relation ∆S = {(q, fq (q1 ), . . . , fq (qk )) | (q, q1 , . . . , qk ) ∈ ∆}. Lemma 4 ([1]). Let A be a looping automaton and AS its subautomaton in- duced by a faithful family of functions. A has a run iff AS has a run. The construction that we will present in Section 4 produces automata that are exponential on the size of the input. For such cases, it has been shown that if the automata are m-blocking for some m bounded polynomially on the size of the input (that is, logarithmically on the size of the automaton), then the emptiness test requires only polynomial space. Definition 5 (PSpace on-the-fly construction). Assume that we have a set I of inputs and a construction that yields, for every i ∈ I, an mi -blocking automaton Ai = (Qi , ∆i , Ii ) working on ki -ary trees. This construction is called a PSpace on-the-fly construction if there is a polynomial P such that, for every input i of size n – mi ≤ P (n) and ki ≤ P (n), – every element of Qi is of a size bounded by P (n), and – one can non-deterministically guess in time bounded by P (n) an element of Ii , and, for a state q ∈ Qi , a transition from ∆i with first component q. Theorem 6 ([1]). If the looping automata Ai are obtained from the inputs i ∈ I by a PSpace on-the-fly construction, then the emptiness problem for Ai can be decided in PSpace. In Section 5 we will use this theorem to give PSpace upper bounds on the complexity of reasoning in the logic ALCI L , which we introduce next. 3 The Fuzzy Logic ALCI L For the rest of this paper, L denotes a fixed residuated, complete De Morgan lattice with the t-norm ⊗. The fuzzy description logic ALCI L is a generalization of the crisp DL ALCI that uses the elements of L as truth values, instead of just the Boolean true and false. The syntax of ALCI L is the same as in ALCI: given the sets NC and NR of concept and role names, the set of complex roles is NR ∪ {r− | r ∈ NR }, and ALCI L concepts are built using the syntactic rule C ::= A | C1 u C2 | C1 t C2 | ¬C | ∃s.C | ∀s.C | > | ⊥, where A ∈ NC and s is a complex role. For a complex role s, the inverse of s (denoted by s) is s− if s ∈ NR and r if s = r− . The semantics of this logic is based on interpretation functions that map every concept C to a function specifying the membership degree of every domain element to C. Definition 7 (semantics of ALCI L ). An interpretation is a pair I = (∆I , ·I ) where ∆I is a non-empty (crisp) domain and ·I is a function that assigns to every concept name A and every role name r functions AI : ∆I → L and rI : ∆I × ∆I → L, respectively. The function ·I is extended to ALCI L concepts as follows for every x ∈ ∆I : – >I (x) = 1, ⊥I (x) = 0, – (C u D)I (x) = C I (x) ⊗ DI (x), (C t D)I (x) = C I (x) ⊕ DI (x), – (¬C)I (x) = ∼WC I (x), I – (∃s.C) (x) = y∈∆I sI (x, y) ⊗ C I (y), – (∀s.C)I (x) = y∈∆I sI (x, y) ⇒ C I (y), V where (r− )I (x, y) = rI (y, x) for all x, y ∈ ∆I and r ∈ NR . Notice that, unlike in crisp ALCI, existential and universal quantifiers are not dual to each other, i.e. in general, (¬∃s.C)I (x) = (∀s.¬C)I (x) does not hold. The axioms of this logic also have an associated lattice value, which expresses the degree to which the restriction must be satisfied. Definition 8 (axioms). Terminological axioms are (labeled) concept defini- . tions of the form hA = C, `i or (labeled) general concept inclusions (GCIs) hC v D, `i, where A ∈ NC , C, D are ALCI L concepts, and ` ∈ L. A general TBox is a finite set of GCIs. An acyclic TBox is a finite set of concept definitions such that every concept name occurs at most once in the left- hand side of an axiom, and there is no cyclic dependency between definitions. A TBox is either a general TBox or an acyclic TBox.4 . An interpretation I satisfies the concept definition hA = C, `i if for every x ∈ ∆I , (AI (x) ⇒ C I (x)) ⊗ (C I (x) ⇒ AI (x)) ≥ ` holds. It satisfies the GCI hC v D, `i if for every x ∈ ∆I , C I (x) ⇒ DI (x) ≥ `. I is a model of the TBox T if it satisfies all axioms in T . If T is an acyclic TBox, then all concept names occuring on the left-hand side of some axiom of T are called defined, all others are called primitive. If T is a general TBox, then all concept names appearing in it are primitive. A concept is an atom if it is either a primitive concept name, or it is a quantified concept, i.e. a concept of the form ∃s.C or ∀s.C for some complex role s and concept C. We emphasize here that ALCI is a special case of ALCI L , where the un- derlying lattice contains only the elements 0 and 1, which may be interpreted as false and true, respectively, and the t-norm and t-conorm are just conjunc- tion and disjunction, respectively. Accordingly, one can generalize the reasoning problems for ALCI to the use of other lattices. We will focus on deciding strong `-satisfiability and `-subsumption [8]. Definition 9 (satisfiability, subsumption). Let C, D be ALCI L concepts, T a TBox, and ` ∈ L. C is strongly `-satisfiable w.r.t. T if there is a model I of T and an x ∈ ∆I such that C I (x) ≥ `. C is `-subsumed by D w.r.t. T if every model I of T is also a model of hC v D, `i. In previous work we have shown that satisfiability is undecidable in ALC L [9], and hence also in ALCI L , in general. For this reason, we assume that L is 4 Notice that we do not consider mixed TBoxes. We could allow axioms of the form hA v C, `i in acyclic TBoxes, as long as they do not introduce cyclic dependencies. To avoid overloading the notation, we exclude this case. finite for the rest of this paper. As we will show in the next sections, under this restriction we obtain the same complexity upper bounds for deciding satisfiability and subsumption as in the crisp case; that is, the lattice based semantics do not increase the complexity of the logic. 4 Deciding Strong Satisfiability and Subsumption Recall that the semantics of the quantifiers require the computation of a supre- mum or infimum of the membership degrees of a possibly infinite set of elements of the domain. To obtain an effective decision procedure, one usually restricts reasoning to witnessed models [14]. Definition 10 (witnessed model). Let n ∈ N. A model I of a TBox T is called n-witnessed if for every x ∈ ∆I and every concept of the form ∃r.C there are n elements x1 , . . . , xn ∈ ∆I such that n _ (∃r.C)I (x) = rI (x, xi ) ⊗ C I (xi ), i=1 and analogously for the universal restrictions ∀r.C. In particular, if n = 1, then the suprema and infima from the semantics of ∃r.C and ∀r.C become maxima and minima, respectively. In this case, we simply say that I is witnessed. We can restrict reasoning to n-witnessed models w.l.o.g.: since L is finite, we always have the n-witnessed model property for some n ∈ N. Lemma 11. If the cardinality of the largest antichain of L is n, then ALCI L has the n-witnessed model property. To simplify the description of the algorithm, in the following we consider n = 1. The algorithm and the proofs of correctness can easily be adapted for any other n ∈ N. Our algorithm for deciding satisfiability and subsumption of concepts exploits the fact that a TBox T has a model iff it has a well-structured tree model, called a Hintikka tree. Intuitively, Hintikka trees are abstract representations of models that explicitly express the membership value of all “relevant” concepts. We will construct automata that have exactly these Hintikka trees as their runs, and use the initial states to verify that an element in the model verifies the satisfiability or violates the subsumption condition, respectively. Reasoning is hence reduced to the emptiness test of these automata. We denote by sub(C, T ) the set of all subconcepts of C and of the concepts . A, E, and F for all axioms hE v F, `i or hA = F, `i in T . The nodes of the Hintikka trees are labeled with so-called Hintikka functions over the domain sub(C, T ) ∪ {ρ}, where ρ is an arbitrary new element, which will be used to express the degree with which the role relation to the parent node holds. Definition 12 (Hintikka function). A Hintikka function for C, T is a partial function H : sub(C, T ) ∪ {ρ} → L such that: (i) H is defined for ρ and for all atoms, (ii) if H(D u E) is defined, then H(D) and H(E) are also defined and it holds that H(D u E) = H(D) ⊗ H(E), (iii) if H(D t E) is defined, then H(D) and H(E) are also defined and it holds that H(D t E) = H(D) ⊕ H(E), (iv) if H(¬D) is defined, then H(D) is defined and H(¬D) = ∼ H(D). . It is compatible with the concept definition hA = E, `i if, whenever H(A) is defined, then H(E) is defined and (H(A) ⇒ H(E)) ⊗ (H(E) ⇒ H(A)) ≥ `.5 It is compatible with the GCI hE v F, `i if H(E) and H(F ) are always defined and H(E) ⇒ H(F ) ≥ ` holds. The Hintikka trees have a fixed arity k determined by the number of existen- tial and universal restrictions, i.e. concepts of the form ∃s.F or ∀s.F , contained in sub(C, T ). Intuitively, each successor will act as the witness for one of these restrictions. Since we need to know which successor in the tree corresponds to which restriction, we fix an arbitrary bijection ϕ : {E | E ∈ sub(C, T ) is of the form ∃s.F or ∀s.F } → K. Definition 13 (Hintikka condition). The tuple (H0 , H1 , . . . , Hk ) of Hintikka functions for C, T satisfies the Hintikka condition if: (i) For every existential restriction ∃s.G ∈ sub(C, T ) – Hϕ(∃s.G) (G) is defined and H0 (∃s.G) = Hϕ(∃s.G) (ρ)⊗Hϕ(∃s.G) (G), and – Hϕ(E) (G) is defined and H0 (∃s.G) ≥ Hϕ(E) (ρ) ⊗ Hϕ(E) (G) for every restriction E ∈ sub(C, T ) of the form ∃s.F or ∀s.F . (ii) For every universal restriction ∀s.G ∈ sub(C, T ) – Hϕ(∀s.G) (G) is defined and H0 (∀s.G) = Hϕ(∀s.G) (ρ) ⇒ Hϕ(∀s.G) (G), – Hϕ(E) (G) is defined and H0 (∀s.G) ≤ Hϕ(E) (ρ) ⇒ Hϕ(E) (G) for every restriction E ∈ sub(C, T ) of the form ∃s.F or ∀s.F . (iii) For every existential restriction ∃s.G ∈ sub(C, T ) and every restriction E ∈ sub(C, T ) of the form ∃s.F or ∀s.F , H0 (G) is defined and Hϕ(E) (∃s.G) ≥ Hϕ(E) (ρ) ⊗ H0 (G). (iv) For every universal restriction ∀s.G ∈ sub(C, T ) and every restriction E ∈ sub(C, T ) of the form ∃s.F or ∀s.F , H0 (G) is defined and Hϕ(E) (∀s.G) ≤ Hϕ(E) (ρ) ⇒ H0 (G). The tuple is compatible with the axiom t if the Hintikka functions H0 , . . . , Hk are compatible with t. Condition (i) makes sure that an existential restriction ∃s.G is witnessed by its designated successor ϕ(∃s.G) and all other s-successors do not contradict the witness. Condition (iii) deals with inverse roles, ensuring that the s-restrictions are propagated backwards through the s-relation. Conditions (ii) and (iv) treat the universal restrictions analogously. 5 This method, called lazy unfolding, is only correct for acyclic TBoxes. A Hintikka tree for C, T is an infinite k-ary tree T labeled with compat- ible Hintikka functions for C, T such that T(ε)(C) is defined and the tuple (T(u), T(u1), . . . , T(uk)) satisfies the Hintikka condition for every node u ∈ K ∗ . The definition of compatibility ensures that all axioms are satisfied at any node of the Hintikka tree, while the Hintikka condition makes sure that the tree is in fact a witnessed model. The proof of the following theorem uses arguments similar to those in [1]. The main difference is the presence of successors witnessing the universal restrictions. Theorem 14. Let C be an ALCI L concept, T a TBox, and ` ∈ L. Then C is strongly `-satisfiable w.r.t. T (in a witnessed model) iff there is a Hintikka tree T for C, T such that T(ε)(C) ≥ `. Proof (Sketch). Every witnessed model I of T with a domain element x ∈ ∆I for which C I (x) ≥ ` holds can be unraveled into a Hintikka tree T for C, T as follows. We start by labeling the root node by the (total) Hintikka function that records the membership values of x for each concept from sub(C, T ). We then create successors of the root by considering every E ∈ sub(C, T ) of the form ∃s.F or ∀s.F and finding the witness y ∈ ∆I for this restriction. We create a new node for y which is the ϕ(E)-th successor of the root node and is labeled by a Hintikka set H with H(ρ) = sI (x, y). The fact that I is a model of T ensures that these successors satisfy the Hintikka condition. By continuing this process, we construct a Hintikka tree T for C, T for which T(ε)(C) ≥ ` holds. Conversely, we show that a Hintikka tree can be seen as a witnessed model with domain K ∗ and interpretation function given by the Hintikka functions. Notice that from the partial function labeling each node we can obtain a valua- tion for each concept name that satisfies all the axioms in T . Indeed, if T is a general TBox, then every concept name is primitive, and hence the valuation is already defined. The fact that the Hintikka function is compatible with all the axioms in T implies that every node satisfies the TBox. On the other hand, if T is an acyclic TBox, and H is undefined for some concept names, then consider . an axiom hA = C, `i for which H(A) is undefined, but H(B) is defined for every atom appearing in C. The acyclicity of T ensures that such an axiom always exists. Thus, we can compute a value for H(C) that still satisfies the conditions of Definition 12. If we set H(A) := H(C), then H is still compatible with T . By an induction argument, we can define a compatible total Hintikka function, and thus a valuation for every concept name that satisfies T . For this valuation to be an interpretation, it only remains to be shown that the semantics of the existential and universal restrictions are satisfied. This is ensured by the Hintikka condition. The choice of the successors also ensures that the interpretation is witnessed. As explained above, it is compatible, and hence also a model of T . Thus, if there is a Hintikka tree T for C, T with T(ε)(C) ≥ `, then C is strongly `-satisfiable w.r.t. T . t u Hintikka trees can also be used for deciding (non-)subsumption between ALCI L concepts. The proof of the following theorem is analogous to the one of Theorem 14. Theorem 15. Let C, D be ALCI L concepts, T a TBox, and ` ∈ L. Then C is not `-subsumed by D (in a witnessed model) iff there is a Hintikka tree T for C u D, T such that T(ε)(C) ⇒ T(ε)(D)  `.6 Notice that this does not yield a reduction from subsumption to satisfiability, since the residuum ⇒ cannot in general be expressed using only the t-norm, t- conorm and negation, and in Theorem 14 the value of C at the root is restricted to a value greater or equal to `, while Theorem 15 negates this restriction. From the last two theorems it follows that satisfiability and subsumption of ALCI L concepts can be reduced to deciding the existence of a Hintikka tree with additional restrictions in the root. By building looping automata whose runs correspond exactly to those Hintikka trees, we reduce ALCI L reasoning to the emptiness problem of these automata. For the following, we focus only on deciding satisfiability and explain the minor modifications required for deciding subsumption. Definition 16 (Hintikka automaton). Let C be an ALCI L concept, T a TBox, and ` ∈ L. The Hintikka automaton for C, T , ` is AC,T ,` = (Q, I, ∆), where Q is the set of all compatible Hintikka functions for C, T , I contains all Hintikka functions H with H(C) ≥ `, and ∆ is the set of all (k + 1)-tuples of Hintikka functions that satisfy the Hintikka condition. The runs of AC,T ,` are exactly the Hintikka trees T having T(ε)(C) ≥ `. Thus, C is strongly `-satisfiable w.r.t. T iff AC,T ,` is not empty. To obtain an automaton deciding `-subsumption between C and D, one needs only modify the set of initial states I to contain all Hintikka functions H with H(C) ⇒ H(D) 6≥ `. In that case, we have that C is `-subsumed by D iff the automaton is empty. The size of the automaton AC,T ,` is exponential in the input C, T . Hence, we have an ExpTime algorithm for this logic. For general TBoxes, this gives a tight upper bound for the complexity of satisfiability and subsumption, since these problems are already ExpTime-hard for crisp ALC [16]. Theorem 17. Deciding strong satisfiability and subsumption in ALCI L w.r.t. general TBoxes is ExpTime-complete. 5 PSpace Results for Acyclic TBoxes If one restricts to acyclic TBoxes, then the upper bound obtained by the empti- ness test of the automaton from Definition 16 does not match the PSpace lower bound given by crisp ALCI with acyclic TBoxes. We will now improve this upper bound and show that satisfiability and subsumption of ALCI L concepts w.r.t. acyclic TBoxes are also PSpace-complete problems. The idea is to modify the construction of the Hintikka automata into a PSpace on-the-fly construction. Notice that AC,T ,` satisfies all but one of the 6 Using C u D only ensures that T(ε)(C) and T(ε)(D) are defined, but imposes no further restriction on their values. conditions from Definition 5: (i) the arity of the automata is given by the number of existential and universal concepts in sub(C, T ); (ii) every Hintikka function has size bounded by |sub(C, T )|; (iii) building a state or a transition of the automaton requires only guessing values for all concepts in sub(C, T ) and then verifying that this is indeed a valid state or transition, which can be done in time polynomial in |sub(C, T )|. However, it is easy to build runs of the automata con- structed by this reduction where blocking occurs only after exponentially many transitions, violating the first condition of PSpace on-the-fly constructions. We will use a faithful family of functions to obtain a reduced automaton that guarantees blocking after at most polynomially many transitions, thus obtaining the PSpace upper bound. The idea is that it suffices to consider only transitions that reduce the maximal role depth (w.r.t. T ) in the support of the states. The role depth w.r.t. T (rdT ) of ALCI L concepts is recursively defined as follows: rdT (A) = rdT (>) = rdT (⊥) = 0 for every primitive concept name A; rdT (C u D) = rdT (C t D) = max{rdT (C), rdT (D)}; rdT (¬C) = rdT (C); rdT (∃r.C) = rdT (∀r.C) = rdT (C) + 1; and rdT (A) = rdT (C) for every definition . hA = C, `i ∈ T . For a Hintikka function H for C, T , we denote as support(H) the set of all concepts in sub(C, T ) such that H(C) is defined and H(C) > 0. We define rdT (H) as the maximum rdT (D) such that D ∈ support(H). Definition 18 (functions fH ). Let H and H 0 be two states of AC,T ,` with rdT (H) = n. The function fH (H 0 ) is given by:  0  if D is an atom and rdT (D) ≥ n 0 0 fH (H )(D) = H (D) if rdT (D) < n  undefined otherwise.  ( 0 if support(H) = ∅ fH (H 0 )(ρ) = 0 H (ρ) otherwise. Since T is acyclic, the function fH (H 0 ) defined above is still a Hintikka function for C, T compatible with all the axioms in T . Lemma 19. The family of mappings fH for states H of AC,T ,` from Defini- tion 18 is faithful w.r.t. AC,T ,` . Proof. Let (H, H1 , . . . , Hk ) be a valid transition of AC,T ,` . We need to show that (H, fH (H1 ), . . . , fH (Hk )) is also a transition, i.e. that it satisfies the Hin- tikka condition. We show in detail only the proof for the restriction (i) from Definition 13, as the others can be treated analogously. For ∃s.G ∈ sub(C, T ), the value Hϕ(E) (G) is defined for all restrictions E of the form ∃s.F or ∀s.F in sub(C, T ). If rdT (∃s.G) > rdT (H), then H(∃s.G) = 0, and all the values fH (Hϕ(E) )(G) are 0. Thus, the inequalities are trivially satis- fied. Otherwise, rdT (G) < rdT (∃s.G) ≤ rdT (H), and thus the values Hϕ(E) (G) are not changed by applying fH . If the values Hϕ(E) (ρ) are also left unchanged, all inequalities remain satisfied. Otherwise, H(∃s.G) = 0, and all the values fH (Hϕ(E) )(ρ) are 0. Thus, the inequalities are again trivially satisfied. t u By Lemma 4, AC,T ,` is empty iff the induced subautomaton ASC,T ,` is empty. Theorem 20. The construction of ASC,T ,` from an ALCI L concept C, ` ∈ L, and an acyclic TBox T is a PSpace on-the-fly construction. Proof. As described before, we only need to show that the automata ASC,T ,` are m-blocking for some m bounded polynomially in |sub(C, T )|. We show that this holds for m = max{rdT (D) | D ∈ sub(C, T )} + 2. By definition of ASC,T ,` , every transition decreases the maximal role depth of the support of the state. Hence, after at most max{rdT (D) | D ∈ sub(C, T )} transitions, we reach a state H, where H(D) = 0 if D is an atom and undefined otherwise, and hence, support(H) = ∅. From the next transition on, all the states additionally satisfy that H(ρ) = 0. Hence, after at most m transitions, we find two states that are equal. Since m ≤ |sub(C, T )| + 2, ASC,T ,` satisfies the requirements for a PSpace on-the-fly construction. t u This shows that emptiness of ASC,T ,` and hence also of AC,T ,` is in PSpace. This yields the desired PSpace upper bound for satisfiability and similar argu- ments can be made for subsumption. PSpace-hardness follows from PSpace- hardness of satisfiability and subsumption w.r.t. the empty TBox in ALC [17]. Theorem 21. Deciding strong satisfiability and subsumption in ALCI L w.r.t. acyclic TBoxes is PSpace-complete. Notice that the definitions of Hintikka functions and Hintikka trees are in- dependent of the operators used. One could have chosen the residual negation ` := ` ⇒ 0 to interpret the constructor ¬, or the Kleene-Dienes implication `1 ⇒ `2 := ∼ `1 ∨ `2 instead of the residuum. The only restrictions are that the semantics must be truth functional, i.e. the value of a formula must depend only on the values of its direct subformulas, and the underlying operators must be computable. We could also use the traditional semantics for concept definitions in which ⊗ is replaced by the simple meet t-norm ∧. We also point out that the algorithm can be modified for reasoning w.r.t. n-witnessed models for n > 1. One needs only extend the arity of the Hintikka trees to account for n witnesses for each quantified formula in sub(C, T ); the arity of AC,T ,` grows polynomially in n. This does not affect the complexity upper bounds from the automata, and hence Theorems 17 and 21 still hold. 6 Conclusions We have shown that reasoning in ALCI L is not harder than in the underlying crisp DL ALCI. More precisely, strong `-satisfiability and `-subsumption can be decided in ExpTime for general TBoxes and in PSpace for acyclic TBoxes. This extends the complexity results from [8–10] and demonstrates that automata can show PSpace results even for fuzzy description logics, as in the crisp case [1]. This paper provides a small step towards reasoning services for fuzzy general- izations of the current standard ontology languages, like SROIQ(D). In the future, we want to study the influence of additional DL constructors and axioms on the complexity of the reasoning tasks. In particular, transitive roles, which are covered by the results in [1], have not been considered in this paper. Although in the crisp case they do not increase the complexity of checking satisfiability, it is not straightforward to generalize the methods used to show this to residuated De Morgan lattices. Satisfiability w.r.t. general TBoxes and residuated total orders has been shown to be undecidable [9], but it remains open to find subclasses of infinite lattices and t-norms for which the problem is decidable. Over the unit inter- val, the product and Lukasiewicz t-norms cause undecidability w.r.t. witnessed models [3, 11]; for arbitrary models decidability is unknown in these cases. References 1. F. Baader, J. Hladik, and R. Peñaloza. Automata can show PSPACE results for description logics. Inform. Comput., 206(9-10):1045–1056, 2008. 2. F. Baader and R. Peñaloza. Are fuzzy description logics with general concept inclusion axioms decidable? In Proc. FuzzIEEE’11, pages 1735–1742. IEEE, 2011. 3. F. Baader and R. Peñaloza. On the undecidability of fuzzy description logics with GCIs and product t-norm. In Proc. FroCoS’11, pages 55–70. Springer-Verlag, 2011. 4. F. Bobillo, F. Bou, and U. Straccia. On the failure of the finite model property in some fuzzy description logics. Fuzzy Set. Syst., 172(1):1–12, 2011. 5. F. Bobillo and U. Straccia. A fuzzy description logic with product t-norm. In Proc. Fuzz-IEEE’07, pages 1–6. IEEE, 2007. 6. F. Bobillo and U. Straccia. Fuzzy description logics with general t-norms and datatypes. Fuzzy Set. Syst., 160(23):3382–3402, 2009. 7. F. Bobillo and U. Straccia. Reasoning with the finitely many-valued Lukasiewicz fuzzy description logic SROIQ. Inf. Sci., 181(4):758–778, 2011. 8. S. Borgwardt and R. Peñaloza. Description logics over lattices with multi-valued ontologies. In Proc. IJCAI’11, pages 768–773. AAAI Press, 2011. 9. S. Borgwardt and R. Peñaloza. Fuzzy ontologies over lattices with t-norms. In Proc. DL’11, pages 70–80. CEUR Workshop Proceedings, 2011. 10. F. Bou, M. Cerami, and F. Esteva. Finite-valued Lukasiewicz modal logic is PSPACE-complete. In Proc. IJCAI’11, pages 774–779. AAAI Press, 2011. 11. M. Cerami and U. Straccia. On the undecidability of fuzzy description logics with GCIs with Lukasiewicz t-norm. 2011. arXiv:1107.4212v3 [cs.LO]. 12. G. De Cooman and E. E. Kerre. Order norms on bounded partially ordered sets. J. Fuzzy Math, 2:281–310, 1993. 13. G. Grätzer. General Lattice Theory, Second Edition. Birkhäuser Verlag, 2003. 14. P. Hájek. Making fuzzy description logic more general. FSS, 154(1):1–15, 2005. 15. T. Lukasiewicz and U. Straccia. Managing uncertainty and vagueness in description logics for the semantic web. J. Web Semant., 6(4):291–308, 2008. 16. K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. IJCAI’91, pages 466–471. Morgan Kaufmann, 1991. 17. M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with comple- ments. Artif. Intell., 48(1):1–26, 1991. 18. U. Straccia. Description logics over lattices. Int. J. Unc. Fuzz., 14(1):1–16, 2006. 19. M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci., 32(2):183–221, 1986.