GCIs Make Reasoning in Fuzzy DL with the Product T-norm Undecidable

Abstract

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 algorithms 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 presence 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 setting 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 ontology 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]

Introduction

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 j ? j > j C1 u C2 j C1 ! C2 j 9r:C j 8r: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 2 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 nonempty domain , a fuzzy set is a function F : ! [0; 1], with the intuition that an element 2 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 ; 2 [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 2 I , >I ( ) = 1; ?I ( ) = 0; (C1 u C2)I ( ) = C1I ( )

C2I ( ) (C1 ! C2)I ( ) = C1I ( ) ) C2I ( ) (9r:C)I ( ) = sup rI ( ; ) 2 I

The interpretation I = ( I ; I ) satisfies the assertional axiom ha : C B qi iff

CI (aI ) B q, it satisfies h(a; b) : r B qi iff rI (aI ; bI ) B q and it satisfies the concept

inclusion hC v D qi iff inf 2 I (CI ( ) ) 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 interpretation I is called witnessed if it satisfies the following two conditions: (wit1) for every 2 I , role r and concept C there exists

(9r:C)I ( ) = rI ( ; ) CI ( ), and (wit2) for every 2 I , role r and concept C there exists (8r:C)I ( ) = rI ( ; ) ) CI ( ). 2 2

I such that

I such that

This model is called weakly witnessed if it satisfies (wit1) and quasi-witnessed if it satisfies (wit1) and the condition

(wit2’) for every 2 I , role r and concept C, either (8r:C)I = 0 or there exists 2 I such that (8r:C)I ( ) = rI ( ; ) ) CI ( ).

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 (CI ( ) ) DI ( )) = CI ( ) ) DI ( ): 2 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 consistency, which itself implies weakly witnessed consistency. The converse implications, 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 ; 2 [0; 1] it holds that ) = 1 iff . Thus, given two concepts C; D, the axiom hC v D 1i expresses that CI ( ) DI ( ) for all 2 I . Additionally, 1 ) = and 0 ) = 1 for all 2 [0; 1], and ) 0 = 0 for all 2 (0; 1].

In the following, we will use the expression hC r Di to abbreviate the axioms hC v 8r:D 1i ; h9r:D v C 1i. To understand this abbreviation, consider an interpretation I satisfying hC r Di and let ; 2 I with rI ( ; ) = 1. From the first axiom it follows that and hence, both axioms together imply that CI ( ) = DI ( ). In other words, hC r Di expresses that the value of CI ( ) is propagated to the valuation of the concept D on all r successors with degree 1 of . Conversely, given an iinmtperliperseCtaIti(on) =I DsuIc(h )t,htahtenrII( i;s a) m2ofd0e;l 1ogf hfoCr arllDi;. 2 I , if rI ( ; ) = 1 For a concept C, and a natural number n 1, the expression Cn will denote n the concatenation of C with itself n times; that is, Cn := of u yields (Cn)I ( ) = (CI ( ))n, for every model I and 2 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 = f1; : : : ; sg; s > 1. The Post correspondence problem (PCP) u C. The semantics j=1 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 i1i2 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 = i1i2 ik 2 f1; : : : ; mg , 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

2 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 2 f1; : : : ; mg . 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 is an element 2 I with AI ( and BI ( ) = 22 fw1;.: :A: d;dmitgionthalelrye, OP such that for every witnessed mo)d=el 2I ovf OP and every 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 2 I such that AI ( ) = BI ( ).

Let 2 I encode the words v; w 2 ; i.e., AI ( ) = 2 v and BI ( ) = 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

TPi := fh> v 9ri:>

1i ; h(Vi u A(s+1)jvij ) ri Ai; h(Wi u B(s+1)jwij ) ri Big:

Recall that we are viewing words in as natural numbers in base s + 1. Thus,

the concatenation of two words u; u0 corresponds to the operation u (s+1)ju0j+u0.

We then have that

(Vi u A(s+1)jvij )I ( ) = ViI ( ) (AI ( ))(s+1)jvij = 2 vvi : If I is a witnessed model of TPi , then from the first axiom it follows that (9ri:>)I ( ) = 1, and according to (wit1), there must exist a 2 I with rI ( ; ) = 1. The last two axioms then ensure that AI ( ) = 2 vvi and BI ( ) = 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

TP0 := fhVj ri Vji; hWj ri Wji j 1 i; j It only remains to ensure that there is a node " where AI ( ") = BI ( ") = 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

0 := fha : A = 1i ; ha : B = 1ig [ AP f a : Vi = 2 vi ; a : Wi = 2 wi j 1 i mg:

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 := fha : H = 0:5ig; T0 := fhH ri Hi j 1 i mg:

This concept name will later be used to detect whether P has a solution (see

Theorem 3).

Let now OP := (AP ; TP ) where AP = AP [ A0 and TP := T0 [ Sim=0 TPi . We 0 define the interpretation IP := ( IP ; IP ) as follows: – IP = f1; : : : ; mg , – aIP = ", for every 2

IP , and for all j; 1 j

m – AIP ( ) = 2 v ; BIP ( ) = 2 w ; HIP ( ) = 0:5, – 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 2 IP , CIP ( ) = CI (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 2 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 q0i.

Let now be such that f ( ) has already been defined. By induction, we

can assume that AI (f ( )) = 2 v ; BI (f ( )) = 2 w ; HI (f ( )) = 0:5, and for every j, 1 j m, VjI (f ( )) = 2 vj ; WjI (f ( )) = 2 wj . Since I is a witnessed rmIo(dfe(l )o;f h)>=v1,9arni:d>as I1is,aftoisrfiaesll ail;l1the aixiommsotfhtehree feoxrmistshCa r D2i 2ITPw,itiht follows that

AI ( ) = 2 v vi = 2 v i ;

BI ( ) = 2 w wi = 2 w i ; HI ( ) = 0:5 and for all j; 1 j m, VjI ( ) = 2 vj ; WjI ( ) = 2 wj . Setting f ( i) = thus satisfies the required property. tu

From this lemma it follows that, if the PCP P has a solution for some 2 f1; : : : ; mg+, then every witnessed model I of OP contains a node = f ( ) such that AI ( ) = BI ( ); 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= BIP ( ) for every 2 f1; : : : ; mg+. This will ensure that the extended ontology will have a model iff P has no solution.

Suppose for now that, for some 2 f1; : : : ; mg , it holds that

2 v

= AIP ( ) > BIP ( ) = 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 ) and thus ((A ! B) u (B ! A))IP ( ) 0:5. Likewise, if AIP ( ) < BIP ( ), we also get ((A ! B) u (B ! A))IP ( ) 0:5. Additionally, if AIP ( ) = BIP ( ), then it is easy to verify that ((A ! B) u (B ! A))IP ( ) = 1. From all this it follows that, for every 2 f1; : : : ; mg ,

AIP ( ) 6= BIP ( ) iff ((A ! B) u (B ! A))IP ( ) 0:5: (1)

Thus, the instance P has no solution iff for every

((A ! B) u (B ! A))IP ( ) 0:5.

0 := (AP ; TP0 ) where We define now the ontology OP 2 f1; : : : ; mg+ it holds that TP0 := TP [ fh> v 8ri:(((A ! B) u (B ! A)) ! H)

Proof. Assume first that P has a solution = i1 ik and let u = v = w and 0 = i1i2 ik 1 2 f1; : : : ; mg . Suppose there is a witnessed model I of OP0 . Since OP OP0 , I must also be a model of OP . From Lemma 2 it then follows that there are nodes ; 0 2 I such that AI ( ) = AIP ( ) = BIP ( ) = BI ( ) 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 (8rik :(((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 OP0 .

For the converse, assume that OP

0 is not witnessed consistent. Then IP is not a model of OP0 . Since it is a model of OP , there must exist an i; 1 i m such that IP violates the axiom h> v 8ri:(((A ! B) u (B ! A)) ! H) 1i. This means that there is some 2 f1; : : : ; mg such that

(8ri:(((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) = BIP ( i) and hence i is a solution of P. tu 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 2 IP (>IP ( ) ) AIP ( )) = 0, but there is no 2 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

si := fhCi v 9ri:> T P

1i ; hVi u A(s+1)jvij ri Ai; hWi u B(s+1)jwij ri Big: The only difference between the TBoxes TPi and T siP is in the first axiom. Intuitively, 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 Cis 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 intuition, we define the ontology OP s

s := (AsP ; TP ) where AsP := A0P [ fa : max(C1; : : : ; Cm) = 1g;

m TPs := TP0 [ [ T siP [ fh(A u B) ! ? v ? 1ig [ i=1 fh> v 8ri: max((A ! B) u (B ! A); C1; : : : ; Cm)

Proof. Let = i1i2 ik be a solution of P and let pre( ) denote the set of all prefixes of . We build the finite interpretation IPs as follows: – IPs := pre( ), – aIPs = ", for all 2 s

IP , – AIPs ( ) = 2 v ; BIPs ( ) = 2 w , and for all j; 1 j

m s s – VjIP ( ) = 2 vj ; WjIP ( ) = 2 wj ,

s s – CjIP ( ) = 1 if j 2 pre( ) and CjIP ( ) = 0 otherwise, and

s s – rjIP ( ; j) = 1 if j 2 pre( ) and rjIP ( ; 0) = 0 if 0 2 pre( ) and 0 6= j. We show now that IPs is a model of OPs . Since IPs is finite, it follows immes satisfies all axioms in diately that it is also strongly witnessed. Clearly IP

s A0P ; additionally, we have that CiI1P (") = 1 and thus, IsPs satisfies AsP . The ahxeniocme (hA(AuuBB))IPs!( ?) v> ?0 fo1ri aelxlpres2sesprteh(at), (AwhuichB)cIlPea(rl)y )hold0s.=W0e, naonwd show that the rest of the axioms are also satisfied for every 2 pre( ). Let 2 pre( ) n f g. sThen we know that there exists i; 1 i m such that i ss s si . Moreover, CIP ( ) = 1 and riIP ( ; i) = 1; thus IPs satisfies the axioms in T P CjIP ( ) = 0 = rjIP ( ; 0) for all j 6= i and all 0 2 pre( ) which means that IPs trivIiafllyi =sati,sfithesenalalsaxiiosmassionluTtisojPn.((A ! B) u (B ! A)s)IPs ( i) = 1; otherwise, there is a j; 1 j m with ij 2 pre( ) and thus CjIP ( i) = 1. This means s that IPs satisfies the last axioms in TPs. Finally, if = , then riIP ( ; 0) = 0 and Ci( ) = 0, for all 0 2 pre( ); 1 i m, and thus the axioms are all trivially satisfied.

For the converse, let I be a strongly witnessed model of OPs . Then, there must be an element 0 2 I with aI = 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 siP1 , there must exist a 1 2 I with riI1 ( 0; 1) = 1, AI ( 1) = 2 vi1 , and BI ( 1) = 2 wi1 . If AI ( 1) = BI ( 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; : : : 2 I where AI ( k) = 2 vi1 vik , and BI ( k) = 2 wi1 wik .

If there is some k such that AI ( k) = BI ( 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

2infI(>I ( ) ) (A u B)I ( )) = 0 and since I is strongly witnessed, there must exist a 2

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. tu Notice that, if P has no solution, then OPs still has witnessed models, but s has a no strongly witnessed models. It is also relevant to point out that OP 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 consistency 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 infinitevalued 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.