In some knowledge domains, a correct handling of vagueness and imprecision is fundamental for adequate knowledge representation and reasoning. For example, when trying to diagnose a disease, medical experts need to confront symptoms described by the patient, which are by de nition subjective, and hence vague. Moreover, a single malady may present a diversity of clinical manifestations in di erent patients, which leads to imprecise (partial) diagnoses. Fuzzy logic [15] is a prominent approach for dealing with imprecise knowledge. It is based on the notion of fuzzy sets [25], where elements are assigned a membership degree from the real interval [0; 1]. So-called t-norms are used to de ne the interpretation of the logical connectives. The notion of membership degrees and the operators used can be generalized to lattices, giving rise to L-fuzzy sets [13] and lattice-based t-norms [26, 12]. During the last two decades, several fuzzy DLs have been de ned by enriching classical DLs rst with fuzzy set semantics [24, 20, 19] and then t-norms [16, 7, 11]. Attempts have also been made at using L-fuzzy set semantics [21, 17]. However, all these approaches either disregard the terminological knowledge, or allow only for a limited class of TBoxes. In fact, it is still unknown whether standard reasoning in fuzzy DLs with general TBoxes is decidable [5, 3]. To the best of our knowledge, the only approaches capable of dealing with full fuzzy TBoxes are based on a nite total order with the Lukasiewicz t-norm [6, 8] or nite De Morgan lattices with the minimum t-norm [9]. In this paper we introduce the lattice-based fuzzy DL ALCL, where L is a complete De Morgan lattice equipped with a t-norm operator. We show that satis ability in this logic is undecidable if L is in nite. Undecidability holds even if L is a countable, residuated total order. On the other hand, if L is nite, then satis ability becomes decidable and, under some conditions on the lattice and the t-norm, ExpTime-complete, i.e. not harder than satis ability in crisp ALC. Our reasoning procedure is in fact general enough to handle any kind of truth-functional semantics, as long as the functions de ning the connectives are computable.
A lattice is an algebraic structure (L; _; ^) over a carrier set L with two binary operations supremum _ and in mum ^ that are idempotent, associative, and commutative and satisfy the absorption laws ` _ (` ^ m) = ` = ` ^ (` _ m) for all `; m 2 L. The order on L is de ned by ` m i ` ^ m = ` for all `; m 2 L. A lattice is 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 suprema and in ma of arbitrary subsets T L exist; these are denoted by Wt2T t and Vt2T t, respectively. Notice that 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 (` _ m) = ` ^ m and (` ^ m) = ` _ m for all `; m 2 L. Figure 1 shows a simple De Morgan lattice.
In fuzzy logics, conjunctions and disjunctions are interpreted with the help of t-norms and t-conorms. Given a De Morgan lattice L, a t-norm on L is an associative and commutative binary operator : L L ! L which has the unit 1, and is monotonic in both arguments. Given a t-norm , its associated t-conorm is constructed using the negation as follows: ` m := ( ` m). For example, the in mum operator ` m := `^m de nes a t-norm; its associated t-conorm is then given by ` m := ` _ m.
Another important operator is the residuum, which is used for interpreting implications in the logic. The residuum of a t-norm on a complete lattice L is the binary operator ) de ned by ` ) m := Wfx j ` x mg. If ` (` ) m) m for all `; m 2 L (that is, if the supremum in the de nition of residuum is always a maximum), then is called residuated and L a residuated lattice.1
In the following we will use two important properties of the residuum: for every `; m 2 L, (i) 1 ) ` = `, and (ii) if ` m, then ` ) m = 1. Additionally, if is residuated, then ` ) m = 1 implies that ` m.
In the next section, we describe the multi-valued description logic ALCL,
whose semantics uses the residuum ) and the De Morgan negation . We
emphasize, however, that the reasoning algorithm presented in Section 5 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 multi-valued
semantics, e.g. [
The Fuzzy Logic ALCL In the following, we will assume that L is a complete De Morgan lattice and is a t-norm on L. The multi-valued description logic ALCL is a generalization of the crisp DL ALC that allows the use of the elements of a complete De Morgan lattice as truth values, instead of just the Boolean values true and false. The syntax of concept descriptions in ALCL is the same as in ALC; that is, ALCL concept descriptions are built from a set of concept names and role names through the constructors u; t; :; >; ?; 9 and 8.
The semantics of this logic is based on interpretation functions that not simply describe whether an element of the domain belongs to a concept or not, but give a lattice value describing the membership degree of the element to this concept; more formally, the semantics is based on L-fuzzy sets.
De nition 1 (semantics of ALCL). 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 ALCL concept descriptions 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), { (9r:C)I (x) = W CI (y), { (8r:C)I (x) = Vy2 I rI (x; y) y2 I rI (x; y) ) CI (y).
DI (x), (C t D)I (x) = CI (x)
DI (x),
Notice that, unlike crisp ALC, the existential and universal quanti ers are not dual to each other, i.e. in general :9r:C and 8r::C have di erent semantics.
The axioms in a TBox are also associated to a lattice value, allowing for a general notion of subsumption between concepts that is based on the residuum. De nition 2 (TBox). A TBox is a nite set of (labeled) general concept inclusions (GCIs) of the form hC v D; `i, where C; D are ALCL concept descriptions and ` 2 L.
An interpretation I satis es a GCI hC v D; `i if Vx2 I CI (x) ) DI (x) `. I is called a model of the TBox T if it satis es all axioms in T .
We emphasize here that ALC is a special case of ALCL, 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 think of generalizing the reasoning problems for ALC to the use of other lattices. We will focus on the problem of deciding satis ability of a concept. We are further interested in computing the highest degree with which an individual may belong to a concept. De nition 3 (satis ability). Let C; D be ALCL concept descriptions, T a TBox and ` 2 L. C is `-satis able w.r.t. T if there is a model I of T such that Wx2 I CI (x) `. The best satis ability degree for C w.r.t. T is the largest ` such that C is `-satis able w.r.t. T .
Notice that if C is `-satis able and `0-satis able w.r.t. T , then C is also ` _ `0satis able. Hence, the notion of the best satis ability degree is well de ned.
In some cases, however, this de nition of satis ability turns out to be too weak, since a concept C may be `-satis able even if no element of the domain may ever belong to C with a value `. Consider the following example. Example 4. We use the lattice L2 from Figure 1 with t-norm ` `0 := ` ^ `0 and the TBox T = fh> v (A u :A) t (B u :B); 1ig. The concept A is 1-satis able w.r.t. T since the interpretation I0 = (fx1; x2g; I0 ) with
AI0 (x1) = BI0 (x2) = `a and BI0 (x1) = AI0 (x2) = `b is a model of T and `a _ `b = 1. However, since ` ^ ` 6= 1 for every ` 2 L2, the axiom can only be satis ed for any y 2 I if fAI (y); BI (y)g = f`a; `bg. Thus, we always have AI (y) < 1.
For this reason, we consider a stronger notion of satis ability that requires at least one element of the domain to satisfy the concept with the given value. A concept C is strongly `-satis able w.r.t. a TBox T if there is a model I of T and an x 2 I such that CI (x) `. Obviously, strong `-satis ability implies `-satis ability. As shown in Example 4, the converse does not hold.
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. If the lattice is nite, then this is in fact a computation
over a nite set of values, but it may be a costly one. If the lattice is in nite,
then the problem is more pronounced. For that reason, it is customary in fuzzy
description logics to restrict reasoning to witnessed models [
CI (xi); and analogously for the universal restrictions 8r:C. In particular, if = 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.
As we will show, `-satis ability, even w.r.t. -witnessed models, is undecidable in general. For nite De Morgan lattices, however, this problem is decidable and belongs to the same complexity class as deciding satis ability of crisp ALC concepts, if the lattice operations are easily computable. 4
Consider the lattice L1 over the domain ([0; 1] \ Q) [ f 1; 1g with the usual total order, the De Morgan negation ` = 1 ` if ` 2 [0; 1], 1 = 1, and ( 1) = 1, and the t-norm
de ned by ` 8maxf` + m > m := <
1 >:minf`; mg 1; 0g if `; m 2 [0; 1] and ` + m 6= 0, if ` = m = 0, and otherwise.
That is, is the Lukasiewicz t-norm on the rationals in (0; 1] extended with two extreme elements 1 and 1. One can easily con rm that this is in fact a residuated lattice and its t-conorm is given by `
1 >:maxf`; mg 8minfl + m; 1g if `; m 2 [0; 1] and ` + m 6= 2, > m := < if ` = m = 1, and
otherwise.
We will reduce the well-known undecidable Post Correspondence Problem [
De nition 6 (PCP). Let v1; : : : ; vp and w1; : : : ; wp be two nite lists of words over an alphabet = f1; : : : ; sg. The Post Correspondence Problem (PCP) asks whether there is a non-empty sequence i1; i2; : : : ; ik, 1 ij p such that wik . Such a sequence, if it exists, is called a solution of For a word = i1i2 ik 2 f1; : : : ; pg we will use v ; w to denote the words vi1 vi2 vik and wi1 wi2 wik , respectively. Given an instance P of PCP, we will construct a TBox TP and a concept name S such that S is strongly 1-satis able i P has no solution. For doing this, we will encode words w from the alphabet as rational numbers 0:w in [0; 1] in base s + 1; exceptionally, the empty word will be encoded by the number 0. The two concept names V and W will store the encoding of the concatenated words v and w , respectively.
Given two ALCL concept descriptions C; D and a role name r, the expression hC Di abbreviates the two axioms hC v D; 1i,hD v C; 1i and the expression hC r Di abbreviates the two axioms hC v 8r:D; 1i, h:C v 8r::D; 1i. For an interpretation I, hC Di expresses that CI (x) = DI (x) for every x 2 I , while hC r Di expresses that, for every x; y 2 I such that rI (x; y) = 1, it holds that CI (x) = DI (y). We will also use n C as abbrevation for the n-ary disjunction C t t C, which is interpreted at x 2 I as the value minfCI (x) + + CI (x); 1g = minfn CI (x); 1g whenever CI (x) 2 [0; 1].
We now de ne the TBoxes TPi for 0 i p as follows:
TP0 := fhS v V; 0i; hS v :V; 1i; hS v W; 0i; hS v :W; 1ig [ fhS v Vi; 0:vii; hS v :Vi; 1 hS v Wi; 0:wii; hS v :Wi; 1 0:vii; pg; TPi := fh> v 9ri:>; 1i; hV t Vi ri V i; hW t Wi ri W ig [ fhVj (s + 1)jvij Fij i; hWj
(s + 1)jwij Gij i; hFij ri Vj i; hGij ri Wj i j 1 j pg: Intuitively, TP0 initializes a search tree for a solution of P, by setting both V and W to the empty word, and describing each pair (vi; wi) by the concepts Vi and Wi. Each TBox TPi then extends the search tree by concatenating each pair of words v; w produced so far with vi and wi, respectively. More formally, consider the interpretation IP = ( IP ; IP ) where { IP = f1; : : : ; pg , { V IP ( ) = 0:v ; W IP ( ) = 0:w ; ViIP ( ) = (s+01:v)jiv j ; WiIP ( ) = (s+1)jw j 0:wi { riIP ( ; i) = 1 and riIP ( ; 0) = { SIP (") = 1.
1 if 0 6= i, and It is easy to see that IP is in fact a model of the TBox T0 := Sip=0 TP . More i interesting, however, is that every model of this TBox where S is 1-satis able must include IP , as stated in the following lemma.
Lemma 7. Let I be a model of T0 such that SI (x) = 1 for some x 2 I . There exists a function f : IP ! I such that CIP ( ) = CI (f ( )) holds for every concept name C occurring in T0 and 2 IP .
Proof (Sketch). The function f is constructed by induction on the length of . We can de ne f (") := x since SI (x) = 1 and I is a model of TP0. Let now be such that f ( ) is already de ned. The axioms h> v 9ri:>; 1i ensure that, for every i; 1 i p there is a 2 I such that riI (f ( ); ) = 1. The de nition f ( i) := satis es the required property. tu
This lemma shows that every model of T0 must include a search tree for a solution of P. Thus, in order to know whether a solution exists, we need to decide if there is a node of this tree where the concept names V and W are interpreted by the same value. Notice that, for any two values `; m 2 [0; 1], ` 6= m i ( ` m) (` m) < 1. Moreover, ` < 1 i ` ` 1 or, equivalently, ` ` 0. Thus, as IP always interprets the concept names V and W in the interval [0; 1], it is a model of the TBox
T 0 := fhE (:A t B) u (A t :B)ig [ fh> v 8ri::(E t E); 0i j 1 i pg i AIP ( ) 6= BIP ( ) holds for every
2 f1; : : : ; pg+.
Theorem 8. The instance P of the PCP has a solution i S is not 1-satis able w.r.t. TP := T0 [ T 0.
Notice that the interpretation IP is witnessed, which means that undecidability holds even if we restrict reasoning to -witnessed models, for any 2 N. Corollary 9. (Strong) satis ability is undecidable, even if the lattice is a countable, residuated total order and reasoning is restricted to -witnessed models, with 2 N.
In the previous section, we have shown that satis ability is undecidable in general. We now show that if we consider only nite De Morgan lattices L, then satis ability in ALCL can be e ectively decided. As the following lemmata show, in this case we can restrict to strong `-satis ability w.r.t. -witnessed models. Lemma 10. The best satis ability degree for C w.r.t. T is the supremum of all ` such that C is strongly `-satis able.
Proof (Sketch). If C is strongly `-satis able and strongly `0-satis able, there are two models I; I0 of T and x 2 ; x0 2 0 with CI (x) ` and CI0 (x0) `0. The disjoint union of I and I0 gives a model J where Wy2 J CJ (y) ` _ `0. tu
We can then nd out whether C is `-satis able by comparing ` to the best satis ability degree of C. We will thus focus on nding all the lattice elements that witness the strong `-satis ability of a given concept.
Lemma 11. If L has width 2 N, i.e. the cardinality of the largest antichain of L is , then ALCL has the -witnessed model property.
To simplify the description, we consider = 1 only. The algorithm and the proofs of correctness can be easily adapted for any other 2 N.
Our approach reduces strong `-satis ability to the emptiness problem of an automaton on in nite trees. Before giving the details of this reduction, we present a brief introduction to these automata. The automata work over the in nite kary tree K for K := f1; : : : ; kg with k 2 N. The positions of the nodes in this tree are represented through words in K : the empty word " represents the root node, and ui represents the i-th successor of the node u.
De nition 12 (looping automaton). A looping automaton (LA) is a tuple A = (Q; I; ) consisting of a nite set Q of states, a set I Q of initial states, and a transition relation Q Qk. A run of A is a mapping r : K ! Q assigning states to each node of K such that (i) r(") 2 I and (ii) 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 problem for LA can be solved in polynomial time [
The following automata-based algorithm uses the fact that a concept is strongly `-satis able i it has a well-structured tree model, called a Hintikka tree. Intuitively, Hintikka trees are abstract representations of tree models that explicitly express the membership value of all \relevant" concept descriptions. The automaton we construct will have exactly these Hintikka trees as its runs. Strong `-satis ability is hence reduced to an emptiness test of this automaton.
We denote as sub(C; T ) the set of all subconcepts of C and of the concept descriptions D and E for all hD v E; `i 2 T . The states of the automaton will be so-called Hintikka sets. These are L-fuzzy sets over the domain sub(C; T ) [ f g, where is an arbitrary new element.
De nition 13 (Hintikka set). A function H : sub(C; T ) [ f g ! L is called a (fuzzy) Hintikka set for C; T if the following four conditions are satis ed: (i) H(D u E) = H(D) H(E) for every D u E 2 sub(C; T ), (ii) H(D t E) = H(D) H(E) for every D t E 2 sub(C; T ), (iii) H(:D) = H(D) for every :D 2 sub(C; T ), and (iv) H(D) ) H(E) ` for every GCI hD v E; `i in T .
The arity k of our automaton is determined by the number of existential and universal restrictions, i.e. concept descriptions of the form 9r:D or 8r:D, contained in sub(C; T ). Intuitively, each successor will act as the witness for one of these restrictions. The additional domain element will be used to express the degree with which the role relation to the parent node holds. 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 9r:D or 8r:Dg ! K. The following conditions de ne the transitions of our automaton. De nition 14 (Hintikka condition). The tuple (H0; H1; : : : ; Hk) of Hintikka sets for C; T satis es the Hintikka condition if: (i) H0(9r:D) = H'(9r:D)( ) H'(9r:D)(D) for every existential restriction 9r:D 2 sub(C; T ), and additionally H0(9r:D) H'(F )( ) H'(F )(D) for every restriction F 2 sub(C; T ) of the form 9r:E or 8r:E, (ii) H0(8r:D) = H'(8r:D)( ) ) H'(8r:D)(D) for every universal restriction 8r:D 2 sub(C; T ), and additionally H0(8r:D) H'(F )( ) ) H'(F )(D) for every restriction F 2 sub(C; T ) of the form 9r:E or 8r:E.
A Hintikka tree for C; T is an in nite k-ary tree T labeled with Hintikka sets where, for every node u 2 K , the tuple (T(u); T(u1); : : : ; T(uk)) satis es the Hintikka condition. The de nition of Hintikka sets 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). A Hintikka tree can be seen as a witnessed model with domain K and interpretation function given by the Hintikka sets. The conditions satis ed by the Hintikka sets and the Hintikka condition ensure that this interpretation is well-de ned. Thus, if there is a Hintikka tree T for C; T with T(")(C) `, then C is strongly `-satis able w.r.t. T .
On the other hand, every witnessed model I 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 Hintikka set that records the membership values of x for each concept from sub(C; T ). We then create successors of the root by considering every element of sub(C; T ) of the form 9r:D or 8r:D and nding the witness y 2 I for this restriction. We create a new node for y which is an r-successor of the root node with degree rI (x; y). By continuing this process, we construct a Hintikka tree T for C; T for which T(")(C) ` holds. tu
Thus, strong `-satis ability w.r.t. witnessed models is equivalent to the nonemptiness of the following automaton.
De nition 16 (Hintikka automaton). Let C be an ALCL concept description, T a TBox, and ` 2 L. The Hintikka automaton for C; T ; ` is the LA AC;T ;` = (Q; I; ) where Q is the set of all Hintikka sets for C; T , I contains all Hintikka sets H with H(C) `, and is the set of all (k + 1)-tuples of Hintikka sets 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.
The size of the automaton AC;T ;` is exponential in C; T and polynomial in L. Hence, the emptiness test for this automaton uses time exponential in C; T and polynomial in the complexity of the lattice operations on L. Notice however that in general the encoding enc(L) of a lattice L may be much smaller than the whole lattice L. For this reason we need to consider the complexity of the lattice operations w.r.t. this encoding.
Theorem 17. If jLj is at most exponential in jenc(L)j and the lattice operations are in a complexity class C w.r.t. the size of enc(L),2 then strong `-satis ability (w.r.t. witnessed models) is in ExpTimeC.
Furthermore, the emptiness test of AC;T ;` can be used to compute the set of all Hintikka sets that may appear at the root of a Hintikka tree. From this set we can extract the set of all values ` such that T( )(C) ` for some Hintikka tree T. From the presented results it follows that the best satis ability degree can also be computed in ExpTimeC.
Corollary 18. If L is xed or of size polynomial in jenc(L)j and , can be computed in time polynomial in jLj, then (strong) `-satis ability (w.r.t. witnessed models) is ExpTime-complete.
Proof. ExpTime-hardness follows from ExpTime-hardness of concept satis
ability in crisp ALC [
m = n, etc. for given `; m; n 2 L is in C.
Notice that the de nitions of Hintikka sets 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 ` ) m := `_m 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.
As a last remark, we want to point out that the algorithm can be modi ed for reasoning w.r.t. -witnessed models with > 1. One needs only extend the arity of the Hintikka trees to account for witnesses for each quanti ed formula in sub(C; T ). The emptiness test of the automaton, and hence also satis ability w.r.t. -witnessed models, is exponential in . 6
We have introduced the fuzzy DL ALCL whose semantics is based on arbitrary complete De Morgan lattices and t-norms. To the best of our knowledge, all previously existing approaches for fuzzy ALC, either based on total orders or on lattices, are special cases of ALCL.
We showed that reasoning in this logic is undecidable, even if restricted to a
very simple in nite lattice and t-norm. This result suggests, but does not prove,
that reasoning with the Lukasiewicz t-norm over the interval [0; 1] may, contrary
to previous claims [
For the special case of nite lattices, we showed decidability by presenting
an automata-based decision procedure that runs in exponential time, assuming
a polynomial-time oracle for computing the lattice and t-norm operations. An
advantage of our decision procedure is that it can easily be adapted to deal with
di erent kinds of truth-functional semantics, and hence is useful for di erent
applications. Given the promising rst steps towards an automata-based
implementation of ALC reasoning shown in [
There are three issues that we will pursue in future work. The rst is to explore the limits of undecidability: are there classes of in nite lattices and tnorms in which reasoning is decidable? As said before, it is still unknown whether reasoning in fuzzy ALC with continuous t-norms over [0; 1] is decidable.
The second issue is to explore the expressivity of DLs. We believe that our
approach can easily be adapted to fuzzy SI. Additionally, if we restrict to acyclic
TBoxes, we may be able to obtain a PSpace upper bound as in [
Finally, we want to develop an algorithm for deciding `-subsumption. Notice that the residuum cannot, in general, be expressed using the t-norm, t-conorm and negation. Thus, the usual idea of reducing subsumption to satis ability by constructing an equivalent concept cannot be applied.