A Framework for Reasoning with Expressive Continuous Fuzzy Description Logics

Abstract

In the current paper we study the reasoning problem for fuzzy SI (f-SI) under arbitrary continuous fuzzy operators. Our work can be seen as an extension of previous works that studied reasoning algorithms for f-SI, but focused on specific fuzzy operators, e.g. fKD-SI and of reasoning algorithms for less expressive fuzzy DLs, like fL-ALC and fP -ALC (fuzzy ALC under the Lukasiewicz and product fuzzy operators, respectively). We show how transitivity can be handled for all the range of continuous fuzzy DLs and discuss about blocking and correctness in this setting. Based on these analysis, we present a unifying framework for reasoning over the class of continuous fuzzy DLs. Finally use the results to prove decidability of several fuzzy SI DLs.

-

Introduction Although, DLs are considerably expressive they have limitations especially when it comes to modelling domains where imprecise or vague information is present, thus fuzzy extensions to DLs have been proposed [ 13, 12, 8, 2 ]. Fuzzy DLs are envisioned to be useful for several applications that face such knowledge and today there is a great deal of effort to apply them in several domains like multimedia analysis and interpretation [ 11 ], multimedia retrieval [ 7 ], and semantic interoperability (ontology alignment) [ 3 ]. For example, in multimedia analysis in order to use semantically rich technologies one has to map from the semanticless numerical values that are extracted by analysis algorithms (e.g. the color, the texture, the shape or other low-level related features) to more high level (fuzzy/vague) concepts like blue, red, smooth, rough, long, small, overlapping, etc. More precisely, we could say that region reg1 is blue to a degree 0.8 and smoothly textured to a degree 0.7 [ 11 ]. Then we can use DL axioms deducing high level assertions about the various image regions.

Up to now many reasoning algorithms for fuzzy DLs have been presented.

Straccia [13] presented a tableaux reasoning algorithm for fKD-ALC (fuzzy

ALC under the Zadeh fuzzy operators: x ∧ y à min(x, y), x ∨ y à max(x, y),

¬x à 1 − x and x → y à max(1 − x, y)). This was later extended to very expressive fuzzy DLs, like fKD-SI and fKD-SHIN by Stoilos et al. [ 12 ], by investigating and extending the classical rule for transitivity (∀+) in the fuzzy setting. Then Straccia presented reasoning algorithms for fuzzy DLs that use other fuzzy operators than the Zadeh ones. Firstly, a reasoning algorithm for fL

ALCf (fuzzy ALCf under the Lukasiewicz operators: x ∧ y à max(0, x + y − 1),

x ∨ y à min(1, x + y), ¬x à 1 − x and x → y à min(1, 1 − x + y)) [ 14 ], while finally Bobillo and Straccia extended the approach to fP -ALCf [ 2 ] (fuzzy

ALCf under the product logic operators: (x ∧ y) à x · y, x ∨ y à x + y − x · y,

¬x à 1 − x and x → y à 1 if x ≤ y, y/x otherwise). These algorithms are based on tableaux procedures, and its application creates a set of inequations that need to be solved, which is different than fKD-DLs which are purely tableaux-based.

Obviously, a general framework for reasoning with fuzzy DLs allowing for a more

general class of fuzzy operators is required. A first such attempt for ALC had already been made by Trest & Molitor [ 15 ], nevertheless they did not provide a clear idea on how or if the system of inequations created can actually be solved in practice. Recently, Bobillo and Straccia [ 1 ] have presented an algorithm for reasoning with f-ALC over arbitrary left-continuous fuzzy operators.

Although the literature on fuzzy-DLs is flourishing it is quite evident that

several open issues exist. More precisely, there is currently no known algorithm for (very) expressive fuzzy DLs, like fuzzy SI, that allow for transitive and inverse roles, and at the same time allow for fuzzy operators other than the

Zadeh operators, needless to say a unifying framework for reasoning over all

continuous fuzzy DLs. In order to extend the algorithms to such fuzzy DLs the semantics of the respective constructors, like transitivity and inverse roles need to be studied and understood [ 12 ]. Furthermore, as we will see in Section 4.2, our investigation has shown that there are some very difficult issues related to termination (blocking condition) and correctness of the respective algorithms.

In this paper we try to tackle with these issue providing a unifying framework

for reasoning in fuzzy SI extended with arbitrary continuous fuzzy operators. 2

Fuzzy Set Theory While in classical set theory an element either belongs to a set or not, in fuzzy set theory elements belong only to a certain degree. More formally, let X be a set of elements. A fuzzy subset A of X, is defined by a membership function µA(x), or simply A(x) [ 6 ]. This function assigns any x ∈ X to a value between 0 and 1 that represents the degree in which this element belongs to X. In this new framework the classical set theoretic and logical operations are performed by special mathematical functions. More precisely fuzzy complement is a unary operation of the form c : [ 0, 1 ] → [ 0, 1 ], fuzzy intersection and union are performed by two binary functions of the form t : [ 0, 1 ] × [ 0, 1 ] → [ 0, 1 ] and u : [ 0, 1 ] × [ 0, 1 ] → [ 0, 1 ], called t-norm and t-conorm operations [ 6 ], respectively, and fuzzy implication also by a binary function, J : [ 0, 1 ] × [ 0, 1 ] → [ 0, 1 ]. In order to produce meaningfull fuzzy complements, conjunctions, disjunctions and implications, these functions must satisfy certain mathematical properties. For example the operators must satisfy the following boundary properties, c(0) = 1, c(1) = 0, t(1, a) = a and u(0, a) = a. Due to space limitations we cannot present all the properties that these functions should satisfy, but rather the reader is referred to [ 6 ]. Some, examples of fuzzy operators are the Lukasiewicz negation, cL(a) = 1 − a, tnorm, tL(a, b) = max(0, a + b − 1), t-conorm, uL(a, b) = min(1, a + b), and implication, JL(a, b) = min(1, 1 − a + b), the G¨odel norms tG(a, b) = min(a, b), uG(a, b) = max(a, b), and implication JG(a, b) = b if a > b, 1 otherwise, the products norms, tP (a, b) = a · b, uP (a, b) = a + b − a · b the Goguen implication JP (a, b) = ab if a > b, 1 otherwise, and the Kleene-Dienes implication (KD-implication), JKD(a, b) = max(1 − a, b).

In the following we will refer to a collection of fuzzy operators hc, t, u, J i as

a fuzzy quadruple and hc, t, ui as a fuzzy triple. 3

A Fuzzy Extension of the S I DL

In this section, we briefly introduce a fuzzy extension of the SI DL, which we call f-SI.

As usual we have an alphabet of distinct concept names (C), role names (R)

and individual names (I). Following [ 13, 12 ], we only extend classical assertions by allowing for degrees of truth, thus creating fuzzy assertions, while no other syntactic extensions are performed. This has the effect that f-SI-roles and f-SIconcepts are defined by the usual abstract syntax: C, D −→ ⊥ | ⊤ | A | C ⊓ D | C ⊔ D | ∃R.C | ∀R.C, R −→ S | S¡.

The semantics are provided by the means of fuzzy interpretations [13]. A

fuzzy interpretation as a pair I = (ΔI , ·I ), which maps

1. an individual a ∈ I to an element aI ∈ ΔI ,

2. a concept name A ∈ C to a membership function AI : ΔI → [0, 1],

3. a role name R ∈ R to a membership function RI : ΔI × ΔI → [0, 1].

For example, if a ∈ ΔI then AI (a) gives the degree that the object a belongs to the fuzzy concept A, e.g. AI (a) = 0.8. The notions of a TBox, RBox and knowledge base are defined in the usual way. On the other hand An f-SI ABox is a finite set of fuzzy assertions [ 13 ] of the form (a : C)⊲⊳n or ((a, b) : R)⊲⊳n, where ⊲⊳ ∈ {≥, ≤} and n ∈ [ 0, 1 ]. In the following ⊲⊳¡ denotes the reflection of inequalities; e.g., the reflection of ≥ is ≤ and that of ≤ is ≥. Table 1 summarizes the semantics of f-SI-concepts, f-SI-roles and satisfiability of TBox, RBox and

ABox axioms.

An f-SI knowledge base Σ = hT , R, Ai is satisfiable (unsatisfiable) iff there exists (does not exist) a fuzzy interpretation I which satisfies all axioms in Σ. An f-SI-concept C is n-satisfiable w.r.t. Σ iff there exists a model I of Σ in which there exists some a ∈ ΔI such that CI (a) = n, and n ∈ (0, 1]. A fuzzy concept C is subsumed by D w.r.t. Σ iff in every model I of Σ we have ∀d ∈ ΔI , CI (d) ≤ DI (d). An f-SI ABox A is consistent (inconsistent ) w.r.t. a

TBox T and an RBox R if there exists (does not exist) a model I of T and R

which satisfies every assertion in A. Given a concept or role axiom or a fuzzy assertion, Ψ , we say that Σ entails Ψ , writing Σ |= Ψ iff every model I of Σ satisfies Ψ . The greatest lower bound of an assertion Φ w.r.t. Σ is defined as, glb(Σ, Φ) = sup{n | Σ |= Φ ≥ n}, where sup ∅ = 0.

Constructor top bottom general negation conjunction disjunction exists restriction value restriction inverse role concept subsumption concept equivalence transitive roles concept assertion role assertion

Syntax ⊤ ⊥ ¬C C ⊓ D C ⊔ D ∃R.C ∀R.C

R− C ⊑ D C ≡ D Trans(R)

Semantics ⊤I (a) = 1 ⊥I (a) = 0 (¬C)I (a) = c(CI (a)) (C ⊓ D)I (a) = t(CI (a), DI (a)) (C ⊔ D)I (a) = u(CI (a), DI (a)) (∃R.C)I (a) = supb∈ΔI {t(RI (a, b), CI (b))} (∀R.C)I (a) = infb∈ΔI {J (RI (a, b), CI (b))} (R−)I (b, a) = RI (a, b) CI (a) ≤ DI (a) CI (a) = DI (a) ∀a, c ∈ ΔI RI (a, c) ≥ sup {t(RI (a, b), RI (b, c))}

b∈ΔI (a : C)⊲⊳n CI (aI )⊲⊳n, ⊲⊳ ∈ {≥, >, ≤, <} ((a, b) : R)⊲⊳n RI (aI , bI )⊲⊳n

In the following we restrict our attention only to witnessed (un)satisfiability.

As it is known in the fuzzy DL literature [4, 1] when allowing for general fuzzy

operators, the resulting f-DL might lack the finite model property. A model is called witnessed if for (∀R.C)I (a) = n there is some b ∈ ΔI such that J (RI (a, b), CI (b)) = n, i.e. an object that witnesses the degree of a in (∀R.C)I .

Moreover, we will use the notation fJ -SI, where J is a fuzzy implication, to refer to a fuzzy DL that uses specific fuzzy operators. For example, fL-SI denotes the fuzzy SI DL that uses the set of Lukasiewicz operators. On the other hand with f¤-SI we refer to all the family of continuous fuzzy-SI.

4

Reasoning with Expressive Fuzzy DLs In the current section we will investigate two of what we believe are the most difficult problems in the development of a correct (sound and complete) reasoning algorithm for expressive fuzzy DLs, that also allow for arbitrary continuous fuzzy operators. Firstly, we investigate how to handle transitivity, i.e. how to extend the ∀+-rule [ 5 ] in f¤-SI. Thus, our investigation has extends the one in [ 12 ] for fKD-SI. Secondly, we also investigate on blocking conditions [ 5 ] and their applicability in the fuzzy setting. The latter one is a very difficult issue and it was the main reason that reasoning algorithms for expressive DLs using arbitrary continuous norms have not been presented until now. 4.1

Transitivity and role hierarchies in Fuzzy Description Logics Stoilos et al. [ 12 ] presented a reasoning algorithm for fKD-DLs that allow for transitive roles by extending the classical results for handling transitivity [ 5 ].

More precisely, they show that in fKD-DLs if (∀R.C)I (aI ) ≥ n and R transitive,

then (∀R.(∀R.C))I (aI ) ≥ n. Using this property they proposed the ∀+-rule for fKD-SI. In order to provide a similar rule for f¤-SI this result needs to be extended. By using properties of fuzzy operators the following can be shown: Lemma 1. If (∀R.C)I (a) ≥ n, Trans(R) then, (∀R.(∀R.C))I (a) ≥ n if the fuzzy implications is either – an R-implication, or – an S-implications and the fuzzy triple hc, t, ui satisfies the De Morgan laws. From this Lemma we can note that in the case of S-implications, the fuzzy triple must additionally satisfy the De Morgan laws in order for the respective ∀+-rule to work properly.

Furthermore, Stoilos et al. [12] show that in the case of fuzzy DLs, apart

from value restrictions a similar property holds for existential restrictions as well. More precisely they show that in fKD-DLs if (∃R.C)I (a) ≤ n and R is transitive, then (∃R.(∃R.C))I (a) ≤ n. It is straightforward to expect that a similar property would generally hold for f¤-SI. Again, by using properties of fuzzy operators we obtain the following: Lemma 2. If (∃R.C)I (a) ≤ n and Trans(R) then, (∃R.(∃R.C))I (a) ≤ n holds. As can be seen in this case no distinction between R- and S-implications has to be made since the type of fuzzy implication now is irrelevant. 4.2

Blocking in Fuzzy Description Logics In [ 12 ] the authors show how to extend the classical blocking condition to the family of fKD-DLs with transitive roles. More precisely, the expansion is terminated when two individuals on some path of roles are asserted to belong to the same set of fuzzy assertions. They also show that this blocking condition is sufficient when reasoning with fKD-DLs since we can restrict our attention only to a finite set of degrees. For example, from (a : C ⊓ D) ≥ 0.8 one can safely infer (a : C) ≥ 0.8 and (a : D) ≥ 0.8, since ⊓ is interpreted as min and min(0.8, 0.8) ≥ 0.8. Finally, they show that the cycle creation technique [ 5 ] can also be used: More precisely, to create a correct model from (a : C) ≥ 0.8, (a : ∃R.C) ≥ 0.8, ((a, b) : R) ≥ 0.8, (b : C) ≥ 0.8, (b : ∃R.C) ≥ 0.8, one can discard b (since it is blocked by a) and create the cycle RI (aI , aI ) ≥ 0.8.

On the other hand, when reasoning with f¤-DLs one has to consider all possible membership degrees. More precisely, from (a : C ⊓ D) ≥ 0.8 we cannot infer (a : C) ≥ 0.8 and (a : D) ≥ 0.8, since for example under the product t-norm, 0.8 · 0.8 < 0.8. To the contrary we have to infer (a : C) ≥ n1 and (a : D) ≥ n2, with the constraints t(n1, n2) ≥ 0.8 and 0 ≤ n1, n2 ≤ 1. Straccia and Bobillo presented reasoning algorithms for fL-ALC and fP -ALCf that allow for GCIs [ 14, 2 ] revising the blocking condition from [ 12 ]. Roughly speaking, an individuals c is blocked by a if they share fuzzy assertions with the same concepts and the degrees are either both the same rational from [ 0, 1 ] or (variable) degree n from [ 0, 1 ]. Similarly as before, if for some individual b, (b, c) : R ≥ n0, then in the constructed model one has to create a new edge RI (bI , aI ) = rnew that points from bI to the node that blocks cI . At the current point we argue that this condition alone might not be sufficient to show the correctness of the procedure.

More precisely, the constrains on the degrees that have been created by the ap

plication of the algorithm might be such that no degree rnew could be selected in order for all the constraints to be satisfied.

Suppose for example that in an application of the tableaux algorithm for

a specific KB the following assertions have been created for some individual b: (b : C) ≥ n1, (b : ∃R.C) ≥ n2 and (b : ∀R.(∃R.C)) ≥ n3. Moreover, suppose that there is also another node c with similar assertions, thus blocked by b, and that the algorithm has computed the following values: n1 = 0.6, n2 = 0.4, n3 = 0.3. To create a model we discard c and create the cycle RI (bI , bI ) = rnew. It is not difficult to see that, in the constructed model, if we use the values that have been computed by the algorithm for degrees of CI (bI ), (∃R.C)I (bI ) and (∀R.(∃R.C))I (bI ), then no degree rnew can be found that satisfies all constraints. More precisely, for (∀R.(∃R.C))I (bI ) = 0.3 (and considering R-implications)1 it should hold that: 0.3 = J (rnew, (∃R.C)I (bI )) = sup{x | t(rnew, x) ≤ t(rnew, CI (bI ))} = sup{x | x ≤ CI (bI )} = CI (bI ) = 0.6, which is absurd. Consequently, when we construct a model out of a set of blocked fuzzy assertions in f¤-SI it might be the case that different degrees than the ones computed by the algorithm have to be used. In the previous case the degrees have to be such that n1 ≥ n3. Nevertheless, it is currently not clear whether such new degrees can always be safely assumed. More precisely, it might the case that the relation n3 < n1 is imposed by other assertions (constraints) in the ABox and thus we cannot select other values in the construction of the model.

Intuitively, the only assertions that can affect the membership degrees of individuals to concepts are those that exist originally in the ABox and that contain specific values from [ 0, 1 ]. Taking this into consideration we propose a more safe approach to blocking in f-SI. Intuitively, our blocking condition is such that the at the point that blocking is allowed the set of inequalities is sufficiently unconstrained in order to ensure that the correct membership degrees in the constructed model can indeed be found. The formal condition that gives this property is the depth of the node in the tree w.r.t. the nested quantifiers that exist in our original KB. More precisely, if k is the largest number of consecutive nested quantifiers in our KB, then the depth of the node should be at least k + 1. 5

A Framework for Reasoning with Fuzzy SI

In the current section we will provide a general framework for reasoning in

f¤-SI. The fuzzy tableau we present here can be seen as an extension of the fuzzy tableau presented in [ 12 ] for fKD-SI, in the sense that we do not make 1 Can also be shown for many S-implications.

(a:D)∪¸n2A

Cv∪D2T specific assumptions about the fuzzy operators used but we use arbitrary ones.

One consequence is that we cannot make usual assumption, like for example that

concepts exist in their negation normal form (NNF). For a fuzzy concept D we use sub(D) to denote the set of subconcepts of D. Finally, for a KB Σ we define: sub(Σ) = sub(D) sub(C) ∪ sub(D).

Definition 1. If Σ is an f¤-SI knowledge base, RA is the set of roles occurring in A and R together with their inverses and IA is the set of individuals in A, a fuzzy tableau T for Σ, is defined to be a quadruple (S, L, E , V) such that: S is a set of elements, L : S × sub(Σ) → [ 0, 1 ] maps each element and concept, that is a member of sub(Σ), to the membership degree of that element to the concept, E : RA × S × S → [ 0, 1 ] maps each role of RA and pair of elements to the membership degree of the pair to the role, and V : IA → S maps individuals occurring in A to elements in S. For all s, t ∈ S, C, D ∈ sub(Σ), n, n1, n2 ∈ (0, 1] and R ∈ RA, T satisfies: 1. L(s, ⊥) = 0 and L(s, ⊤) = 1 for all s ∈ S, 2. if L(s, ¬C)⊲⊳n, then L(s, C)⊲⊳¡n0, where n0⊲⊳¡c(n), 3. if L(s, C ⊓ E) ≥ n then L(s, C) ≥ n1, L(s, E) ≥ n2 with t(n1, n2) ≥ n, 4. if L(s, C ⊔ E) ≤ n then L(s, C) ≤ n1, L(s, E) ≤ n2 with u(n1, n2) ≤ n, 5. if L(s, C ⊔ E) ≥ n then L(s, C) ≥ n1, L(s, E) ≥ n2 with u(n1, n2) ≥ n, 6. if L(s, C ⊓ E) ≤ n then L(s, C) ≤ n1, L(s, E) ≤ n2 with t(n1, n2) ≤ n, 7. if L(s, ∀R.C) ≥ n, then E (R, hs, ti) ≤ n1, L(t, C) ≥ n2 with J (n1, n2) ≥ n, 8. if L(s, ∃R.C) ≤ n, then either E (R, hs, ti) = n1 ≤ n or L(t, C) ≤ n2 with t(n1, n2) ≤ n, 9. if L(s, ∃R.C) ≥ n, then there exists t ∈ S such that E (R, hs, ti) ≥ n1,

L(t, C) ≥ n2 with t(n1, n2) ≥ n, 10. if L(s, ∀R.C) ≤ n, then there exists t ∈ S such that E (R, hs, ti) ≤ n1,

L(t, C) ≤ n2 with t(n1, n2) ≤ n, 11. if L(s, ∀R.C) ≥ n and Trans(R), then E (R, hs, ti) ≤ n1 and L(t, ∀R.C) ≥ n2 with J (n1, n2) ≥ n, 12. if L(s, ∃R.C) ≤ n and Trans(R), then E (R, hs, ti) = n1 ≤ n or L(t, ∀R.C) ≤ n2 with t(n1, n2) ≤ n, 13. E (R, hs, ti) ≥ n iff E (Inv(R), ht, si) ≥ n, 14. if (a : C)⊲⊳n ∈ A, then hL(V(a), C)⊲⊳n, 15. if ((a, b) : R)⊲⊳n ∈ A, then E (R, hV(a), V(b)i)⊲⊳n, 16. if C ⊑ D ∈ T , then for all s ∈ S, L(s, C) ≤ L(s, D).

Lemma 3. An f¤-SI KB Σ is satisfiable by a witnessed model, iff there exists a fuzzy tableau for Σ.

An Algorithm for Constructing an f∗-SI Tableau

As it is obvious in order to decide f¤-SI knowledge base satisfiability a procedure

that constructs a tableau for a Σ has to be determined.

Definition 2 (Completion-Forest). A completion-forest F for an f¤-SI KB Σ = hT , A, Ri is a collection of trees whose distinguished roots are arbitrarily connected by edges and which also allows for a set of inequality constraints X . Each node x is labelled with a set L(x) = {hC, ⊲⊳, ni}, where C ∈ sub(Σ), ⊲⊳ ∈ {≥ , ≤} and n is either a degree from [ 0, 1 ] or a variable degree, i.e. a variable taking values in [ 0, 1 ]. Each edge hx, yi is labelled with a set L(hx, yi) = {hR, ⊲⊳, ni}, where R ∈ RA are (possibly inverse) roles occurring in A.

If nodes x and y are connected by an edge hx, yi with hR, ⊲⊳, ni ∈ L(hx, yi), then y is called an R⊲⊳n-successor of x and x is called an R⊲⊳n-predecessor of y. If y is an R⊲⊳n-successor or an Inv(R)⊲⊳n-predecessor of x, then y is called an R⊲⊳n-neighbour of x. As usual, ancestor is the transitive closure of predecessor.

A node x is blocked iff it is not a root node and it is either directly or indirectly blocked. A node x is directly blocked iff none of its ancestors are blocked, it has an ancestor y such that L(x) and L(y) are equivalent, written L(x) ≈ L(y), i.e. hCi, ⊲⊳, nii ∈ L(x) iff hCi, ⊲⊳, n0ii ∈ L(y), for all 1 ≤ i ≤ k and both ni and n0i are variable degrees or the same rational from (0, 1] and the level of y is greater than the largest number of consecutive nested quantifiers found in concepts of Σ. Finally, a node x is indirectly blocked iff one of its predecessor is blocked.

A completion-forest F is said to contain a clash iff the system X of inequations has no solution, or for some node x, L(x) contains one of the following triples h⊥, ≥, ni, h⊤, ≤, ni, with n > 0 or n < 1, respectively.

For an f¤-SI KB Σ = hT , A, Ri, the algorithm initialises a forest F to contain (i) a root node xai , for each individual ai ∈ IA occurring in A, labelled with L(x) such that hCi, ⊲⊳, ni ∈ L(xai ) for each assertion of the form (ai : Ci)⊲⊳n ∈ A, (ii) an edge hxai , xaj i, for each assertion ((ai, aj ) : Ri)⊲⊳n ∈ A, labelled with L(hxai , xaj i) such that hRi, ⊲⊳, ni ∈ L h ( xai , xaj i), and (iii) a system of inequations X to contain u(xai ,xaj ):R⊲⊳n for each ((ai, aj ) : Ri)⊲⊳n ∈ A. Furthermore, the algorithm expands R by adding an axiom Trans(Inv(R)) for each Trans(R) ∈ R. F is then expanded by repeatedly applying the completion rules from Table 2 stopping when none of them is applicable (saying that F is complete) and adding necessary constraints 0 ≤ n ≤ 1 for each new degree n that is created during expansion, as well as constraints 0 < ɛ ≤ 1 for any degree ɛ added due to normalization. The application of expansion rules adds inequalities in X which after F is complete should be solved by a suitable solution method, computing a value for each variable degree ua:A, u(a,b):R and n that appears in X , respectively. The algorithm answers ‘Σ is satisfiable’ iff the completion rules can be applied in such a way that they yield a complete and clash-free completionforest (a completion-forest that is both complete and no clash condition appears), and ‘Σ is unsatisfiable’ otherwise.

Lemma 4. Let Σ be an f¤-SI KB. Then, (i) when started for Σ the tableaux algorithm consisting of the expansion rules of Table 2 terminates; (ii) Σ has a fuzzy tableau if and only if the expansion rules of Table 2 can be applied to Σ such that they yield a complete and clash-free augmented completion forest.

Rule eq : u¸ t· t¸

As is if obvious from the above, the application of expansion rules creates a system of inequations. Straccia [14] proposed the use of optimisation techniques for solving such a system:

Definition 3. An optimization problem can be formalized as follows: minimize f (x) subject to gi(x) ≤ bi, 1 ≤ i ≤ m where x = (x1, . . . , xn), xi ∈ R is a vector of variables, f is called the objective function and gi are the constraint functions.

Depending on the form of f and gi, as well as the constraints imposed on x we obtain different types of optimization problems. If for all xi, a ≤ xi ≤ b holds, then the problem is called bounded ; if xi ∈ Z it is called integer ; If xi ∈ Z, xj ∈ R, with 1 ≤ i 6= j ≤ m, the problem is called mixed integer. On the other hand depending on the form of f, gi we obtain a (i) linear programming problem, if f, gi are linear functions, (ii) quadratic, (iii) convex if some gi is an arbitrary nonquadratic function but still convex, or (iv) non-convex. These characterizations are essential in order to determine the difficulty of the problem. For example, the

Simplex algorithm [9] is a very successful method for solving mixed integer linear

systems. On the other hand for arbitrary functions the problem becomes highly complex and usually one requires that all gi are convex in order to guarantee that the method will reach a global minimum.

Straccia [14] showed that reasoning in fL-ALC and fKD-ALC can be for

malized as a bounded Mixed Integer Linear Programming (bMILP) problem [ 10 ]. This is because, for example, under the Lukasiewicz t-norm from t(x, y) = max(0, x+y−1) ≥ n we (roughly) obtain a linear constraint x+y−1 ≥ n together with some integer contrains which analyze the “ max ” function. Subsequently,

Straccia and Bobillo [2] showed that reasoning in fP -ALC could be formalized as

a bounded Mixed Integer Quadratic Programming (bMIQP) problem [ 10 ]. These methods can still be used in our framework as long as the norm operators used can be analyzed to form a bMILP or a bMIQP problem. Moreover, all inference problems can be reduced to KB (un)satisfiability as follows: C is n-satisfiable w.r.t. Σ iff

C ⊑ D w.r.t. Σ iff Σ |= a : C ≥ n iff min x = 0 under hT , R, A ∪ {(a : C) ≥ n}i min x = 0 under hT , R, A ∪ {(a : C) ≥ x1, (a : D) ≤ x2}i and X = {x ≥ x1 − x2}. min x under hT , R, A ∪ {a : C ≤ n − ɛ}i, where ɛ is an arbitrary small degree, be solved glb(Σ, a : C) = n iff

min x = n under hT , R, A ∪ {a : C ≤ x}i

Consequently, we have the following:

Theorem 1 (Decidability of fL-SI and fP -SI). The tableaux algorithm together with a bMILP (resp. bMIQP) solver consist of a decision procedure for the inference problems of fL-SI (resp. fP -SI).

Let fRei-SI be the fuzzy SI DL that uses the Lukasiewicz negation, the

product t-norm the probabilistic sum and the Reichenbach S-implication. Theorem 2 (Decidability of fRei-SI). The tableaux algorithm together with a bMIQP solver consist of a decision procedure for the inference problems of fRei-SI.

Nevertheless, in the current paper we have given an overall framework for

reasoning in expressive fuzzy DLs extended with arbitrary continuous t-norms.

Unfortunately, most norm functions have a very complex form which cannot be

analyzed into linear or quadratic functions. Consider for example the family of Frank t-norms: t(x, y) = logs (1 + (sx¡1)(sy¡1) ) , s > 0, s 6= 1. As we can note s¡1 the parameters appear as exponents inside a logarithm.

Operator complement t-norm t-conorm S-impl.

R-impl.

Nevertheless, there are still some norms or restrictions of them whose function can be analyzed into mixed integer linear constraints. Table 3 summarizes a few that we were able to identify. Note that different fuzzy implications define a different fuzzy DL. Consequently, we have the following results.

fYS -SI, fSSS2 -SI and fSSR2 -SI.

Theorem 3 (Decidability of fWS -SI, fWR -SI, fYS -SI, fYR -SI, fSSS2 -SI and fSSR2 -SI). The tableaux algorithm together with a bMIQP solver consist of a decision procedure for the inference problems of fWR -SI, fWS -SI, fYR -SI, 6

Conclusions In the current paper we attempt to tackle with the problem of reasoning with expressive fuzzy DLs that used arbitrary fuzzy operators. To accomplish our goals firstly, we have investigated the properties of the semantics of transitive roles when these are used in value and existential restrictions. This greatly extends the results that have been presented in [ 12 ] for transitivity in fuzzy DLs which use the min − max operators. Secondly, we have dealt with the non-termination problem. We have seen that finding a correct and sufficient blocking condition for such fuzzy DLs is considerably difficult, which justifies the fact that reasoning with expressive fuzzy DLs was an open problem for many years. We have analyzed these difficulties and have proposed a safe blocking condition. Nevertheless, it is still an open question whether a more relaxed condition can indeed be employed. Subsequently, using our investigations we developed a tableaux reasoning algorithm for deciding the satisfiability problem for an f¤-SI KB. Subsequently, we prove the soundness, completeness and termination of the algorithm. Finally, we show how one can use this algorithm to provide practical reasoning by using bMILP and bMIQP solvers as suggested in [ 14, 2 ]. Overall, we have proved decidability of the fuzzy DLs fL-SI, fP -SI, fWR -SI, fWS -SI, fYR -SI, fYS -SI, fRei-SI, fSSS2 -SI and fSSR2 -SI.

References

1. Fernando Bobillo and Umberto Straccia . Fuzzy description logics with general t-norms and datatypes . Fuzzy Sets and Systems , In Press.

2. Fernando Bobillo and Umberto Straccia . A fuzzy description logic with product t-norm . In Proceedings of the IEEE International Conference on Fuzzy Systems (Fuzz-IEEE-07) , London, 2007 .

3. Alfio Ferrara , Davide Lorusso, Giorgos Stamou, Giorgos Stoilos, Vassilis Tzouvaras, and Tassos Venetis . Resolution of conflicts among ontology mappings: a fuzzy approach . In Proceedings of the 3rd International Workshop on Ontology Matching (OM 2008 ), Karlsruhe, Germany, 2008 .

4. P. Hajek . Making fuzzy description logic more general . Fuzzy Sets and Systems , 154 ( 1 ): 1 - 15 , 2005 .

5. I. Horrocks and U. Sattler . A description logic with transitive and inverse roles and role hierarchies . Journal of Logic and Computation , 9 : 385 - 410 , 1999 .

6. G. J. Klir and B. Yuan . Fuzzy Sets and Fuzzy Logic: Theory and Applications . Prentice-Hall, 1995 .

7. Carlo Meghini , Fabrizio Sebastiani, and Umberto Straccia . A model of multimedia information retrieval . Journal of the ACM , 48 ( 5 ): 909 - 970 , 2001 .

8. J.Z. Pan , G. Stamou, G. Stoilos, and E. Thomas. Scalable querying services over fuzzy ontologies . In Proceedings of the International World Wide Web Conference (WWW 2008 ), Beijing, 2008 .

9. C.H. Papadimitriou and K. Steiglitz . Combinatorial Optimization: Algorithms and Complexity . Prentice-Hall, Englewood Cliffs, New Jersey, 1982 .

10. H. Salkin and M. Kamlesh . Foundations of Integer Programming . North-Holland, 1988 .

11. N. Simou , Th. Athanasiadis, G. Stoilos, and S. Kollias . Image indexing and retrieval using expressive fuzzy description logics . Signal, Image and Video Processing , Springer, 2 ( 4 ): 321 - 335 , 2008 .

12. Giorgos Stoilos , Giorgos Stamou, Vassilis Tzouvaras, Jeff Z. Pan , and Ian Horrocks . Reasoning with very expressive fuzzy description logics . Journal of Artificial Intelligence Research , 30 ( 5 ): 273 - 320 , 2007 .

13. U. Straccia . Reasoning within fuzzy description logics . Journal of Artificial Intelligence Research , 14 : 137 - 166 , 2001 .

14. U. Straccia and F. Bobillo . Mixed integer programming, general concept inclusions and fuzzy description logics . In Proceedings of the 5th Conference of the European Society for Fuzzy Logic and Technology (EUSFLAT-07) , pages 213 - 220 , 2007 .

15. C. Tresp and R. Molitor . A description logic for vague knowledge . In In proc of the 13th European Conf. on Artificial Intelligence (ECAI-98) , pages 361 - 365 , 1998 .