Fuzzy DLs over Finite Lattices with Nominals? Stefan Borgwardt Theoretical Computer Science, TU Dresden, Germany stefborg@tcs.inf.tu-dresden.de Abstract. The complexity of reasoning in fuzzy description logics (DLs) over a finite lattice L usually does not exceed that of the underlying clas- sical DLs. This has recently been shown for the logics between L-IALC and L-ISCHI using a combination of automata- and tableau-based tech- niques. In this paper, this approach is modified to deal with nominals and constants in L-ISCHOI. Reasoning w.r.t. general TBoxes is ExpTime- complete, and PSpace-completeness is shown under the restriction to acyclic terminologies in two sublogics. The latter implies two previously unknown complexity results for the classical DLs ALCHO and SO. 1 Introduction Fuzzy extensions of DLs have first been studied in [28,32,34] to model concepts that do not have a precise meaning. Such concepts occur in many application domains. For example, a physician may base a diagnosis on the patient having a high fever, which is not clearly characterized even by the precise body tem- perature. The main idea behind fuzzy DLs is that concepts are not interpreted as sets, but rather as fuzzy sets, which assign a membership degree from [0, 1] to each domain element. As a fuzzy concept, HighFever could assign degree 0.7 to a patient with a body temperature of 38 ◦ C, and 0.9 when the body temperature is 39 ◦ C. The first fuzzy DLs were based on the so-called Zadeh semantics that is de- rived from fuzzy set theory [35]. Later, it was proposed [19] to consider fuzzy DLs from the point of view of Mathematical Fuzzy Logic [18] and t-norm-based se- mantics were introduced. A t-norm is a binary operator on [0, 1] that determines how the conjunction of two fuzzy statements is evaluated. Unfortunately, it was shown that many t-norm-based fuzzy DLs allowing general TBoxes have unde- cidable consistency problems [3,12,16]. This can be avoided by either choosing a t-norm that allows the consistency problem to be trivially reduced to classi- cal reasoning [10], restricting to acyclic TBoxes [5], or taking the truth values from a finite structure, usually a total order [7,8,29] or a lattice [11,13,24,30]. Recently, it was shown that the complexity of reasoning in fuzzy DLs over finite lattices with (generalized) t-norms often matches that of the underlying classical DLs [13,14]. ? Partially supported by the DFG under grant BA 1122/17-1 and in the research training group 1763 (QuantLA) In this paper, we analyze the complexity of fuzzy extensions of SHOI using a finite lattice L. In the classical case, deciding consistency of ontologies with gen- eral TBoxes is ExpTime-complete in all logics between ALC and SHOI [20,26], and we show that this also holds for L-ISCHOI. The additional letters I and C in the name of the logic denote the presence of the constructors for implication and involutive negation, respectively. This nomenclature was introduced to make the subtle differences between different fuzzy DLs more explicit [12,15]. As all fuzzy DLs considered in this paper have both I and C, it is safe to ignore these letters here and simply read L-SHOI instead of L-ISCHOI. Consistency remains ExpTime-complete in the classical DLs ALCOI and SH even w.r.t. the empty TBox [22,31]. However, when restricting to acyclic (or empty) TBoxes in SI, it is only PSpace-complete [1,23]. Similar results have been shown before under finite lattice semantics in L-IALCHI and L-ISCI c [13]. The latter restricts all roles to be crisp, i.e. they are allowed to take only the two classical truth values. Here, we extend these results to L-IALCHO and L-ISCOc , which also shows previously unknown complexity results for the classical DLs ALCHO and SO with acyclic TBoxes. Due to space constraints, all proofs can be found only in the accompanying technical report [9]. 2 Preliminaries We first introduce looping automata on infinite trees and several helpful notions from [1], which will be used later for our reasoning procedures. Afterwards, we briefly recall relevant definitions from lattice theory [17]. 2.1 Looping Automata We consider automata on the (unlabeled ) infinite tree of fixed arity k ∈ N, represented by the set K ∗ of its nodes, where K abbreviates {1, . . . k}. Here, ε represents the root node, and ui, i ∈ K, is the i-th successor of the node u ∈ K ∗ . A path in this tree is a sequence u1 , . . . , um of nodes such that u1 = ε and, for every i, 1 ≤ i ≤ m − 1, ui+1 is a successor of ui . Definition 1 (looping automaton). A looping (tree) automaton is a tuple A = (Q, I, ∆) where Q is a finite set of states, I ⊆ Q is a set of initial states, and ∆ ⊆ Qk+1 is the transition relation. A run of A is a mapping r : K ∗ → Q such that r(ε) ∈ I and (r(u), r(u1), . . . , r(uk)) ∈ ∆ for every u ∈ K ∗ . The emptiness problem is to decide whether a given looping automaton has a run. The emptiness problem for such automata is decidable in polynomial time [33]. However, the automata we construct in Section 4 are exponential in the size of the input. In order to obtain PSpace decision procedures, we need to identify the length of the longest possible path in a run that does not repeat any states. Definition 2 (invariant, blocking). Let A = (Q, I, ∆) be a looping automaton and  a binary relation over Q, called the blocking relation. A is -invariant if (q0 , q1 , . . . , qi , . . . , qk ) ∈ ∆ and qi  qi0 always imply (q0 , q1 , . . . , qi0 , . . . , qk ) ∈ ∆. If this is the case, then A is m-blocking for m ∈ N if in every path u1 , . . . , um of length m in a run r of A there are two indices 1 ≤ i < j ≤ m with r(uj )  r(ui ). The notion of blocking is similar to that used in tableau algorithms for DLs [4,23]. If q is blocked by its ancestor q 0 (q  q 0 ), then we do not need to consider the subtree below q since every transition involving q can be replaced by one using q 0 instead. Of course, every looping automaton is =-invariant and |Q|- blocking. However, as mentioned above the size of Q may already be exponential in some external parameter. To obtain m-blocking automata with m bounded polynomially in the size of the input, we can use a faithful family of functions to prune the transition relation. Definition 3 (faithful). Let A = (Q, I, ∆) be a looping automaton. A family f = (fq )q∈Q of functions fq : Q → Q is called faithful (w.r.t. A) if – for all (q, q1 , . . . , qk ) ∈ ∆, we have (q, fq (q1 ), . . . , fq (qk )) ∈ ∆, and – for all (q0 , q1 , . . . , qk ) ∈ ∆, we have (fq (q0 ), fq (q1 ), . . . , fq (qk )) ∈ ∆. The subautomaton Af := (Q, I, ∆f ) induced by f is defined by ∆f := {(q, fq (q1 ), . . . , fq (qk )) | (q, q1 , . . . , qk ) ∈ ∆}. The name faithful reflects the fact that the resulting subautomaton simulates all runs of A. The following connection between the two automata was shown in [1]. Proposition 4. Let A be a looping automaton and f be a faithful family of func- tions for A. Then A has a run iff Af has a run. Together with the following additional assumptions, polynomial blocking allows us to test emptiness in polynomial space. Definition 5 (PSpace on-the-fly construction). Let I be a set of inputs. A construction that yields, for each i ∈ I, an mi -blocking looping automaton Ai over ki -ary trees is called a PSpace on-the-fly construction if there is a polynomial P such that, for every input i of size n, (i) mi ≤ P (n) and ki ≤ P (n), (ii) the size of every state of Ai is bounded by P (n), and (iii) one can guess in time bounded by P (n) an initial state, and, given a state q, a transition (q, q1 , . . . , qk ) of Ai . The following result is again taken from [1]. Proposition 6. If the looping automata Ai are obtained by a PSpace on-the-fly construction, then emptiness of Ai can be decided in PSpace in the size of i. 2.2 Residuated Lattices A lattice is an algebraic structure (L, ∨, ∧) with two commutative, associative, and idempotent binary operators, called supremum (∨) and infimum (∧), that satisfy x ∧ (x ∨ y) = x and x ∨ (x ∧ y) = x for all x, y ∈ L. The natural partial order on L is given by x ≤ y iff x ∧ y = x for all x, y ∈ L. An antichain is a set S ⊆ L of incomparable elements. The width of a lattice is the maximal cardinality of all its antichains. A lattice L is complete if W suprema andVinfima of arbitrary subsets S ⊆ L exist; these are denoted by x∈S x and x∈S x, respectively. It is distributive if ∧ and ∨ distribute over each other, finite if L is finite, and bounded if it has a least element 0 and a greatest element 1.VEvery W is complete, and every complete lattice is bounded by 0 := x∈L x finite lattice and 1 := x∈L x. A De Morgan lattice is a distributive lattice L with a unary involutive operator ∼ on L satisfying the De Morgan laws ∼(x ∨ y) = ∼x ∧ ∼y and ∼(x ∧ y) = ∼x ∨ ∼y for all x, y ∈ L. Such an operator is always antitone and satisfies ∼0 = 1. A t-norm over a bounded lattice L is a commutative, as- sociative, monotone binary operator ⊗ on L that has 1 as its unit. A residuated lattice is a bounded lattice L with a t-norm ⊗ and a residuum ⇒ : L × L → L satisfying (x ⊗ y) ≤ z iff y ≤ (x ⇒ z) y, z ∈ L. We always assume that  x, W W for all ⊗ is join-preserving, that is, x ⊗ y∈S y = y∈S (x ⊗ y) holds for all x ∈ L and S ⊆ L. This is a natural assumption that corresponds to the left-continuity assumption for t-norms over the standard fuzzy interval [0, 1] [18]. 3 L-ISCHOI Since fuzzy DLs over infinite lattices easily become undecidable when dealing with GCIs [3,12,14,16], we now fix a finite residuated De Morgan lattice L. For the complexity analysis, we assume that L is given as a list of its elements and that all lattice operations are computable in polynomial time.1 The syntax of the fuzzy description logic L-ISCHOI is similar to that of classical SHOI: complex roles and concepts are constructed from disjoint sets NC of concept names, NR of role names, and NI of individual names. Definition 7 (syntax). The set N− R of (complex) roles is {r, r − | r ∈ NR }. The set of (complex) concepts is constructed as follows: – every concept name is a concept, and – for concepts C, D, r ∈ N− R , a ∈ NI , and p ∈ L, the following are also concepts: p (constant), {a} (nominal), ¬C (negation), C u D (conjunction), C → D (implication), ∃r.C (existential restriction), and ∀r.C (value restriction). For a complex role s, the inverse of s (written s) is s− if s ∈ NR and r if s = r− . 1 If instead the size of the input encoding of L is logarithmic in the cardinality of L, then all complexity results except Theorem 18 remain valid. Definition 8 (semantics). A (fuzzy) interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I and an interpretation function ·I that assigns to every A ∈ NC a fuzzy set AI : ∆I → L, to every r ∈ NR a fuzzy binary relation rI : ∆I × ∆I → L, and to every a ∈ NI a domain element aI ∈ ∆I . This function is extended to complex roles and concepts as follows for all x, y ∈ ∆I : – (r− )I (x, y) := rI (y, x); – pI (x) := p; – {a}I (x) := 1 if x = aI , and {a}I (x) := 0 otherwise; – (¬C)I (x) := ∼C I (x); – (C u D)I (x) := C I (x) ⊗ DI (x); – (C → D)I (x) := I I W C (x) ⇒ D (x); – (∃r.C)I (x) := y∈∆I rI (x, y) ⊗ C I (y); and – (∀r.C)I (x) := y∈∆I rI (x, y) ⇒ C I (y). V One can express fuzzy nominals [6] of the form {p1 /a1 , . . . , pn /an } with pi ∈ L and ai ∈ NI , 1 ≤ i ≤ n, by ({a1 }up1 )t· · ·t({an }upn ), where C tD abbreviates ¬(¬C u ¬D). Unlike in classical DLs, existential and value restrictions need not be dual to each other, i.e. in general we have (¬∃r.C)I 6= (∀r.¬C)I . Definition 9 (ontology). An axiom α is a concept assertion ha:C ./ pi, a con- . cept definition hA = C ≥ pi, a general concept inclusion (GCI) hC v D ≥ pi, a role inclusion hr v si, or a transitivity axiom trans(r), where C, D are concepts, r, s ∈ N−R , a ∈ NI , A ∈ NC , p ∈ L, and ./ ∈ {<, ≤, =, ≥, >}. An interpreta- tion I satisfies α if C I (aI ) ./ p, (AI (x) ⇒ C I (x)) ⊗ (C I (x) ⇒ AI (x)) ≥ p, C I (x) ⇒ DI (x) ≥ p, rI (x, y) ≤ sI (x, y), or rI (x, y) ⊗ rI (y, z) ≤ rI (x, z), respectively, hold for all x, y, z ∈ ∆I . An acyclic TBox is a finite set T of concept definitions where every A ∈ NC . has at most one definition hA = C ≥ pi in T and the relation >T on NC is acyclic, where A >T B iff B occurs in the definition of A. A general TBox is a finite set of GCIs, an ABox a finite set of concept assertions, and an RBox a finite set of role inclusions and transitivity axioms. An ontology is a triple (A, T , R) consisting of an ABox A, an (acyclic or general) TBox T , and an RBox R. An interpretation is a model of this ontology if it satisfies all its axioms. We denote by NI (O) and NR (O) the sets of individual names and role names, respectively, occurring in an ontology O, and set N− − R (O) := {r, r | r ∈ NR (O)}. As usual, for an ontology O = (A, T , R) we define the role hierarchy vR as the reflexive transitive closure of {(r, s) ∈ N−R (O) | r vR s ∈ R or r vR s ∈ R}, and we call a role r transitive if either trans(r) ∈ R or trans(r) ∈ R. We do not consider role assertions of the form h(a, b):r ./ pi since in the pres- ence of nominals they can be simulated by concept assertions, e.g. ha:∃r.{b} ./ pi. The reasoning problem we consider in this paper is consistency, i.e. deciding the existence of a model for a given ontology. Due to the expressivity of our asser- tions, other reasoning problems such as satisfiability, subsumption, and instance checking can be reduced to consistency in linear time. For example, a concept C is p-subsumed by D w.r.t. O = (A, T , R), i.e. we have C I (x) ⇒ DI (x) ≥ p for all models I of O and all x ∈ ∆I , iff (A ∪ {ha:C → D < pi}, T , R) is inconsistent, where a is a fresh individual name. 4 Deciding Consistency Consistency in L-ISCHOI with general TBoxes is ExpTime-complete, matching the complexity of classical SHOI [20]. To show this, we adapt the automata- based procedures from [1,13] to this more expressive logic. The conditions for the role hierarchy, inverse roles, and transitive roles are similar to the tableaux rules from [23]. To deal with nominals, we employ pre-completions inspired by the approaches in [2,14,21]. In Section 5, we derive complexity results for consistency in the sublogics L-IALCHO (without transitivity and inverse roles) and L-ISCOc (without role inclusions, inverse roles, and fuzzy roles) with acyclic TBoxes. It was shown in [13] that over a finite lattice L every interpretation I is n-witnessed, where n is the width of the lattice. This means that for every concept C, r ∈WN− I I R , and x ∈ ∆ there are n witnesses y1 , . . . , yn ∈ ∆ such that I n I I (∃r.C) (x) = i=1 r (x, yi )⊗C (yi ), and similarly for the value restrictions. For the sake of simplicity, we present the following reasoning procedure only for the case of n = 1, i.e. we assume that all interpretations are (1-)witnessed. It can be generalized to handle arbitrary n by easy adaptations of the following definitions, in particular the introduction of more than one witness in Definition 12. We now consider an ontology O = (A, T , R) that we want to test for con- sistency. The main idea of the algorithm is to find an abstract representation of a tree-shaped model of O, a so-called Hintikka tree. Every node of this tree consists of a Hintikka function that describes the values of all relevant concepts for one domain element of the model. Additionally, each Hintikka function stores the values of all role connections from the parent node. We define the set sub(O) to contain all subconcepts of concepts occurring in O, together with all ∃s.C (and ∀s.C) for which ∃r.C (∀r.C) occurs in O, s vR r, and s is transitive. Definition 10 (Hintikka function). A Hintikka function for O is a partial function H : sub(O) ∪ N− R (O) → L satisfying the following conditions: – H(s) is defined for all s ∈ N− R (O); – if H(p) is defined, then H(p) = p; – if H({a}) is defined, then H({a}) ∈ {0, 1}; – if H(C u D) is defined, then H(C) and H(D) are also defined and it holds that H(C u D) = H(C) ⊗ H(D); and similarly for ¬C and C → D. This function is compatible with – an assertion ha:C ./ `i if, whenever H({a}) = 1, then H(C) is defined and H(C) ./ `. . – a concept definition hA = C ≥ `i if, whenever H(A) is defined, then H(C) is defined and (H(A) ⇒ H(C)) ⊗ (H(C) ⇒ H(A)) ≥ `. – a GCI hC v D ≥ `i if H(C) and H(D) are defined and H(C) ⇒ H(D) ≥ `. – a role inclusion r v s if H(r) ≤ H(s). – an ABox/TBox/RBox/ontology if it is compatible with all axioms in it. The support of H is the set supp(H) of all C ∈ sub(O) for which H is defined, and Ind(H) is the set of all a ∈ NI (O) for which H({a}) = 1. To deal with nominals, our algorithm maintains a polynomial amount of global information about the named domain elements, called a pre-completion. Since one domain element can have several names, we first consider a partition of NI (O) that specifies which names are interpreted by the same elements. The pre- completion further contains one Hintikka function for each named individual, and the values of all role connections between them. Definition 11 (pre-completion). A pre-completion for the ontology O is a triple P = (P, HP , RP ), where P is a partition of NI (O), HP = (HX )X∈P is a family of Hintikka functions for O, and RP = (rP )r∈NR (O) is a family of fuzzy binary relations rP : P ×P → L, such that, for all X ∈ P, we have Ind(HX ) = X and HX is compatible with O. A Hintikka function H for O is compatible with P if for all a ∈ Ind(H), we have H|sub(O) = H[a]P |sub(O) . − We further set rP (X, Y ) := rP (Y, X) for all X, Y ∈ P and r ∈ NR (O). The arity k of our Hintikka trees is the number of existential and value restrictions in sub(O). Each successor in the tree describes the witness for one restriction. For the following definition, we consider K := {1, . . . , k} as before and fix a bijection ϕ : {C | C ∈ sub(O) is of the form ∃r.D or ∀r.D} → K. Definition 12 (Hintikka condition). The tuple (H0 , H1 , . . . , Hk ) of Hintikka functions for O satisfies the Hintikka condition if the following hold: a) For every existential restriction ∃r.C ∈ sub(O): – If ∃r.C ∈ supp(H0 ) and i = ϕ(∃r.C), then we have C ∈ supp(Hi ) and H0 (∃r.C) = Hi (r) ⊗ Hi (C). – If ∃r.C ∈ supp(H0 ), then for all i ∈ K, we have C ∈ supp(Hi ) and H0 (∃r.C) ≥ Hi (r) ⊗ Hi (C); moreover, for all transitive roles s vR r, we have ∃s.C ∈ supp(Hi ) and H0 (∃r.C) ≥ Hi (s) ⊗ Hi (∃s.C). – For all i ∈ K with ∃r.C ∈ supp(Hi ), we have C ∈ supp(H0 ) and Hi (∃r.C) ≥ Hi (r) ⊗ H0 (C); moreover, for all transitive roles s vR r, we have ∃s.C ∈ supp(H0 ) and Hi (∃r.C) ≥ Hi (s) ⊗ H0 (∃s.C). b) For every value restriction ∀r.C ∈ sub(O): – If ∀r.C ∈ supp(H0 ) and i = ϕ(∀r.C), then we have C ∈ supp(Hi ) and H0 (∀r.C) = Hi (r) ⇒ Hi (C). – If ∀r.C ∈ supp(H0 ), then for all i ∈ K, we have C ∈ supp(Hi ) and H0 (∀r.C) ≤ Hi (r) ⇒ Hi (C); moreover, for all transitive roles s vR r, we have ∀s.C ∈ supp(Hi ) and H0 (∀r.C) ≤ Hi (s) ⇒ Hi (∀s.C). – For all i ∈ K with ∀r.C ∈ supp(Hi ), we have C ∈ supp(H0 ) and Hi (∀r.C) ≤ Hi (r) ⇒ H0 (C); moreover, for all transitive roles s vR r, we have ∀s.C ∈ supp(H0 ) and Hi (∀r.C) ≤ Hi (s) ⇒ H0 (∀s.C). c) For all r ∈ N− R (O) and i, j ∈ K such that a ∈ Ind(Hi ), b ∈ Ind(Hj ), and [a]P = [b]P , we have Hi (r) = Hj (r). d) For all a ∈ Ind(H0 ), r ∈ N− R (O), i ∈ K, and b ∈ Ind(Hi ), it holds that Hi (r) = rP ([a]P , [b]P ). Intuitively, Condition a) ensures that the designated successor satisfies the wit- nessing condition for ∃r.C, and that the other successors do not interfere; this includes the parent node, which is a r-predecessor. Additionally, existential re- strictions are transferred along transitive roles, as in the ∀+ -rule from [23]. Con- ditions c) and d) are concerned with the behavior of named successors; in par- ticular, the values for the role connections between named individuals specified by the pre-completion should be respected. Given a pre-completion P = (P, HP , RP ), a Hintikka tree for O starting with HX , X ∈ P, is a mapping T that assigns to each u ∈ K ∗ a Hintikka function T(u) for O that is compatible with T , R, and P such that T(ε) = HX and every tuple (T(u), T(u1), . . . , T(uk)) satisfies the Hintikka condition. The proof of the following lemma can be found in [9]. Lemma 13. O is consistent iff there exist a pre-completion P = (P, HP , RP ) for O and, for each X ∈ P, a Hintikka tree for O starting with HX . The Hintikka automaton for O and HX is the LA AO,HX := (QO , IHX , ∆O ), where QO consists of all pairs (H, i) of Hintikka functions H for O that are compatible with T , R, and P and indices i ∈ K, IHX := {(HX , 1)}, and ∆O is the set of all tuples ((H0 , i0 ), (H1 , 1), . . . , (Hk , k)) such that (H0 , . . . , Hk ) sat- isfies the Hintikka condition. It is easy to see that the first components of the runs of AO,HX are exactly the Hintikka trees for O starting with HX , and the second components simply store the index of the existential or value restriction for which the state acts as a witness. By Lemma 13, consistency of O is thus equivalent to the existence of a pre-completion and the non-emptiness of the Hintikka automata AO,HX for each equivalence class X. Since the number of pre-completions is bounded exponentially in the size of the input (O and L) and each pre-completion is of size polynomial in the size of the input, we can enumerate all pre-completions in exponential time and for each of them check emptiness of the polynomially many automata AO,HX . Since the size of these automata is exponential in the size of the input, by [33] we obtain the following complexity result. ExpTime-hardness holds already in ALC [26]. Theorem 14. In L-ISCHOI over a finite residuated De Morgan lattice L, con- sistency w.r.t. general TBoxes is ExpTime-complete. 5 Acyclic TBoxes We now extend the previous complexity results for lattice-based fuzzy DLs with acyclic TBoxes [13,14] by showing that consistency in L-IALCHO and L-ISCOc is PSpace-complete in this setting. Recall that in L-ISCOc , roles must always be interpreted as crisp functions that only take the values 0 and 1. Due to the absence of inverse roles, in the following we can restrict all definitions to use NR (O) instead of N− R (O), and we can remove Condition d) and the last items of Conditions a) and b) from Definition 12 [9]. Let now O = (A, T , R) be such that T is acyclic. We can guess a triple P = (P, HP , RP ) and verify the conditions of Definition 11 in (nondeterminis- tic) polynomial space. Thus, if emptiness of the polynomially many Hintikka au- tomata AO,HX could be decided in polynomial space, we would obtain a PSpace upper bound for consistency [25]. The idea is to modify the construction of AO,HX using a faithful family of functions to obtain a PSpace on-the-fly construction. As in [13], these automata already satisfy most of Definition 5, except the poly- nomial bound on the maximal length a path before (equality) blocking occurs. The faithful families of functions we use are very similar to those employed in [13] for L-IALCHI and L-ISCI c . For the subsequent constructions to work, we need to change the notion of compatibility of a Hintikka function H with P to a weaker variant: we only require that for every a ∈ Ind(H) and every C ∈ sub(O) for which H(C) is defined, H[a]P (C) is also defined and H(C) = H[a]P (C). This new definition does not work in the presence of inverse roles. However, in L-IALCHO and L-ISCOc , all previous results remain valid [9]. We now present a faithful family of functions for the case that O is formulated in L-IALCHO. For this, we denote by rdT (C) the role depth of the unfolding of a concept C w.r.t. the acyclic TBox T , by rdT (H) for a Hintikka function H the maximal rdT (C) of a concept C ∈ supp(H), and by sub≤n (O) the restriction of sub(O) to concepts C with rdT (C) ≤ n. Definition 15 (family f). We define f = (fq )q∈QO for all q = (H, i) ∈ QO with n := rdT (H) and all q 0 = (H 0 , i0 ) ∈ QO by fq (q 0 ) := (H 00 , i0 ), where, for every C ∈ sub(O) and r ∈ NR (O), ( ( 00 H 0 (C) if C ∈ sub≤n−1 (O), 00 H 0 (r) if supp(H) 6= ∅, H (C) := H (r) := undefined otherwise; 0 otherwise. For all q, q 0 ∈ QO , we have that fq (q 0 ) is again a state of AO,HX (according to the new definition of compatibility with P). The idea is to reduce the maximal role depth of the Hintikka function in every transition of the automaton. This works since in the absence of transitive roles the Hintikka condition only constrains the values of C for restrictions ∃r.C or ∀r.C that appear in the parent node. Thus, (equality) blocking occurs after polynomially many transitions. We show in [9] that f is faithful w.r.t. AO,HX and the construction of the in- duced subautomaton AfO,HX from L, O, and HX constitutes a PSpace on-the-fly construction. By Propositions 4 and 6, we obtain the desired complexity result; PSpace-hardness holds already in classical ALC w.r.t. the empty TBox [27]. Theorem 16. In L-IALCHO over a finite residuated De Morgan lattice L, con- sistency w.r.t. acyclic TBoxes is PSpace-complete. For L-ISCOc , the construction is a little more involved. Since now the interpre- tations of roles are restricted to 0 and 1, all Hintikka functions H for O need to satisfy the additional condition that H(r) ∈ {0, 1} for all r ∈ NR (O). We further denote by ϕr (O) for r ∈ NR (O) the set of all indices i ∈ K such that i = ϕ(C) for a concept C of the form ∃r.D or ∀r.D. We then replace K in Definition 12 by ϕr (O). The idea is that in the absence of role inclusions it suffices to consider one role for each successor. The resulting definition is closer to the Hintikka condition from [13]. Lemma 13 remains valid under these modifications [9]. Given a Hintikka function H for O and a role name r, we define the set H|r := {C ∈ supp(H) | C = ∃r.D or C = ∀r.D}. Definition 17 (family g). We define g = (gq )q∈QO for all q = (H, i) ∈ QO with n := rdT (H) and all q 0 = (H 0 , i0 ) ∈ QO and r0 ∈ NR (O) such that i0 ∈ ϕr0 (O) by gq (q 0 ) := (H 00 , i0 ), where, for all C ∈ sub(O) and r ∈ NR (O): ( sub≤n (O) ∩ H 0 |r0 if r0 is transitive, P := ∅ otherwise; ( H 0 (C) if C ∈ sub≤n−1 (O) ∪ P , H 00 (C) := undefined otherwise; ( H 0 (r) if supp(H) 6= ∅ and r = r0 , H 00 (r) := 0 otherwise. Again, the resulting pair (H 00 , i0 ) is an element of QO . Here, we cannot always reduce the role depth of the Hintikka functions, but have to keep all existential and value restrictions that are transferred along a transitive role r0 to ensure that the family g is faithful w.r.t. AO,HX . To prove that the induced subautomaton AgO,HX is obtained by a PSpace on-the-fly construction, we have to employ a complicated blocking condition that extends the one used for L-ISCI c in [13]. The main problem is to show that every path in a run of this automaton involving the same transitive role r can be blocked after polynomially many steps. The idea is that along such a path, only the values of the concepts in H|r and their direct subconcepts are relevant. Polynomial blocking follows from the facts that r is crisp and the Hintikka condition thus guarantees the values of all these concepts to behave monotonically along this path. For details, see the full proof in [9]. Propositions 4 and 6 and [27] now entail the following result. Theorem 18. In L-ISCOc over a finite residuated De Morgan lattice L, consis- tency w.r.t. acyclic TBoxes is PSpace-complete. As a side effect, we obtain new, albeit not surprising, complexity results for the underlying classical description logics. Corollary 19. In classical ALCHO and SO, consistency w.r.t. acyclic TBoxes is PSpace-complete. SHOI ALCHOI SOI SHO SHI ALCOI ALCHO ALCHI SO SI SH ALCO ALCI ALCH S ALC Fig. 1. The PSpace/ExpTime boundary in classical DLs with acyclic TBoxes 6 Conclusions We have extended previous complexity results about fuzzy DLs with finite lat- tice semantics to cover nominals. This required extensive adaptations of the automata-based algorithm used for L-ISCHI and its sublogics in [13]. We em- ployed pre-completions similar to those in [2,14,21] to show complexity results for ontology consistency. Due to the expressivity of our ABoxes, these easily transfer to other standard reasoning problems. In particular, we have shown that con- sistency in L-ISCHOI w.r.t. general TBoxes can be decided in ExpTime. This drops to PSpace when restricting to acyclic TBoxes in the sublogics L-IALCHO and L-ISCOc . To the best of our knowledge, only the sublogics SI [1,23] and ALCHI [13,14] of classical SHOI were known to have PSpace-complete rea- soning problems w.r.t. acyclic TBoxes. On the other hand, in ALCOI and SH reasoning is already ExpTime-hard without any TBox [22,31]. The present re- sults for ALCHO and SO thus complete the picture about reasoning w.r.t. acyclic TBoxes in the logics between ALC and SHOI (see Figure 1). It would be interesting to extend the presented results to deal with fuzzy role inclusions (hr v s ≥ pi) or cardinality restrictions (≥n r.C), although it is not clear how to define the semantics of the latter in a setting where already a simple existential restriction may entail the existence of n > 1 witnessing role successors. We also plan to extend the automata-based algorithm for the fuzzy DL G-IALC based on the so-called Gödel t-norm over the truth degrees from [0, 1] to more expressive logics using the ideas presented here and in [13,14]. Acknowledgments The author is indebted to Rafael Peñaloza for many discussions on the topics of (fuzzy) DLs in general and automata-based reasoning procedures in particular. References 1. Baader, F., Hladik, J., Peñaloza, R.: Automata can show PSPACE results for description logics. Inform. Comput. 206(9-10), 1045–1056 (2008) 2. Baader, F., Lutz, C., Miličić, M., Sattler, U., Wolter, F.: Integrating description logics and action formalisms for reasoning about web services. LTCS-Report 05-02, Chair for Automata Theory, TU Dresden, Germany (2005), see http://lat.inf.tu- dresden.de/research/reports.html 3. Baader, F., Peñaloza, R.: On the undecidability of fuzzy description logics with GCIs and product t-norm. In: Proc. FroCoS’11, LNCS, vol. 6989, pp. 55–70. Springer (2011) 4. Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69(1), 5–40 (2001) 5. Bobillo, F., Bou, F., Straccia, U.: On the failure of the finite model property in some fuzzy description logics. Fuzzy Set. Syst. 172(1), 1–12 (2011) 6. Bobillo, F., Delgado, M., Gómez-Romero, J.: A crisp representation for fuzzy SHOIN with fuzzy nominals and general concept inclusions. In: Uncertainty Rea- soning for the Semantic Web I. LNAI, vol. 5327, pp. 174–188. Springer (2008) 7. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Joining Gödel and Zadeh fuzzy logics in fuzzy description logics. Int. J. Uncertain. Fuzz. 20(4), 475–508 (2012) 8. Bobillo, F., Straccia, U.: Finite fuzzy description logics and crisp representations. In: Uncertainty Reasoning for the Semantic Web II, LNCS, vol. 7123, pp. 102–121. Springer (2013) 9. Borgwardt, S.: The complexity of fuzzy description logics over finite lattices with nominals. LTCS-Report 14-02, Chair for Automata Theory, TU Dresden, Germany (2014), see http://lat.inf.tu-dresden.de/research/reports.html. 10. Borgwardt, S., Distel, F., Peñaloza, R.: How fuzzy is my fuzzy description logic? In: Proc. IJCAR’12. LNAI, vol. 7364, pp. 82–96. Springer (2012) 11. Borgwardt, S., Peñaloza, R.: Description logics over lattices with multi-valued on- tologies. In: Proc. IJCAI’11. pp. 768–773. AAAI Press (2011) 12. Borgwardt, S., Peñaloza, R.: Undecidability of fuzzy description logics. In: Proc. KR’12. pp. 232–242. AAAI Press (2012) 13. Borgwardt, S., Peñaloza, R.: The complexity of lattice-based fuzzy description logics. J. Data Semant. 2(1), 1–19 (2013) 14. Borgwardt, S., Peñaloza, R.: Consistency reasoning in lattice-based fuzzy descrip- tion logics. Int. J. Approx. Reason. (2014), in press. 15. Cerami, M., Garcia-Cerdaña, À., Esteva, F.: From classical description logic to n-graded fuzzy description logic. In: Proc. FUZZ-IEEE’10. pp. 1–8. IEEE Press (2010) 16. Cerami, M., Straccia, U.: On the (un)decidability of fuzzy description logics under Łukasiewicz t-norm. Inform. Sciences 227, 1–21 (2013) 17. Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics, Studies in Logic and the Foundations of Mathe- matics, vol. 151. Elsevier (2007) 18. Hájek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer (2001) 19. Hájek, P.: Making fuzzy description logic more general. Fuzzy Set. Syst. 154(1), 1–15 (2005) 20. Hladik, J.: To and Fro Between Tableaus and Automata for Description Logics. Ph.D. thesis, Technische Universität Dresden, Germany (2007) 21. Hollunder, B.: Consistency checking reduced to satisfiability of concepts in termi- nological systems. Ann. Math. Artif. Intell. 18(2-4), 133–157 (1996) 22. Horrocks, I.: Optimising Tableaux Decision Procedures for Description Logics. Ph.D. thesis, University of Manchester, UK (1997) 23. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip- tion logics. L. J. IGPL 8(3), 239–263 (2000) 24. Jiang, Y., Tang, Y., Wang, J., Deng, P., Tang, S.: Expressive fuzzy description logics over lattices. Knowl.-Based Syst. 23(2), 150–161 (2010) 25. Savitch, W.J.: Relationships between nondeterministic and deterministic tape com- plexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970) 26. Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. IJCAI’91. pp. 466–471. Morgan Kaufmann (1991) 27. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with comple- ments. Artif. Intell. 48(1), 1–26 (1991) 28. Straccia, U.: A fuzzy description logic. In: Proc. AAAI’98. pp. 594–599 (1998) 29. Straccia, U.: Transforming fuzzy description logics into classical description logics. In: Proc. JELIA’04. LNCS, vol. 3229, pp. 385–399. Springer (2004) 30. Straccia, U.: Uncertainty in description logics: A lattice-based approach. In: Proc. IPMU’04. pp. 251–258 (2004) 31. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res. 12, 199–217 (2000) 32. Tresp, C.B., Molitor, R.: A description logic for vague knowledge. In: Proc. ECAI’98. pp. 361–365. John Wiley and Sons (1998) 33. Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of pro- grams. J. Comput. Syst. Sci. 32(2), 183–221 (1986) 34. Yen, J.: Generalizing term subsumption languages to fuzzy logic. In: Proc. IJ- CAI’91. pp. 472–477. Morgan Kaufmann (1991) 35. Zadeh, L.A.: Fuzzy sets. Inform. Control 8(3), 338–353 (1965)