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 reg 1 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 f KD -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 f KD -SI and f KD -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 f L -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 f P -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 f KD -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.

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 :

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]. In the following we will refer to a collection of fuzzy operators c, t, u, J as a fuzzy quadruple and c, t, u as a fuzzy triple.

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:

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 a I ∈ Δ I , 2. a concept name A ∈ C to a membership function

For example, if a ∈ Δ I then A I (a) gives the degree that the object a belongs to the fuzzy concept A, e.g. A I (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 Σ = T , R, A 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 C I (a) = n, and n

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,

Table 1. Semantics of f-SI-concepts and f-SI-roles

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)

e. an object that witnesses the degree of a in (∀R.C) I .

Moreover, we will use the notation f J -SI, where J is a fuzzy implication, to refer to a fuzzy DL that uses specific fuzzy operators. For example, f L -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.

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 f KD -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.

Stoilos et al. [12] presented a reasoning algorithm for f KD -DLs that allow for transitive roles by extending the classical results for handling transitivity [5].

More precisely, they show that in f KD -DLs if (∀R.C) I (a I ) ≥ n and R transitive, then (∀R.(∀R.C)) I (a I ) ≥ n. Using this property they proposed the ∀ + -rule for f KD -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: 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 f KD -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: 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.

In [12] the authors show how to extend the classical blocking condition to the family of f KD -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 f KD -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 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) ≥ n 1 and (a : D) ≥ n 2 , with the constraints t(n 1 , n 2 ) ≥ 0.8 and 0 ≤ n 1 , n 2 ≤ 1. Straccia and Bobillo presented reasoning algorithms for f L -ALC and f P -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 ≥ n , then in the constructed model one has to create a new edge R I (b I , a I ) = r new that points from b I to the node that blocks c I . 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 application of the algorithm might be such that no degree r new 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

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 n 1 ≥ n 3 . Nevertheless, it is currently not clear whether such new degrees can always be safely assumed. More precisely, it might the case that the relation n 3 < n 1 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.

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 f KD -SI, in the sense that we do not make 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:

Definition 1. If Σ is an f * -SI knowledge base, R A is the set of roles occurring in A and R together with their inverses and I A 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 : R A × S × S → [0, 1] maps each role of R A and pair of elements to the membership degree of the pair to the role, and V :

dually to the ≥ -rule, i.e. replace ≥ by ≤ and the t-norm (t) with a t-conorm u.

dually to the ≥ -rule, i.e. replace ≥ by ≤ and t with u.

and

dually to the ∃ ≥ -rule, i.e. replace ≥ by ≤ (except for R, ≥, n1 ) and t with J .

x is not indirectly blocked, and 2.

x has an R ≥n -neighbour y with C, ≥, n2 ∈ L(y) and {u (x,y):R ≤ n1,

, with Trans(R), x is not indirectly blocked, and 2. x has a R ≥n -neighbour y with, ∀R.C, ≥, n2 ∈ L(y), and

Table 2. Tableaux expansion rules for f * -SI

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:

where x = (x 1 , . . . , x n ), x i ∈ R is a vector of variables, f is called the objective function and g i are the constraint functions.

Depending on the form of f and g i , as well as the constraints imposed on x we obtain different types of optimization problems. If for all x i , a ≤ x i ≤ b holds, then the problem is called bounded ; if

the problem is called mixed integer. On the other hand depending on the form of f, g i we obtain a (i) linear programming problem, if f, g i are linear functions, (ii) quadratic, (iii) convex if some g i 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 g i are convex in order to guarantee that the method will reach a global minimum.

Straccia [14] showed that reasoning in f L -ALC and f KD -ALC can be formalized 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 f P -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: Let f Rei -SI be the fuzzy SI DL that uses the Lukasiewicz negation, the product t-norm the probabilistic sum and the Reichenbach S-implication.

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) = log s

) , s > 0, s = 1. As we can note the parameters appear as exponents inside a logarithm. Table 3. The fuzzy logic resulting by the Weber, Yu and Schweizer & Sklar operators.

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.

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 f L -SI, f P -SI, f WR -SI, f WS -SI, f YR -SI, f YS -SI, f Rei -SI, f SS 2 S -SI and f SS 2 R -SI.