GCIs Make Reasoning in Fuzzy DL with the Product T-norm Undecidable Franz Baader and Rafael Peñaloza Theoretical Computer Science, TU Dresden, Germany {baader,penaloza}@tcs.inf.tu-dresden.de 1 Introduction Fuzzy variants of Description Logics (DLs) were introduced in order to deal with applications where not all concepts can be defined in a precise way. A great variety of fuzzy DLs have been investigated in the literature [12,8]. In fact, compared to crisp DLs, fuzzy DLs offer an additional degree of freedom when defining their expressiveness: in addition to deciding which concept constructors (like conjunction, disjunction, existential restriction) and which TBox formalism (like no TBox, acyclic TBox, general concept inclusions) to use, one must also decide how to interpret the concept constructors by appropriate functions on the domain of fuzzy values [0, 1]. For example, conjunction can be interpreted by different t-norms (such as Gödel, Łukasiewicz, and product) and there are also different options for how to interpret negation (such as involutive negation and residual negation). In addition, one can either consider all models or only so-called witnessed models [10] when defining the semantics of fuzzy DLs. Decidability of fuzzy DLs is often shown by adapting the tableau-based algo- rithms for the corresponding crisp DL to the fuzzy case. This was first done for the case of DLs without general concept inclusion axioms (GCIs) [19,17,14,6], but then also extended to GCIs [16,15,18,4,5]. Usually, these tableau algorithms reason w.r.t. witnessed models.1 It should be noted, however, that in the pres- ence of GCIs there are different ways of extending the notion of witnessed models from [10], depending on whether the witnessed property is required to apply also to GCIs (in which case we talk about strongly witnessed models) or not (in which case we talk about witnessed models). The paper [4] considers the case of reasoning w.r.t. fuzzy GCIs in the set- ting of a logic with product t-norm and involutive negation. More precisely, the tableau algorithm introduced in that paper is supposed to check whether an on- tology consisting of fuzzy GCIs and fuzzy ABox assertions expressed in this DL has a strongly witnessed model or not.2 Actually, the proof of correctness of this algorithm given in [4] implies that, whenever such an ontology has a strongly witnessed model, then it has a finite model. However, it was recently shown in [2] 1 In fact, witnessed models were introduced in [10] to correct the proof of correctness for the tableau algorithm presented in [19]. 2 Note that the authors of [4] actually use the term “witnessed models” for what we call “strongly witnessed models.” that this is not the case in the presence of general concept inclusion axioms, i.e., there is an ontology written in this logic that has a strongly witnessed model, but does not have a finite model. Of course, this does not automatically imply that the algorithm itself is wrong. In fact, if one applies the algorithm from [4] to the ontology used in [2] to demonstrate the failure of the finite model property, then one obtains the correct answer, and in [2] the authors actually conjecture that the algorithm is still correct. However, incorrectness of the algorithm has now independently been shown in [3] and in [1]. Thus, one can ask whether the fuzzy DL considered in [4] is actually decidable. Though this question is not answered in [1], the paper gives strong indications that the answer might in fact be “no.” More precisely, [1] contains a proof of undecidability for a variant of the fuzzy DL considered in [4], which (i) additionally allows for strict GCIs, i.e., GCIs whose fuzzy value is required to be strictly greater than a given rational number; and (ii) where the notion of strongly witnessed models used in [4] is replaced by the weaker notion of witnessed models. In this paper, we consider a different fuzzy DL with product t-norm, where disjunction and involutive negation are replaced by the constructor implication, which is interpreted as the residuum. In this logic, residual negation can be expressed, but neither involutive negation nor disjunction. It was introduced in [10], where decidability of reasoning w.r.t. witnessed models was shown for the case without GCIs. In [7], an analogous decidability result was shown for the case of reasoning w.r.t. so-called quasi-witnessed models. Following [7], we call this logic ∗-ALE. In the present paper we show that adding GCIs makes reasoning in ∗-ALE undecidable w.r.t. several variants of the notion of witnessed models (including witnessed, quasi-witnessed, and strongly witnessed models). 2 Preliminaries In this section, we introduce the logic ∗-ALE and some of the properties that will be useful throughout the paper. The syntax of this logic is slightly different from standard description logics, as it allows for an implication constructor, and no negation or disjunction. ∗-ALE concepts are built through the syntactic rule C ::= A | ⊥ | > | C1 u C2 | C1 → C2 | ∃r.C | ∀r.C where A is a concept name and r is a role name. A ∗-ALE ABox is a finite set of assertion axioms of the form ha : C B qi or h(a, b) : r B qi, where C is a ∗-ALE concept, r ∈ NR , q is a rational number in [0, 1], a, b are individual names and B is either ≥ or =. A ∗-ALE TBox is a finite set of concept inclusion axioms of the form hC v D ≥ qi, where C, D are ∗-ALE concepts and q is a rational number in [0, 1]. A ∗-ALE ontology is a tuple (A, T ), where A is a ∗-ALE ABox and T a ∗-ALE TBox. In the following we will often drop the prefix ∗-ALE, and speak simply of e.g. TBoxes and ontologies. The semantics of this logic extends the classical DL semantics by interpreting concepts and roles as fuzzy sets over an interpretation domain. Given a non- empty domain ∆, a fuzzy set is a function F : ∆ → [0, 1], with the intuition that an element δ ∈ ∆ belongs to F with degree F (δ). Here, we focus on the product t-norm semantics, where logical constructors are interpreted using the product t-norm ⊗ and its residuum ⇒ defined, for every α, β ∈ [0, 1], as follows: α ⊗ β := α · β, ( 1 if α ≤ β α ⇒ β := β/α otherwise. The semantics of ∗-ALE is based on interpretations. An interpretation is a tuple I = (∆I , ·I ) where ∆I is a non-empty set, called the domain, and the function ·I maps each individual name a to an element of ∆I , each concept name A to a function AI : ∆I → [0, 1] and each role name r to a function rI : ∆I × ∆I → [0, 1]. The interpretation function is extended to arbitrary ∗-ALE concepts as follows. For every δ ∈ ∆I , >I (δ) = 1, ⊥I (δ) = 0, (C1 u C2 )I (δ) = C1I (δ) ⊗ C2I (δ) (C1 → C2 )I (δ) = C1I (δ) ⇒ C2I (δ) (∃r.C)I (δ) = sup rI (δ, γ) ⊗ C I (γ) γ∈∆I (∀r.C) (δ) = inf rI (δ, γ) ⇒ C I (γ). I γ∈∆I The interpretation I = (∆I , ·I ) satisfies the assertional axiom ha : C B qi iff C (aI ) B q, it satisfies h(a, b) : r B qi iff rI (aI , bI ) B q and it satisfies the concept I inclusion hC v D ≥ qi iff inf δ∈∆I (C I (δ) ⇒ DI (δ)) ≥ q. This interpretation is called a model of the ontology O if it satisfies all the axioms in O. In fuzzy DLs, reasoning is often restricted to witnessed models [10]. An in- terpretation I is called witnessed if it satisfies the following two conditions: (wit1) for every δ ∈ ∆I , role r and concept C there exists γ ∈ ∆I such that (∃r.C)I (δ) = rI (δ, γ) ⊗ C I (γ), and (wit2) for every δ ∈ ∆I , role r and concept C there exists γ ∈ ∆I such that (∀r.C)I (δ) = rI (δ, γ) ⇒ C I (γ). This model is called weakly witnessed if it satisfies (wit1) and quasi-witnessed if it satisfies (wit1) and the condition (wit2’) for every δ ∈ ∆I , role r and concept C, either (∀r.C)I = 0 or there exists γ ∈ ∆I such that (∀r.C)I (δ) = rI (δ, γ) ⇒ C I (γ). In the presence of GCIs, witnessed interpretations are sometimes further restricted [6,2,8] to satisfy (wit3) for every two concepts C, D, there is a γ such that inf (C I (η) ⇒ DI (η)) = C I (γ) ⇒ DI (γ). η∈∆I Witnessed interpretations that satisfy this third restriction (wit3) are called strongly witnessed interpretations. We say that an ontology O is consistent (resp. weakly witnessed consistent, quasi-witnessed consistent, witnessed consistent, strongly witnessed consistent) if it has a model (resp. a weakly witnessed model, a quasi-witnessed model, a witnessed model, a strongly witnessed model). Obviously, strongly witnessed consistency implies witnessed consistency, which implies quasi-witnessed consis- tency, which itself implies weakly witnessed consistency. The converse implica- tions, however, need not hold; for instance, a quasi-witnessed consistent ∗-ALE ontology that has no witnessed models can be derived from the example in [7]. We now describe some properties of t-norms and axioms that will be useful for the rest of the paper. For every α, β ∈ [0, 1] it holds that α ⇒ β = 1 iff α ≤ β. Thus, given two concepts C, D, the axiom hC v D ≥ 1i expresses that C I (δ) ≤ DI (δ) for all δ ∈ ∆I . Additionally, 1 ⇒ β = β and 0 ⇒ β = 1 for all β ∈ [0, 1], and α ⇒ 0 = 0 for all α ∈ (0, 1]. r In the following, we will use the expression hC Di to abbreviate the axioms hC v ∀r.D ≥ 1i , h∃r.D v C ≥ 1i. To understand this abbreviation, consider an r interpretation I satisfying hC Di and let δ, γ ∈ ∆I with rI (δ, γ) = 1. From the first axiom it follows that C I (δ) ≤ (∀r.D)I (δ) = inf rI (δ, η) ⇒ DI (η) η∈∆I ≤ rI (δ, γ) ⇒ DI (γ) = 1 ⇒ DI (γ) = DI (γ). From the second axiom it follows that C I (δ) ≥ (∃r.D)I (δ) = sup rI (δ, η) · DI (η) η∈∆I ≥ rI (δ, γ) · DI (γ) = DI (γ), and hence, both axioms together imply that C I (δ) = DI (γ). In other words, r hC Di expresses that the value of C I (δ) is propagated to the valuation of the concept D on all r successors with degree 1 of δ. Conversely, given an interpretation I such that rI (δ, γ) ∈ {0, 1} for all δ, γ ∈ ∆I , if rI (δ, γ) = 1 r implies C I (δ) = DI (γ), then I is a model of hC Di. For a concept C, and a natural number n ≥ 1, the expression C n will denote n the concatenation of C with itself n times; that is, C n := u C. The semantics j=1 of u yields (C n )I (δ) = (C I (δ))n , for every model I and δ ∈ ∆I . We will show that consistency of ∗-ALE ontologies w.r.t. the different variants of witnessed models introduced above is undecidable. We will show this using a reduction from the Post correspondence problem, which is well-known to be undecidable [13]. Definition 1 (PCP). Let (v1 , w1 ), . . . , (vm , wm ) be a finite list of pairs of words over an alphabet Σ = {1, . . . , s}, s > 1. The Post correspondence problem (PCP) asks whether there is a non-empty sequence i1 , i2 , . . . , ik , 1 ≤ ij ≤ m such that vi1 vi2 · · · vik = wi1 wi2 · · · wik . If such a sequence exists, then the word i1 i2 · · · ik is called a solution of the problem. We assume w.l.o.g. that there is no pair vi , wi where both words are empty. For a word µ = i1 i2 · · · ik ∈ {1, . . . , m}∗ , we will denote as vµ and wµ the words vi1 vi2 · · · vik and wi1 wi2 · · · wik , respectively. The alphabet Σ consists of the first s positive integers. We can thus view every word in Σ ∗ as a natural number represented in base s + 1 in which 0 never occurs. Using this intuition, we will express the empty word as the number 0. In the following reductions, we will encode the word w in Σ ∗ using the number −w 2 ∈ [0, 1]. We will construct an ontology whose models encode the search for a solution. The interpretation of two designated concept names A and B at a node will correspond to the words vµ , wµ , respectively, for µ ∈ {1, . . . , m}∗ . 3 Undecidability w.r.t. Witnessed Models We will show undecidability of consistency w.r.t. witnessed models by construct- ing, for a given instance P = ((v1 , w1 ), . . . , (vm , wm )) of the PCP, an ontology OP such that for every witnessed model I of OP and every µ ∈ {1, . . . , m}∗ there is an element δµ ∈ ∆I with AI (δµ ) = 2−vµ and B I (δµ ) = 2−wµ . Additionally, we will show that this ontology has a witnessed model whose domain has only these elements. Then, P has a solution iff for every witnessed model I of OP there exist a δ ∈ ∆I such that AI (δ) = B I (δ). Let δ ∈ ∆I encode the words v, w ∈ Σ ∗ ; i.e., AI (δ) = 2−v and B I (δ) = 2−w , and let i, 1 ≤ i ≤ m. Assume additionally that we have concept names Vi , Wi with ViI (δ) = 2−vi and WiI (δ) = 2−wi . We want to ensure the existence of a node γ that encodes the concatenation of the words v, w with the i-th pair from P; i.e. vvi and wwi . This is done through the TBox |vi | ri |wi | ri TPi := {h> v ∃ri .> ≥ 1i , h(Vi u A(s+1) ) Ai, h(Wi u B (s+1) ) Bi}. Recall that we are viewing words in Σ ∗ as natural numbers in base s + 1. Thus, 0 the concatenation of two words u, u0 corresponds to the operation u·(s+1)|u | +u0 . We then have that |vi | |vi | (Vi u A(s+1) )I (δ) = ViI (δ) · (AI (δ))(s+1) = 2−vvi . If I is a witnessed model of TPi , then from the first axiom it follows that (∃ri .>)I (δ) = 1, and according to (wit1), there must exist a γ ∈ ∆I with rI (δ, γ) = 1. The last two axioms then ensure that AI (γ) = 2−vvi and B I (γ) = 2−wwi ; thus, the concept names A and B encode, at node γ, the words vvi and wwi , as desired. If we want to use this construction to recursively construct all the pairs of concatenated words defined by P, we need to ensure also that VjI (γ) = 2−vj , WjI (γ) = 2−wj hold for every j, 1 ≤ j ≤ m. This can be done through the axioms ri ri TP0 := {hVj Vj i, hWj Wj i | 1 ≤ i, j ≤ m}. It only remains to ensure that there is a node δε where AI (δε ) = B I (δε ) = 1 = 20 (that is, where A and B encode the empty word) and VjI (δε ) = 2−vj , WjI (δε ) = 2−wj hold for every j, 1 ≤ i ≤ m. This condition is easily enforced through the ABox3 A0P := {ha : A = 1i , ha : B = 1i} ∪ { a : Vi = 2−vi , a : Wi = 2−wi | 1 ≤ i ≤ m}. Finally, we include a concept name H that must be interpreted as 0.5 in every domain element. This is enforced by the following axioms: A0 := {ha : H = 0.5i}, ri T0 := {hH Hi | 1 ≤ i ≤ m}. This concept name will later be used to detect whether P has a solution (see Theorem 3). Sm Let now OP := (AP , TP ) where AP = A0P ∪ A0 and TP := T0 ∪ i=0 TPi . We define the interpretation IP := (∆IP , ·IP ) as follows: – ∆IP = {1, . . . , m}∗ , – aIP = ε, for every µ ∈ ∆IP , – AIP (µ) = 2−vµ , B IP (µ) = 2−wµ , H IP (µ) = 0.5, and for all j, 1 ≤ j ≤ m – VjIP (µ) = 2−vj , WjIP (µ) = 2−wj , and – rjIP (µ, µj) = 1 and rjIP (µ, µ0 ) = 0 if µ0 6= µj. It is easy to see that IP is in fact a witnessed model of OP , since every node has exactly one ri successor with degree greater than 0, for every i, 1 ≤ i ≤ m. More interesting, however, is that for every witnessed model I of OP , there is an homomorphism from IP to I as described in the following lemma. Lemma 2. Let I be a witnessed model of OP . Then there exists a function f : ∆IP → ∆I such that, for every µ ∈ ∆IP , C IP (µ) = C I (f (µ)) holds for every concept name C and riI (f (µ), f (µi)) = 1 holds for every i, 1 ≤ i ≤ m. Proof. The function f is built inductively on the length of µ. First, as I is a model of AP , there must be a δ ∈ ∆I such that aI = δ. Notice that AP fixes the interpretation of all concept names on δ and hence f (ε) = δ satisfies the condition of the lemma. 3 Notice that equality is necessary for this construction; since there is no negation constructor, it is not possible to express ha : X = qi with q < 1 using only axioms of the form ha : Y ≥ q 0 i. Let now µ be such that f (µ) has already been defined. By induction, we can assume that AI (f (µ)) = 2−vµ , B I (f (µ)) = 2−wµ , H I (f (µ)) = 0.5, and for every j, 1 ≤ j ≤ m, VjI (f (µ)) = 2−vj , WjI (f (µ)) = 2−wj . Since I is a witnessed model of h> v ∃ri .> ≥ 1i, for all i, 1 ≤ i ≤ m there exists a γ ∈ ∆I with r rI (f (µ), γ) = 1, and as I satisfies all the axioms of the form hC Di ∈ TP , it follows that AI (γ) = 2−vµ vi = 2−vµi , B I (γ) = 2−wµ wi = 2−wµi , H I (γ) = 0.5 and for all j, 1 ≤ j ≤ m, VjI (γ) = 2−vj , WjI (γ) = 2−wj . Setting f (µi) = γ thus satisfies the required property. t u From this lemma it follows that, if the PCP P has a solution µ for some µ ∈ {1, . . . , m}+ , then every witnessed model I of OP contains a node δ = f (µ) such that AI (δ) = B I (δ); that is, where A and B encode the same word. Conversely, if every witnessed model contains such a node, then in particular IP does, and thus P has a solution. The question is now how to detect whether a node with this characteristics exists in every model. We will extend OP with axioms that further restrict IP to satisfy AIP (µ) 6= B IP (µ) for every µ ∈ {1, . . . , m}+ . This will ensure that the extended ontology will have a model iff P has no solution. Suppose for now that, for some µ ∈ {1, . . . , m}∗ , it holds that 2−vµ = AIP (µ) > B IP (µ) = 2−wµ . We then have that vµ < wµ and hence wµ − vµ ≥ 1. It thus follows that (A → B)IP (µ) = 2−wµ /2−vµ = 2−(wµ −vµ ) ≤ 2−1 = 0.5 and thus ((A → B) u (B → A))IP (µ) ≤ 0.5. Likewise, if AIP (µ) < B IP (µ), we also get ((A → B) u (B → A))IP (µ) ≤ 0.5. Additionally, if AIP (µ) = B IP (µ), then it is easy to verify that ((A → B) u (B → A))IP (µ) = 1. From all this it follows that, for every µ ∈ {1, . . . , m}∗ , AIP (µ) 6= B IP (µ) iff ((A → B) u (B → A))IP (µ) ≤ 0.5. (1) Thus, the instance P has no solution iff for every µ ∈ {1, . . . , m}+ it holds that ((A → B) u (B → A))IP (µ) ≤ 0.5. 0 We define now the ontology OP := (AP , TP0 ) where TP0 := TP ∪ {h> v ∀ri .(((A → B) u (B → A)) → H) ≥ 1i | 1 ≤ i ≤ m}. 0 Theorem 3. The instance P of the PCP has a solution iff the ontology OP is not witnessed consistent. Proof. Assume first that P has a solution µ = i1 · · · ik and let u = vµ = wµ and µ0 = i1 i2 · · · ik−1 ∈ {1, . . . , m}∗ . Suppose there is a witnessed model I of OP 0 . 0 Since OP ⊆ OP , I must also be a model of OP . From Lemma 2 it then follows that there are nodes δ, δ 0 ∈ ∆I such that AI (δ) = AIP (µ) = B IP (µ) = B I (δ) and riIk (δ 0 , δ) = 1. Then, ((A → B) u (B → A))I (δ) = 1 and hence (((A → B) u (B → A)) → H)I (δ) = 1 ⇒ 0.5 = 0.5. This then means that (∀rik .(((A → B) u (B → A)) → H))I (δ 0 ) ≤ 0.5, violating one of the axioms in TP0 . Hence I is cannot be a model of OP 0 . 0 For the converse, assume that OP is not witnessed consistent. Then IP is not 0 a model of OP . Since it is a model of OP , there must exist an i, 1 ≤ i ≤ m such that IP violates the axiom h> v ∀ri .(((A → B) u (B → A)) → H) ≥ 1i. This means that there is some µ ∈ {1, . . . , m}∗ such that (∀ri .(((A → B) u (B → A)) → H))IP (µ) < 1. Since riIP (µ, µ0 ) = 0 for all µ0 6= µi and riIP (µ, µi) = 1, this implies that (((A → B) u (B → A)) → H)IP (µi) < 1, i.e. ((A → B) u (B → A))IP (µi) > 0.5. From (1) it follows that AIP (µi) = B IP (µi) and hence µi is a solution of P. t u Corollary 4. Witnessed consistency of ∗-ALE ontologies is undecidable. Notice that in the proofs of Lemma 2 and Theorem 3, the second condition of the definition of witnessed models was never used. Moreover, the witnessed interpretation IP is obviously also weakly witnessed. We thus have the following corollary. Corollary 5. Weakly witnessed consistency and quasi-witnessed consistency of ∗-ALE ontologies are undecidable. 4 Undecidability w.r.t. Strongly Witnessed Models Unfortunately, the model IP constructed in the previous section is not a strongly witnessed model of OP since, for instance, inf η∈∆IP (>IP (η) ⇒ AIP (η)) = 0, but there is no δ ∈ ∆IP with AIP (δ) = 0. Thus, the construction of OP does not yield an undecidability result for strongly witnessed consistency in ∗-ALE. Thus, we need a new reduction that proves undecidability of strongly wit- nessed consistency. This reduction will follow a similar idea to the one used in the previous section, in which models describe a search for a solution of the PCP P. However, rather than building the whole search tree, models will describe only individual branches of this tree. The condition (wit3) will be used to ensure that at some point in this branch a solution is found. Before describing the reduction in detail, we recall a property of t-norms. From a t-norm ⊗ and residuum ⇒, one can express the minimum and maximum operators as follows [9]: – min(α, β) = α ⊗ (α ⇒ β), – max(α, β) = min(((α ⇒ β) ⇒ β), ((β ⇒ α) ⇒ α)). We can thus introduce w.l.o.g. the ∗-ALE concept constructor max with the obvious semantics. We will use this constructor to simulate the non-deterministic choices in the search tree as described next. Given an instance P = ((v1 , w1 ), . . . , (vm , wm )) of the PCP, we define the ABox A0P and the TBox TP0 as in the previous section, and for every i, 1 ≤ i ≤ m we construct the TBox |vi | ri |wi | ri T s iP := {hCi v ∃ri .> ≥ 1i , hVi u A(s+1) Ai, hWi u B (s+1) Bi}. The only difference between the TBoxes TPi and T s iP is in the first axiom. In- tuitively, the concept names Ci encode the choice of the branch in the tree to be expanded. If CiI (δ) = 1, there will be an ri successor with degree 1, and the i-th branch of the tree will be explored. For this intuition to work, we need to ensure that at least one of the Ci s is interpreted as 1 in every node. On the other hand, we can stop expanding the tree once a solution has been found. Using this s intuition, we define the ontology OP := (AsP , TPs ) where AsP := A0P ∪ {a : max(C1 , . . . , Cm ) = 1}, m [ TPs := TP0 ∪ T s iP ∪ {h(A u B) → ⊥ v ⊥ ≥ 1i} ∪ i=1 {h> v ∀ri . max((A → B) u (B → A), C1 , . . . , Cm ) ≥ 1i | 1 ≤ i ≤ m}. s Theorem 6. The instance P of the PCP has a solution iff the ontology OP is strongly witnessed consistent. Proof. Let ν = i1 i2 · · · ik be a solution of P and let pre(ν) denote the set of all prefixes of ν. We build the finite interpretation IPs as follows: s – ∆IP := pre(ν), s – aIP = ε, s for all µ ∈ ∆IP , s s – AIP (µ) = 2−vµ , B IP (µ) = 2−wµ , and for all j, 1 ≤ j ≤ m Is Is – Vj P (µ) = 2−vj , Wj P (µ) = 2−wj , Is Is – Cj P (µ) = 1 if µj ∈ pre(ν) and Cj P (µ) = 0 otherwise, and Is Is – rj P (µ, µj) = 1 if µj ∈ pre(ν) and rj P (µ, µ0 ) = 0 if µ0 ∈ pre(ν) and µ0 6= µj. We show now that IPs is a model of OP s . Since IPs is finite, it follows imme- diately that it is also strongly witnessed. Clearly IPs satisfies all axioms in Is A0P ; additionally, we have that Ci1P (ε) = 1 and thus, IPs satisfies AsP . The s axiom h(A u B) → ⊥ v ⊥ ≥ 1i expresses that (A u B)IP (µ) ⇒ 0 = 0, and s IP hence (A u B) (µ) > 0 for all µ ∈ pre(ν), which clearly holds. We now show that the rest of the axioms are also satisfied for every µ ∈ pre(ν). Let µ ∈ pre(ν) \ {ν}. Then we know that there exists i, 1 ≤ i ≤ m such that Is Is Ci P (µ) = 1 and ri P (µ, µi) = 1; thus IPs satisfies the axioms in T s iP . Moreover, Is Is Cj P (µ) = 0 = rj P (µ, µ0 ) for all j 6= i and all µ0 ∈ pre(ν) which means that IPs trivially satisfies all axioms in T s jP . s If µi = ν, then as ν is a solution ((A → B) u (B → A))IP (µi) = 1; otherwise, s I there is a j, 1 ≤ j ≤ m with µij ∈ pre(ν) and thus Cj P (µi) = 1. This means Is that IPs satisfies the last axioms in TPs . Finally, if µ = ν, then ri P (µ, µ0 ) = 0 and Ci (µ) = 0, for all µ0 ∈ pre(ν), 1 ≤ i ≤ m, and thus the axioms are all trivially satisfied. s For the converse, let I be a strongly witnessed model of OP . Then, there must I I be an element δ0 ∈ ∆ with a = δ0 . Since I must satisfy all axioms in AsP , there is an i1 , 1 ≤ i1 ≤ m such that CiI1 (δ0 ) = 1. Since it must satisfy the axioms in T s iP1 , there must exist a δ1 ∈ ∆I with riI1 (δ0 , δ1 ) = 1, AI (δ1 ) = 2−vi1 , and B I (δ1 ) = 2−wi1 . If AI (δ1 ) = B I (δ1 ), then i1 is a solution of P. Otherwise, from the last set of axioms in TPs , there must exist an i2 , 1 ≤ i2 ≤ m with CiI2 (δ1 ) = 1. We can then iterate this same process to generate a sequence i3 , i4 , . . . of indices and δ2 , δ3 , . . . ∈ ∆I where AI (δk ) = 2−vi1 ···vik , and B I (δk ) = 2−wi1 ···wik . If there is some k such that AI (δk ) = B I (δk ), then i1 · · · ik is a solution of P. Assume now that no such k exists. We then have an infinite sequence of indices i1 , i2 , . . . and since for every i, 1 ≤ i ≤ m either vi 6= 0 or wi 6= 0, then at least one of the sequences vi1 · · · vik , wi1 · · · wik diverges. Thus, for every natural number n there is a k such that either vi1 · · · vik > n or wi1 · · · wik > n; equivalently, (A u B)I (δk ) < 1/n. This implies that inf (>I (η) ⇒ (A u B)I (η)) = 0 η∈∆I and since I is strongly witnessed, there must exist a γ ∈ ∆I with 0 = >I (γ) ⇒ (A u B)I (γ) = (A u B)I (γ). But from this it follows that ((A u B) → ⊥)I (γ) ⇒ 0 = 0, contradicting the axiom h(A u B) → ⊥ v ⊥ ≥ 1i of TPs . Thus, P has a solution. t u s Notice that, if P has no solution, then OP still has witnessed models, but s no strongly witnessed models. It is also relevant to point out that OP has a strongly witnessed model iff it has a finite model. In fact, the condition of strongly witnessed was only used for ensuring finiteness of the model, and hence, that a solution is indeed found. Corollary 7. For ∗-ALE ontologies, strongly witnessed consistency and consis- tency w.r.t. finite models are undecidable. 5 Conclusions We have shown that consistency of ∗-ALE ontologies w.r.t. a wide variety of models, ranging from finite models to weakly witnessed models, is undecidable if the product t-norm semantics are used. Whether consistency in general, that is, without restricting the class of interpretations used, is also undecidable is still an open problem. In [11] it was shown that, if only crisp axioms are used, then consistency is equivalent to quasi-witnessed consistency. However, it is unclear how to extend this result to the fuzzy axioms used in this paper. As future work we plan to study whether these undecidability results still hold if the disjunction and negation constructors are used in place of the implication considered in this paper. Additionally, we will study the decidability status of these logics if different t-norms are chosen for the semantics. References 1. F. Baader and R. Peñaloza. Are fuzzy description logics with general concept inclusion axioms decidable? In Proc. of Fuzz-IEEE 2011. IEEE, 2011. To appear. 2. F. Bobillo, F. Bou, and U. Straccia. On the failure of the finite model property in some fuzzy description logics. CoRR, abs/1003.1588, 2010. 3. F. Bobillo, F. Bou, and U. Straccia. On the failure of the finite model property in some fuzzy description logics. Fuzzy Sets and Systems, 172(23):1–12, 2011. 4. F. Bobillo and U. Straccia. A fuzzy description logic with product t-norm. In Proc. of FUZZ-IEEE 2007, pages 1–6. IEEE, 2007. 5. F. Bobillo and U. Straccia. On qualified cardinality restrictions in fuzzy description logics under Łukasiewicz semantics. In Proc. of IPMU-08, pages 1008–1015, 2008. 6. F. Bobillo and U. Straccia. Fuzzy description logics with general t-norms and datatypes. Fuzzy Sets and Systems, 160(23):3382–3402, 2009. 7. M. Cerami, F. Esteva, and F. Bou. Decidability of a description logic over infinite- valued product logic. In Proceedings of KR 2010. AAAI Press, 2010. 8. A. García-Cerdaña, E. Armengol, and F. Esteva. Fuzzy description logics and t-norm based fuzzy logics. Int. J. of Approx. Reasoning, 51:632 – 655, July 2010. 9. P. Hájek. Metamathematics of Fuzzy Logic (Trends in Logic). Springer, 2001. 10. P. Hájek. Making fuzzy description logic more general. Fuzzy Sets and Systems, 154(1):1–15, 2005. 11. M. C. Laskowski and S. Malekpour. Provability in predicate product logic. Arch. Math. Log., 46(5-6):365–378, 2007. 12. T. Lukasiewicz and U. Straccia. Managing uncertainty and vagueness in description logics for the semantic web. Journal of Web Semantics, 6(4):291–308, 2008. 13. E. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52:264–268, 1946. 14. G. Stoilos, G. B. Stamou, V. Tzouvaras, J. Z. Pan, and I. Horrocks. The fuzzy description logic f-SHIN. In Proc. of URSW’05, pages 67–76, 2005. 15. G. Stoilos, U. Straccia, G. B. Stamou and J. Z. Pan. General concept inclusions in fuzzy description logics. In Proc. of ECAI’06, pages 457–461, 2006. 16. U. Straccia. Reasoning within fuzzy description logics. JAIR, 14:137–166, 2001. 17. U. Straccia. Description logics with fuzzy concrete domains. In Proc. of UAI’05, pages 559–567. AUAI Press, 2005. 18. U. Straccia and F. Bobillo. Mixed integer programming, general concept inclusions and fuzzy description logics. In Proc. of 5th EUSFLAT Conf., pages 213–220, 2007. 19. C. Tresp and R. Molitor. A description logic for vague knowledge. In Proc. of ECAI’98, pages 361–365, Brighton, UK, 1998. J. Wiley and Sons.