We consider the fuzzy logic ALCI with semantics based on a nite residuated lattice. We show that the problems of satis ability and subsumption of concepts in this logic are ExpTime-complete w.r.t. general TBoxes and PSpace-complete w.r.t. acyclic TBoxes. This matches the known complexity bounds for reasoning in crisp ALCI.
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
literature on the topic is very extensive (see [
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 [
If one considers the Lukasiewicz t-norm over nitely many values, then
reasoning is decidable even for very expressive DLs, as shown in [
In this paper, we improve these complexity results to the fuzzy logic ALCIL over nite lattices with general and acyclic TBoxes. More precisely, we show that in this logic, concept satis ability 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 rst give a short introduction to residuated lattices, which will be used for de ning 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 complexity of deciding satis ability and subsumption of concepts. 2.1
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 2 L. L induces the ordering `1 `2 i `1 ^ `2 = `1 for all `1; `2 2 L. L is called distributive if _ and ^ distribute over each other, nite if L is nite, and bounded if it has a minimum and a maximum element, denoted as 0 and 1, respectively. It is complete if joins and meets of arbitrary subsets T L, denoted by Wt2T t and Vt2T t respectively, exist. Every nite 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 involutive 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 2 L.
A residuated lattice is a lattice L extended with two binary operators (called t-norm) and ) (called residuum) such that is associative, commutative, and has 1 as its unit and for every `1; `2; `3 2 L, `1 `2 `3 i `2 `1 ) `3 holds. In a complete residuated lattice L, `1 ) `2 = Wfx j `1 x `2g.3 A simple consequence of this is that for every `1; `2 2 L, (i) 1 ) `1 = `1, and (ii) `2 `2 i `1 ) `2 = 1. Additionally, the t-norm is always monotonic.
In a residuated De Morgan lattice L, one can de ne the t-conorm as
`1 `2 := ( `1 `2). For example, the meet operator `1 ^ `2 de nes a
t-norm; its t-conorm is `1 _ `2.
2 For a more comprehensive view on residuated lattices, we refer the reader to [
In the following section, we will describe the fuzzy description logic ALCIL,
whose semantics uses the residuum ) and the negation . We emphasize,
however, 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 [
To obtain upper bounds for the complexity of reasoning in ALCIL, we will make a reduction to the emptiness problem of looping automata on in nite trees. These automata receive as input the (unlabeled) in nite k-ary tree K for K := f1; : : : ; kg with k 2 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.
De nition 1 (looping automaton). A looping automaton (LA) is a tuple A = (Q; I; ) where Q is a nite 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(") 2 I and for every u 2 K we have (r(u); r(u1); : : : ; r(uk)) 2 . 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 [
De nition 2 (m-blocking). Let A = (Q; ; I) be a looping automaton. We say that A is m-blocking for m 2 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 > jQj. However, the main interest in blocking automata arises when one can nd a smaller bound on m. One way to reduce this limit is through a so-called faithful family of functions.
De nition 3 (faithful). Let A = (Q; ; I) be a looping automaton on k-ary trees. The family of functions fq : Q ! Q for q 2 Q is faithful w.r.t. A if for all q; q0; q1; : : : ; qk 2 Q, { if (q; q1; : : : ; qk) 2 { if (q0; q1; : : : ; qk) 2 , then (q; fq(q1); : : : ; fq(qk)) 2 , and , then (fq(q0); fq(q1); : : : ; fq(qk)) 2 .
The subautomaton AS = (Q; S ; I) of A induced by this family has the transition relation S = f(q; fq(q1); : : : ; fq(qk)) j (q; q1; : : : ; qk) 2 g.
Lemma 4 ([
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.
De nition 5 (PSpace on-the- y construction). Assume that we have a set I of inputs and a construction that yields, for every i 2 I, an mi-blocking automaton Ai = (Qi; i; Ii) working on ki-ary trees. This construction is called a PSpace on-the- y 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 2 Qi, a transition from i with rst component q.
Theorem 6 ([
In Section 5 we will use this theorem to give PSpace upper bounds on the complexity of reasoning in the logic ALCIL, which we introduce next. 3
The Fuzzy Logic ALCI L For the rest of this paper, L denotes a xed residuated, complete De Morgan lattice with the t-norm . The fuzzy description logic ALCIL 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 ALCIL is the same as in ALCI: given the sets NC and NR of concept and role names, the set of complex roles is NR [ fr j r 2 NRg, and ALCIL concepts are built using the syntactic rule
C ::= A j C1 u C2 j C1 t C2 j :C j 9s:C j 8s:C j > j ?; where A 2 NC and s is a complex role. For a complex role s, the inverse of s (denoted by s) is s if s 2 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.
De nition 7 (semantics of ALCIL). 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 ALCIL concepts as follows for every x 2 I : { >I (x) = 1; ?I (x) = 0, { (C u D)I (x) = CI (x) { (:C)I (x) = CI (x), { (9s:C)I (x) = Wy2 I sI (x; y) CI (y), { (8s:C)I (x) = Vy2 I sI (x; y) ) CI (y),
DI (x), (C t D)I (x) = CI (x)
DI (x), where (r )I (x; y) = rI (y; x) for all x; y 2 I and r 2 NR.
Notice that, unlike in crisp ALCI, existential and universal quanti ers are not dual to each other, i.e. in general, (:9s:C)I (x) = (8s::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 satis ed.
De nition 8 (axioms). Terminological axioms are (labeled) concept de ni: tions of the form hA = C; `i or (labeled) general concept inclusions (GCIs) hC v D; `i, where A 2 NC, C; D are ALCIL concepts, and ` 2 L.
A general TBox is a nite set of GCIs. An acyclic TBox is a nite set of concept de nitions such that every concept name occurs at most once in the lefthand side of an axiom, and there is no cyclic dependency between de nitions. A TBox is either a general TBox or an acyclic TBox.4 :
An interpretation I satis es the concept de nition hA = C; `i if for every x 2 I , (AI (x) ) CI (x)) (CI (x) ) AI (x)) ` holds. It satis es the GCI hC v D; `i if for every x 2 I , CI (x) ) DI (x) `. I is a model of the TBox T if it satis es 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 de ned, 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 quanti ed concept, i.e. a concept of the form 9s:C or 8s:C for some complex role s and concept C.
We emphasize here that ALCI is a special case of ALCIL, where the
underlying 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
conjunction and disjunction, respectively. Accordingly, one can generalize the reasoning
problems for ALCI to the use of other lattices. We will focus on deciding strong
`-satis ability and `-subsumption [
De nition 9 (satis ability, subsumption). Let C; D be ALCIL concepts, T a TBox, and ` 2 L. C is strongly `-satis able w.r.t. T if there is a model I of T and an x 2 I such that CI (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 satis ability is undecidable in ALCL [
nite 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 satis ability and subsumption as in the crisp case; that is, the lattice based semantics do not increase the complexity of the logic. 4
Deciding Strong Satis ability and Subsumption
Recall that the semantics of the quanti ers require the computation of a
supremum or in mum of the membership degrees of a possibly in nite set of elements
of the domain. To obtain an e ective decision procedure, one usually restricts
reasoning to witnessed models [
De nition 10 (witnessed model). Let n 2 N. A model I of a TBox T is called n-witnessed if for every x 2 I and every concept of the form 9r:C there are n elements x1; : : : ; xn 2 I such that (9r:C)I (x) =
CI (xi); n _ rI (x; xi) i=1 and analogously for the universal restrictions 8r:C. In particular, if n = 1, then the suprema and in ma from the semantics of 9r:C and 8r: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 nite, we always have the n-witnessed model property for some n 2 N.
Lemma 11. If the cardinality of the largest antichain of L is n, then ALCIL 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 2 N.
Our algorithm for deciding satis ability and subsumption of concepts exploits the fact that a TBox T has a model i 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 veri es the satis ability 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 ) [ f g, where is an arbitrary new element, which will be used to express the degree with which the role relation to the parent node holds. De nition 12 (Hintikka function). A Hintikka function for C; T is a partial function H : sub(C; T ) [ f g ! L such that: (i) H is de ned for and for all atoms, (ii) if H(D u E) is de ned, then H(D) and H(E) are also de ned and it holds that H(D u E) = H(D) H(E), (iii) if H(D t E) is de ned, then H(D) and H(E) are also de ned and it holds that H(D t E) = H(D) H(E), (iv) if H(:D) is de ned, then H(D) is de ned and H(:D) = H(D). : It is compatible with the concept de nition hA = E; `i if, whenever H(A) is de ned, then H(E) is de ned 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 de ned and H(E) ) H(F ) ` holds.
The Hintikka trees have a xed arity k determined by the number of existential and universal restrictions, i.e. concepts of the form 9s:F or 8s: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 x an arbitrary bijection
' : fE j E 2 sub(C; T ) is of the form 9s:F or 8s:F g ! K: De nition 13 (Hintikka condition). The tuple (H0; H1; : : : ; Hk) of Hintikka functions for C; T satis es the Hintikka condition if: (i) For every existential restriction 9s:G 2 sub(C; T ) { H'(9s:G)(G) is de ned and H0(9s:G) = H'(9s:G)( ) H'(9s:G)(G), and { H'(E)(G) is de ned and H0(9s:G) H'(E)( ) H'(E)(G) for every restriction E 2 sub(C; T ) of the form 9s:F or 8s:F . (ii) For every universal restriction 8s:G 2 sub(C; T ) { H'(8s:G)(G) is de ned and H0(8s:G) = H'(8s:G)( ) ) H'(8s:G)(G), { H'(E)(G) is de ned and H0(8s:G) H'(E)( ) ) H'(E)(G) for every restriction E 2 sub(C; T ) of the form 9s:F or 8s:F . (iii) For every existential restriction 9s:G 2 sub(C; T ) and every restriction E 2 sub(C; T ) of the form 9s:F or 8s:F , H0(G) is de ned and H'(E)(9s:G) H'(E)( ) H0(G). (iv) For every universal restriction 8s:G 2 sub(C; T ) and every restriction E 2 sub(C; T ) of the form 9s:F or 8s:F , H0(G) is de ned and H'(E)(8s: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 9s:G is witnessed by its designated successor '(9s: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 in nite k-ary tree T labeled with compatible Hintikka functions for C; T such that T(")(C) is de ned and the tuple (T(u); T(u1); : : : ; T(uk)) satis es the Hintikka condition for every node u 2 K . The de nition of compatibility ensures that all axioms are satis ed 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 [
Proof (Sketch). Every witnessed model I of T with a domain element x 2 I for which CI (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 2 sub(C; T ) of the form 9s:F or 8s:F and nding the witness y 2 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 valuation for each concept name that satis es all the axioms in T . Indeed, if T is a general TBox, then every concept name is primitive, and hence the valuation is already de ned. The fact that the Hintikka function is compatible with all the axioms in T implies that every node satis es the TBox. On the other hand, if T is an acyclic TBox, and H is unde ned for some concept names, then consider an axiom hA =: C; `i for which H(A) is unde ned, but H(B) is de ned 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 satis es the conditions of De nition 12. If we set H(A) := H(C), then H is still compatible with T . By an induction argument, we can de ne a compatible total Hintikka function, and thus a valuation for every concept name that satis es T .
For this valuation to be an interpretation, it only remains to be shown that the semantics of the existential and universal restrictions are satis ed. 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 `-satis able w.r.t. T . tu
Hintikka trees can also be used for deciding (non-)subsumption between ALCIL concepts. The proof of the following theorem is analogous to the one of Theorem 14.
Theorem 15. Let C; D be ALCIL concepts, T a TBox, and ` 2 L. Then C is not `-subsumed by D (in a witnessed model) i 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 satis ability, since the residuum ) cannot in general be expressed using only the t-norm, tconorm 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 satis ability and subsumption of ALCIL 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 ALCIL reasoning to the emptiness problem of these automata. For the following, we focus only on deciding satis ability and explain the minor modi cations required for deciding subsumption.
De nition 16 (Hintikka automaton). Let C be an ALCIL concept, T a TBox, and ` 2 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 `-satis able w.r.t. T i 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 i 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 satis ability and subsumption, since
these problems are already ExpTime-hard for crisp ALC [
Theorem 17. Deciding strong satis ability and subsumption in ALCIL 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 emptiness test of the automaton from De nition 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 satis ability and subsumption of ALCIL 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- y construction. Notice that AC;T ;` satis es all but one of the 6 Using C u D only ensures that T(")(C) and T(")(D) are de ned, but imposes no further restriction on their values. conditions from De nition 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 jsub(C; T )j; (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 jsub(C; T )j. However, it is easy to build runs of the automata constructed by this reduction where blocking occurs only after exponentially many transitions, violating the rst condition of PSpace on-the- y 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 su ces 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 ALCIL concepts is recursively de ned as follows: rdT (A) = rdT (>) = rdT (?) = 0 for every primitive concept name A; rdT (C u D) = rdT (C t D) = maxfrdT (C); rdT (D)g; rdT (:C) = rdT (C); rdT (:9r:C) = rdT (8r:C) = rdT (C) + 1; and rdT (A) = rdT (C) for every de nition hA = C; `i 2 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 de ned and H(C) > 0. We de ne rdT (H) as the maximum rdT (D) such that D 2 support(H). De nition 18 (functions fH ). Let H and H0 be two states of AC;T ;` with rdT (H) = n. The function fH (H0) is given by: if D is an atom and rdT (D)
n if rdT (D) < n otherwise. fH (H0)(D) = fH (H0)( ) = 80 > <
H0(D) >:unde ned (0
if support(H) = ;
H0( ) otherwise.
Since T is acyclic, the function fH (H0) de ned 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 De nition 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 satis es the Hintikka condition. We show in detail only the proof for the restriction (i) from De nition 13, as the others can be treated analogously.
For 9s:G 2 sub(C; T ), the value H'(E)(G) is de ned for all restrictions E of the form 9s:F or 8s:F in sub(C; T ). If rdT (9s:G) > rdT (H), then H(9s:G) = 0, and all the values fH (H'(E))(G) are 0. Thus, the inequalities are trivially satised. Otherwise, rdT (G) < rdT (9s: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 satis ed. Otherwise, H(9s:G) = 0, and all the values fH (H'(E))( ) are 0. Thus, the inequalities are again trivially satis ed. tu S By Lemma 4, AC;T ;` is empty i the induced subautomaton AC;T ;` is empty.
S Theorem 20. The construction of AC;T ;` from an ALCIL concept C, ` 2 L, and an acyclic TBox T is a PSpace on-the- y construction.
S Proof. As described before, we only need to show that the automata AC;T ;` are m-blocking for some m bounded polynomially in jsub(C; T )j. We show that this holds for m = maxfrdT (D) j D 2 sub(C; T )g + 2.
S
By de nition of AC;T ;`, every transition decreases the maximal role depth of the support of the state. Hence, after at most maxfrdT (D) j D 2 sub(C; T )g transitions, we reach a state H, where H(D) = 0 if D is an atom and unde ned 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 nd two states that are equal. Since m jsub(C; T )j + 2, ASC;T ;` satis es the requirements for a PSpace on-the- y construction. tu
S
This shows that emptiness of AC;T ;` and hence also of AC;T ;` is in PSpace.
This yields the desired PSpace upper bound for satis ability and similar
arguments can be made for subsumption. PSpace-hardness follows from
PSpacehardness of satis ability and subsumption w.r.t. the empty TBox in ALC [
Notice that the de nitions of Hintikka functions and Hintikka trees are independent 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 de nitions in which is replaced by the simple meet t-norm ^.
We also point out that the algorithm can be modi ed 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 quanti ed formula in sub(C; T ); the arity of AC;T ;` grows polynomially in n. This does not a ect the complexity upper bounds from the automata, and hence Theorems 17 and 21 still hold. 6
Conclusions
We have shown that reasoning in ALCIL is not harder than in the underlying
crisp DL ALCI. More precisely, strong `-satis ability 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 [
In the future, we want to study the in uence of additional DL constructors
and axioms on the complexity of the reasoning tasks. In particular, transitive
roles, which are covered by the results in [
Satis ability w.r.t. general TBoxes and residuated total orders has been
shown to be undecidable [