Description Logics over Lattices with Multi-Valued Ontologies

1 Introduction

Description logics (DLs) [Baader et al., 2003] are a family of logic-based knowledge representation formalisms, which have been employed in various application domains and whose most notable success so far is the adoption of the DLbased language OWL as a standard for the semantic web. However, in their usual form, DLs lack the ability to handle uncertainty. Uncertainty is unavoidable in areas such as medicine, where determining without doubt whether a patient has a specific disease may require intrusive or expensive tests. For example, a full diagnosis for anemia requires a blood test measuring the number of red blood cells and hemoglobin level. However, this test should only be performed if there is some valid reason to suspect an abnormality in these levels. Additionally, when preparing a diagnosis, experts must deal with symptoms reported by the patients, which are by definition subjective, and hence imprecise and incomparable.

Moreover, the relationship between diseases and their external manifestations is rarely clear-cut. For instance, the anemic syndrome may be caused by a very wide range of maladies (undernourishment, leukemia, drepanocytosis, etc.) which may be more or less likely depending on the ethnic origin, gender, or activity of the patient, but none of these factors is fully determinant to the origin of the syndrome.

We propose an extension of classical DLs that can handle uncertainty through multi-valued semantics. In our approach we consider a finite number of truth values, organized in a lattice extended with a negation operator. The semantics of this logic is a standard generalization from classical DLs in the sense that concepts (classically interpreted as sets) are now interpreted as multi-valued sets over the background lattice. The semantics of the concept constructors is also generalized from Boolean to lattice operators.

A previous approach combining DLs with multi-valued semantics based on lattices was presented in [Straccia, 2006], but can only deal with acyclic terminologies containing crisp axioms. Thus, it is unable to express cyclic relations necessary for representing, e.g. hereditary diseases: a patient having a relative with drepanocytosis is likely, but not certain, to exhibit this disorder as well. In this paper we develop reasoning procedures that are able to handle general concept inclusion axioms, which may themselves include a degree of uncertainty. We can then reason over cyclic axioms like 1

〈∃relative.Drepanocytosis ⊑ Drepanocytosis, likely〉 ,

which expresses the fact that drepanocytosis is a hereditary disease, i.e. a patient having a relative with drepanocytosis is likely, but not certain, to exhibit this disorder as well.

In order to present the main ideas of our approach, we restrict ourselves to ALCL, the multi-valued variant of ALC over the lattice L. It should be clear, however, that the same ideas can be transferred to more expressive DLs. We then describe an exponential-time procedure for reasoning in this logic, which is EXPTIME-hard.

In Section 2 we present some basic notions of lattice theory and the logic ALCL with its main reasoning problems. We then show how to reason in this logic on the assumption that it has the witnessed model property. In Section 4 we prove that the witnessed model property may not hold in general, but the algorithm, with minor modifications, remains correct. Finally, in Section 5, we give an overview of the wide range of approaches that have been proposed to deal with uncertainty and imprecision in DL, and compare them to our own. Due to a lack of space we only sketch the proofs of our results.

2 AMulti-valued Description Logic

In this section we first introduce some basic notions of lattice theory and then define the lattice-based multi-valued description logic ALCL.

1 The semantics of this expression can be found in Definition 3.

2.1 Lattices

A lattice is an algebraic structure (L,⊕,⊗) consisting of a carrier set L and two binary operations supremum ⊕ and infimum ⊗ that are commutative and associative, and satisfy the absorption laws ℓ ⊕ (ℓ ⊗ m) = ℓ = ℓ ⊗ (ℓ ⊕ m) for all ℓ,m ∈ L. 2 The order ≤ on L is defined by ℓ ≤ m iff ℓ ⊗ m = ℓ for all ℓ,m ∈ L. A lattice 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. Every finite lattice is also bounded. In a finite lattice, we may use the notation ⊕t∈T t (⊗t∈T t) for the supremum (infimum) of a set T ⊆ L. 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 unary operation ⊖, called negation, that satisfies De Morgan's laws ⊖(ℓ ⊕ m) = ⊖ ℓ ⊗ ⊖m and ⊖(ℓ ⊗m) = ⊖ℓ ⊕ ⊖m for all ℓ,m ∈ L. The negation is an anti-monotone bijection on the lattice. Figure 1 shows a simple De Morgan lattice.

The operators of a De Morgan lattice can be seen as the natural generalization of the logical operators ∨, ∧, and ¬. Based on this intuition, we define the implication of two elements in the lattice as ℓ ⇒ m := ⊖ ℓ ⊕ m.

For the rest of this paper, we assume that L is an arbitrary, but fixed, finite De Morgan lattice. The elements of this lattice will describe the certainty of assertions. For instance, one could use values in a total order (e.g. unlikely, likely, very likely, sure) or use several dimensions to express incomparable values of uncertainty (e.g. subjective measurements made by different sources).

2.2 Multi-valued ALC

The multi-valued description logic ALCL is a generalization of the crisp DL ALC that allows the use of the elements of a 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.

Definition 1 (syntax of ALCL). Let NC and NR be two disjoint sets of concept names and role names, respectively. ALCL concept descriptions are built through the following syntactic rule:

2 See [Gr¨atzer, 1998] for a more detailed introduction to lattices.

where A ∈ NC, r ∈ NR, and C,C1,C2 are ALCL concept descriptions.

The semantics of this logic is given by an interpretation function that not simply describes whether an element of the domain belongs to a concept, but gives a lattice value describing the certainty with which the element satisfies this concept; in other words, the semantics is based on multi-valued sets.

Definition 2 (semantics of ALCL). An interpretation is a pair I = (ΔI , ·I ) where ΔI is a non-empty 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:

• (C ⊓D)I (x) = C I (x) ⊗DI (x),
• (C ⊔D)I (x) = C I (x) ⊕DI (x),
• (¬C)I (x) = ⊖C I (x),
• (∃r.C)I (x) = ⊕y∈ΔI rI (x, y) ⊗C I (y),
• (∀r.C)I (x) = ⊗y∈ΔI rI (x, y) ⇒C I (y),
• ⊤I (x) = 1, ⊥I (x) = 0.

for every x ∈ ΔI .

Notice that the existential and universal quantifiers are dual, i.e. ¬∃r.C and ∀r.¬C have the same semantics for every ALCL concept description C and every role name r.

The knowledge of a domain is usually stored in an ontology, which is a collection of axioms. In this paper, we restrict to terminological knowledge, given by a so-called TBox.

Definition 3 (TBox). A TBox is a finite set of (labeled) general concept inclusions (GCIs) of the form 〈C ⊑ D, ℓ〉, where C, D are ALCL concept descriptions and ℓ ∈ L.

An interpretation I is a model of the TBox T if it satisfies all axioms in T , i.e. if for every axiom 〈C ⊑D, ℓ〉 ∈ T it holds that ⊗x∈ΔI C I (x) ⇒ DI (x) ≥ ℓ.

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. Accordingly, one can think of generalizing the reasoning problems for ALC to the use of other lattices. The standard reasoning problems for crisp DLs are satisfiability and subsumption of concepts. In our setting, we are further interested in the degree of certainty with which these properties hold.

Definition 4 (satisfiability, subsumption). Let C,D be ALCL concept descriptions, T a TBox and ℓ ∈ L. C is ℓ-satisfiable w.r.t. T if there is a model I of T with ⊕x∈ΔI C I (x) ≥ ℓ. The best satisfiability degree for C w.r.t. T is the largest ℓ such that C is ℓ-satisfiable w.r.t. T .

C is ℓ-subsumed by D w.r.t. T if every model I of T is also a model of 〈C ⊑ D, ℓ〉. The best subsumption degree for C and D is the largest ℓ ∈ L such that C is ℓ-subsumed by D w.r.t. T .

Notice that if C is ℓ-satisfiable and ℓ′ -satisfiable w.r.t. T , then C is also ℓ ⊕ ℓ′ -satisfiable. Likewise for ℓ-subsumption. Hence, the notions of best satisfiability and best subsumption degrees are well defined. Moreover, as the following lemma shows, it is sufficient to develop an algorithm for finding the best satisfiability degree of a concept.

Lemma 5. Let C,D be two concept descriptions, T a TBox, and ℓ ∈ L. The best satisfiability degree for C ⊓ ¬D is ℓ iff the best subsumption degree for C and D is ⊖ ℓ.

The best satisfiability degree of a concept is important for medical applications, where a doctor may want to find out how likely a given pathology is. For example, the best satisfiability degree of Male ⊓ Hepatomegalia ⊓ Anemia expresses the likelihood of finding an hepatomegalic male with anemia. In some cases, however, this notion of satisfiability turns out to be too weak, since a concept C may be ℓ-satisfiable even if no element of the domain may ever belong to C with a value greater or equal to ℓ.

Example 6. We use the lattice L3 from Figure 1. The concept A is 1-satisfiable w.r.t. the TBox T having the axioms

since I0 = ({x1, x2}, ·I0 ) with AI0 (x1) = BI0 (x2) = ℓa, BI0 (x1) = AI0 (x2) = ℓc is a model of T and ℓa ⊕ ℓc = 1. However, there is no model I of T where AI (x) = 1 for some x ∈ ΔI . If such I and x existed, then the first axiom would restrict BI (x) to be ≤ ⊖ℓb (either ⊖ℓb or 0), while the second axiom would force this value to be 1.

For this reason, we consider a stronger notion of satisfiability that requires at least one element of the domain to satisfy the concept with the given value. A concept C is strongly ℓ-satisfiable w.r.t. a TBox T if there is a model I of T and an x ∈ ΔI such that C I (x) ≥ ℓ. Obviously, strong ℓ-satisfiability implies ℓ-satisfiability. As shown in Example 6, the converse does not hold. However, satisfiability can be reduced to strong satisfiability by means of the following lemma.

Lemma 7. The best satisfiability degree for C w.r.t. T is the supremum of all ℓ such that C is strongly ℓ-satisfiable.

Proof Sketch. If C is strongly ℓ- and strongly ℓ′ -satisfiable, there exist two models I, I ′ of T and x ∈ Δ, x′ ∈ Δ′ with C I (x) ≥ ℓ and C I ′ (x′ ) ≥ ℓ′ . The disjoint union of I and I ′ gives a model J where ⊕y∈ΔJ C J (y) ≥ ℓ ⊕ ℓ′ .

We can then find out whether C is ℓ-satisfiable by comparing ℓ to the best satisfiability degree of C. We will thus focus on developing an algorithm for finding all the lattice elements that witness the strong satisfiability of a given concept. As we will show, this reasoning problem is not harder than deciding satisfiability of crisp ALC concepts.

3 Deciding Strong Satisfiability

We now present an automata-based algorithm for deciding the strong satisfiability of a concept. To simplify the construction, we first consider reasoning over witnessed models only (see Definition 8). We later show (in Section 4) that this restriction is not necessary for the correctness of the algorithm.

Definition 8 (witnessed model). Let η ∈ N. A model I of a TBox T is called η-witnessed if for every x ∈ ΔI and every concept description of the form ∃r.C there are η elements x1, . . . , xη ∈ ΔI such that

and analogously for the universal restrictions ∀r.C. In particular, if η = 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 will present a procedure to check strong satisfiability w.r.t. witnessed models which is based on the emptiness check of finite automata working on infinite trees. But first, we give a brief introduction to this kind of automata.

As input structure we consider the infinite k-ary tree K∗ for K := {1, . . . , k} with k ∈ N. The positions of the nodes in this tree are represented through words in K∗ in the usual way: the empty word ε represents the root node, and ui represents the i-th successor of the node u.

Definition 9 (looping automaton). A looping automaton (LA) is a tuple (Q, I,Δ) consisting of a finite set Q of states, a set I ⊆ Q of initial states and a transition relation Δ ⊆ Q × Qk .

A run of this automaton is a mapping r : K∗ → Q that assigns states to each node of K∗ such that (i) r(ε) ∈ I and (ii) for every u ∈ K∗ , (r(u), r(u1), . . . , r(uk)) ∈ Δ.

The emptiness problem for LA is to decide whether a given LA has a run.

The emptiness problem for LA can be solved by the following procedure in polynomial time. The idea is to incrementally build the set of all states that cannot appear in any run; we will call these bad states. All states without transitions are clearly bad states, and hence the set is initialized with those states. On each iteration, we add to this set all states that only have transitions leading to bad states. This set becomes stable after at most |Q| iterations. The automaton has a run iff there is an initial state that is not bad. It is worth to point out that, as a side-effect, this procedure computes the set of all non-bad initial states without additional effort.

We now return to the problem of deciding strong ℓsatisfiability of ALCL concept descriptions. Our automatabased approach relies on the fact that a concept is strongly ℓsatisfiable iff it has a well-structured tree model, called a Hintikka tree. Intuitively, Hintikka trees are abstract representations of tree models, that express the membership value of all "relevant" concept descriptions. The automaton will have exactly these Hintikka trees as its runs. Strong ℓ-satisfiability is thus reduced to the emptiness test of an automaton.

In the following we assume that all concept descriptions are in negation normal form (NNF); that is, negation appears only in front of concept names. Any ALCL concept description can be transformed to NNF using the De Morgan rules, duality of quantifiers, and elimination of double negations. We denote the NNF of C by nnf(C) and nnf(¬C) by ∽C. The concept description nnf(C) always has the same semantics as C, since we are using a De Morgan lattice and existential and universal restrictions are dual to each other.

We denote as sub(C, T ) the set of all subconcepts of C and of the concept descriptions ∽ D ⊔ E for 〈D ⊑ E, ℓ〉 ∈ T .

The states of the automaton will be so-called Hintikka sets. Strictly speaking, these are multi-valued sets: every element has an associated membership value from the lattice L. Their domain is the set sub(C, T ), together with an arbitrary element ρ.

Definition 10 (Hintikka set). A function H : sub(C, T ) ∪ {ρ} → L is called a (multi-valued) Hintikka set for C, T if it satisfies the conditions (i) H(D ⊓ E) = H(D) ⊗H(E), (ii) H(D ⊔ E) = H(D) ⊕ H(E), and (iii) for every concept name A, H(¬A) = ⊖H(A).

The Hintikka set H is compatible with the GCI 〈D ⊑ E, ℓ〉 if H(∽D ⊔ E) ≥ ℓ.

The arity k of our automaton is determined by the number of existential and universal restrictions, i.e. concept descriptions of the form ∃r.D or ∀r.D, contained in sub(C, T ). Intuitively, each successor acts as the witness for one of these restrictions. The additional domain element ρ is used to express the degree with which the role relation to the parent node holds. 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 ∃r.D or ∀r.D} → K. The following Hintikka conditions define the transitions of our automaton.

Definition 11 (Hintikka condition). The tuple of Hintikka sets (H0,H1, . . . ,Hk) for C, T satisfies the Hintikka condition if: (i) for every existential restriction ∃r.D, H0(∃r.D) = Hϕ(∃r.D)(ρ) ⊗ Hϕ(∃r.D)(D) and additionally for every restriction F of the form ∃r.E or ∀r.E, it holds H0(∃r.D) ≥ Hϕ(F)(ρ) ⊗ Hϕ(F)(D); and (ii) for every universal restriction ∀r.D, H0(∀r.D) = Hϕ(∀r.D)(ρ) ⇒ Hϕ(∀r.D)(D) and additionally for every restriction F of the form ∃r.E or ∀r.E, it holds H0(∀r.D) ≤ Hϕ(F )(ρ) ⇒ Hϕ(F )(D).

A Hintikka tree for C, T is an infinite k-ary tree T labeled with Hintikka sets that are compatible with every GCI in T where, for every node u ∈ K∗ , the tuple (T(u),T(u1), . . . ,T(uk)) satisfies the Hintikka condition. The compatibility condition 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.

Recall that for now we are only considering reasoning w.r.t. witnessed models, namely, decide whether there is a witnessed model I such that C I (x) ≥ ℓ for some x ∈ ΔI . The proof of the following theorem uses arguments similar to those in [Baader et al., 2008].

Theorem 12. Let C be a concept description and T a TBox. 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. A Hintikka tree can be seen as a witnessed model with domain K∗ and interpretation function given by the Hintikka sets. Thus, any Hintikka tree T for C, T with T(ε)(C) ≥ ℓ entails strong ℓ-satisfiability of C w.r.t. T .

On the other hand, every witnessed model I 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 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 ∃r.D or ∀r.D and finding the witness y ∈ Δ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.

Thus, in order to decide strong ℓ-satisfiability w.r.t. witnessed models, we only need to decide emptiness of the following automaton.

Definition 13 (Hintikka automaton). Let C be an ALCL concept description, T a TBox, and ℓ ∈ L. The Hintikka automaton for C, T , ℓ is the LA AC,T ,ℓ = (Q, I, Δ) where Q is the set of all compatible Hintikka sets for C, T , I contains all Hintikka sets H with H(C) ≥ ℓ, and Δ is the set of all (k + 1)-tuples of compatible 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 ℓ-satisfiable w.r.t. T iff AC,T ,ℓ is non-empty. Since the automaton AC,T ,ℓ is exponential in C, T , and the emptiness test for looping automata is polynomial in the size of the automaton, overall we obtain an exponential time decision procedure for strong ℓsatisfiability. This bound is optimal, because concept satisfiability is already EXPTIME-hard for crisp ALC with general concept inclusions [Baader et al., 2003].

Theorem 14. The problem of deciding strong ℓ-satisfiability (w.r.t. witnessed models) of an ALCL concept description C w.r.t. a TBox T is EXPTIME-complete.

Furthermore, the emptiness test described before can be used to compute the set of all Hintikka sets that may appear at the root of a Hintikka tree. From this we can extract the set of all values ℓ such that T(ϵ)(C) ≥ ℓ for some Hintikka tree T. From Lemma 7 it then follows that the best satisfiability degree for C w.r.t. T can also be computed in exponential time. By Lemma 5, all of the reasoning problems defined in this paper are EXPTIME-complete.

We emphasize here that this complexity analysis does not consider the underlying lattice L as part of the input. This is a reasonable assumption as, for any given application, the lattice will never be modified, and hence all the lattice-based operations can be hardcoded to be performed in constant time. However, if the size of the lattice is measured as the number of its elements, then the algorithm is also exponential in this value, since all the lattice operations can be performed in polynomial time in this size.

4 DealingWithMoreWitnesses

The use of the Hintikka automata from Definition 13 for deciding strong ℓ-satisfiability is only correct if ALCL has the witnessed model property, i.e. every strongly ℓ-satisfiable concept is also strongly ℓ-satisfiable w.r.t. witnessed models. However, this property does not hold in general.

Example 15. Consider the lattice L3 and the TBox T from Example 6. If we extend the interpretation I0 from the same example such that rI0 (x1, x1) = rI0 (x1, x2) = 1, then we see that ∃r.A is strongly 1-satisfiable. However, in any witnessed model I, the strong 1-satisfiability of this concept would imply the existence of an individual x such that AI (x) = 1, which was shown to be impossible in Example 6.

Nonetheless, there is always a constant η ∈ N, depending only on the underlying lattice L, such that ALCL has the ηwitnessed model property; i.e. strong ℓ-satisfiability is equivalent to strong ℓ-satisfiability w.r.t. η-witnessed models. The number η depends on the compactness degree of L.

Definition 16 (compactness). Let η ∈ N. A lattice L is called η-compact if for every A ⊆ L there is a subset B ⊆ A with at most η elements such that ⊕ B = ⊕ A. The compactness degree of L is the smallest η for which L is ηcompact.

The following lemma states that the compactness degree yields a bound on the number of successors that witness any existential and universal restriction. It is an easy consequence of Definitions 8 and 16.

Lemma 17. Let L be a finite De Morgan lattice and η ∈ N. If L is η-compact, then ALCL has the η-witnessed model property.

Moreover, the compactness degree of a given lattice L is bounded by the width of L, i.e. the cardinality of the longest antichain of L.

Lemma 18. If L has width η ∈ N, then L is η-compact.

Proof. If a set A ⊆ L contains two comparable elements, then we can always remove one of them without affecting the supremum of A.

This implies that ALCL always has the η-witnessed model property for some η ∈ N, since we assumed L to be finite. From Lemma 18 we deduce that every total order is 1-compact. Consequently, if L is a finite total order with De Morgan negation, then ALCL has the witnessed model property. This is the case, e.g. for fuzzy ALC based on the Zadeh fuzzy operations [Straccia, 2001].

The constructions of the previous section can easily be adapted for η-witnessed models. We can introduce the notion of η-witnessed Hintikka trees and construct looping automata Aη,C,T ,ℓ such that the following are equivalent: (i) C is strongly ℓ-satisfiable w.r.t. T (in an η-witnessed model), (ii) there is an η-witnessed Hintikka tree T for C, T such that T(ε)(C) ≥ ℓ, and (iii) the LA Aη,C,T ,ℓ is non-empty. The main difference lies in the arity k of the Hintikka trees. Thus, a similar algorithm can be applied even if the logic does not have the witnessed model property.

Theorem 19. The problem of deciding strong ℓ-satisfiability of an ALCL concept description C w.r.t. a TBox T is EXPTIME-complete.

As before, the complexity of this problem does not change if we do not view the lattice L as fixed, but measure its size as the number of its elements.

5 RelatedWork

Several different formalisms have so far been suggested for dealing with uncertainty or vagueness in DL ontologies.

In [Straccia, 2006], a similar approach to the one presented here was taken. The description logic ALC is augmented by multi-valued interpretations over a De Morgan lattice. The difference to our approach lies in the treatment of axioms. In [Straccia, 2006], the TBox axiom C ⊑ D is satisfied by an interpretation I if C I (x) ≤ DI (x) holds for all x ∈ ΔI . Additionally, only acyclic TBoxes are allowed, and thus, all defined concepts can be expanded beforehand. This eliminates the need to deal with the TBox in the algorithm that checks satisfiability. Consequently, the presented tableaux algorithm only checks ABox consistency in ALCL w.r.t. an empty TBox. Our approach using automata allows us to deal with arbitrary TBox axioms expressing, e.g. hereditary diseases; on the other hand, we do not consider ABox axioms. [Jiang et al., 2010] extend the work of [Straccia, 2006] to the more expressive DL SHIN. However, they limit the expressivity of the terminological axioms in the same way.

Fuzzy DLs are another way to deal with uncertainty in ontologies [Yen, 1991; Lukasiewicz and Straccia, 2008]. These formalisms apply the ideas of fuzzy sets [Zadeh, 1965] to description logics. Concepts are interpreted as mappings from the domain into the unit interval [0, 1]. Depending on the underlying logical operators, the logics differ in the interpretation of the concept constructors. However, the total order [0, 1] does not allow for incomparable degrees of uncertainty as our approach does.

Our definition of ALCL includes the fuzzy DL with Zadeh semantics and Kleene-Dienes-implication [Straccia, 2001; Stoilos et al., 2007]. In this case, the semantics is as that of ALCL for the De Morgan lattice L = ([0, 1],max,min) with negation x ↦→ 1 - x. Although this lattice is not finite, once the TBox is fixed we can restrict ourselves w.l.o.g. to a finite subset of [0, 1], as max and min create no new values. The tableau algorithm that was developed for reasoning in fuzzy ALC with Zadeh semantics and general TBoxes generalizes the well-known algorithm for crisp ALC and may thus require non-deterministic exponential time in the worst case. Our algorithm improves on this by giving an EXPTIME upper bound, thus proving EXPTIME-completeness of the problem for the first time. Since our approach satisfies desirable properties such as idempotency of conjunction and duality of quantifiers, it is unable to treat more complex t-norm based semantics [Bobillo and Straccia, 2009a].

A different way to enrich DLs with uncertainty is to follow the approach of rough set theory [Pawlak, 1982]. The basic idea of rough DLs [Schlobach et al., 2007; Keet, 2010] is that some concepts cannot be described precisely, but only by some lower and upper approximation. The semantics of this logic requires, in addition to the interpretation of the different concepts, an equivalence relation, called indiscernibility, on the elements of the domain, which is used to formalize these approximations. This formalism assumes that one can specify a global indiscernibility relation on the domain, whereas the idea behind multi-valued DLs is that one is able to locally specify a membership degree for each individual. The authors show that the rough set semantics can be translated to classical DL. This is predicated on the existence of transitivity, symmetry and reflexivity axioms for roles, which do not exist in ALC. In any DL that includes these axioms, one can easily translate the indiscernibility equivalence relation of rough set theory into a special role without adding to the complexity of reasoning. However, for ALC this reduction yields a strict increase in complexity. Efforts have also been made to combine the approaches of rough set theory and fuzzy logic into a single description logic [Bobillo and Straccia, 2009b].

6 Conclusions

We presented a general framework for reasoning under uncertainty based on the description logic ALC. We considered the reasoning tasks of deciding ℓ-satisfiability and ℓ-subsumption as well as computing the best satisfiability and subsumption degrees w.r.t. general TBoxes. It turns out that these reasoning tasks are in the same complexity class as for the crisp DL ALC. In [Straccia, 2006] it was shown that satisfiability w.r.t. crisp acyclic TBoxes is PSPACE-complete.

To our knowledge, this is the first time that automatabased techniques were used to analyze reasoning in DLs augmented by De Morgan lattices. This enabled us to treat the case of general concept inclusions instead of the simpler acyclic TBoxes. Although we did not consider reasoning w.r.t. ABoxes, it is clear that a preprocessing method similar to the one presented in [Hollunder, 1996], combining the tableaux algorithm developed in [Straccia, 2006] with this automata-based approach, would allow for the simultaneous treatment of ABoxes and general TBoxes. We also plan to extend our approach to more expressive DLs, as was already done for reasoning w.r.t. crisp TBoxes in [Jiang et al., 2010]. Considering the close relationship between the automaton deciding satisfiability in ALC and our approach, we believe that a similar argument can be used to show that multi-valued SI is PSPACE-complete with acyclic TBoxes and EXPTIMEcomplete with general TBoxes [Baader et al., 2008].

It would also be interesting to see whether concept modifiers (e.g. (very)Tall) can be treated in this framework. Additionally, one may consider an implication different from the one we used here, e.g. the residuum of the infimum ⊗.

The advantage of description logics over more expressive logical formalism has always been the feasibility for implementation. Regarding the treatment of uncertainty, there are several possible ways to implement reasoning procedures. One could implement a completely new system or augment an existing system like RACER 3 or FaCT++ 4 to deal with multi-valued instead of crisp semantics.

Furthermore, it may be possible to reduce reasoning in ALCL to reasoning in ALC. This has already been done for fuzzy DLs [Straccia, 2004] and multi-valued DLs based on linear orders [Straccia, 2006]. The advantage of this approach is that one can reuse existing optimized reasoners for crisp DLs. However, it remains to be seen whether this is feasible for arbitrary De Morgan lattices. Finally, one could also use a straightforward translation of ALCL into a multi-valued first order language and use existing reasoners for these more expressive formalisms, e.g. 3TAP. 5

3 http://www.racer-systems.com/

4 http://owl.man.ac.uk/factplusplus

5 http://i12www.ira.uka.de/threetap