By the development of Semantic Web, increasing demands for vague information representation have triggered a mass of theoretical and applied researches of fuzzy ontologies, whose main logical infrastructures are fuzzy description logics. However, current tableau algorithms can not supply complete reasoning support within fuzzy ontology: reasoning with general TBox is still a difficult problem in fuzzy description logics. The main trouble is that fuzzy description logics adopt fuzzy models with continuous but not discrete membership degrees. In this paper, we propose a novel semantical discretization to discretize membership degrees in fuzzy description logic F SHIN . Based on this discretization, we design discrete tableau algorithms to achieve reasoning with general TBox. The Semantic Web stands for the idea of a future Web, in which information is given well-defined meaning, better enabling intelligent Web information processing [1]. In the Semantic Web, ontology is a crucial knowledge representation model to express a shared understanding of information between users and machines. Along with the evolvement from current Web to the Semantic Web, the management of ill-structured, ill-defined or imprecise information plays a more and more important role in applications of the Semantic Web [13]. This trend calls for ontologies with capability to deal with uncertainty. However, classical DLs, as the logical foundation of ontologies, are two-value-based languages. The need for expressing uncertainty in the Semantic Web has triggered extending classical DLs with fuzzy capabilities, yielding Fuzzy DLs (FDLs for short). Straccia proposed a representative fuzzy extension F ALC of DL ALC, in which fuzzy semantics is introduced to interpret concepts and roles as fuzzy sets [11]. Following researchers extended F ALC with more complex constructions: F ALCQ [6] with qualified number restriction , F SI [7] with transitive and inverse role, and F SHIN [8], a extension of F SI with role hierarchy and unqualified number restriction. Stoilos et al introduced Straccia's fuzzy framework into OWL, hence getting a fuzzy ontology language F SHOIN , by which fuzzy ontologies are coded as FDL knowledge bases [9]. Though the fuzzy DLs have done a lot, to our best knowledge, reasoning with general TBox in FDLs is still a difficult problem [8]. Current tableau algorithms in FDLs are applied to achieve reasoning without TBox or with acyclic TBox [7, 8, 11], that limits reasoning support within fuzzy ontologies. The main trouble in reasoning with general TBox is that fuzzy interpretations I map concepts C into membership degree functions CI () w.r.t domain ¢I : ¢I ! [0; 1], where the value domain [0,1] is continuous. In [4], we represented a novel semantical discretization technique to enable translation of membership degree values from continuous ones into discrete ones. In this paper, we will extend this discretization technique into F SHIN ; and based on it, we will design a discrete tableau algorithm for reasoning with general TBox in F SHIN . Since nominals should not be fuzzyfied, our discrete tableau algorithms for SHIN , together with reasoning technique to deal with nominals in crisp DLs [3], can be extended to provide a tableau algorithm for general TBox in F SHOIN , that will achieve complete reasoning within fuzzy ontologies.
2
Logical Infrastructure of Fuzzy Ontologies Let NC be a set of concept names (A), NR a set of role names (R) with a subset NR+ of transitive role names and NI a set of individual names (a). F SHIN roles are either role names R 2 NR or their inverse roles R¡. To avoid R¡¡, we use Inv(R) to denote the inverse role of R. F SHIN concepts C, D are inductively defined with the application of F SHIN concept constructors in the following syntax rules:
C; D :: >j?jAj:CjC u DjC t Dj9R:Cj8R:Cj ¸ pRj · pR
Since concepts and roles in F SHIN are considered as fuzzy sets, the semantics of concepts and roles are defined in terms of fuzzy interpretations I = h¢I ; ¢I i, where ¢I is a nonempty domain, and ¢I is an interpretation function mapping individuals a into aI 2 ¢I ; concept (role) names A (R) into membership functions AI (RI ) : ¢I (¢I £ ¢I ) ! [0; 1]. And for any transitive role name R 2 NR+, I satisfies 8d; d0 2 ¢I , RI (d; d0) ¸ supx2¢I fmin(RI (d; x); RI (x; d0))g. Furthermore, ¢I satisfies the following conditions for complex concepts and roles built by concept and role constructors: for any d; d0 2 ¢I >I (d) ?I (d) (:C)I (d) (C u D)I (d) (C t D)I (d) (9R:C)I (d) (8R:C)I (d) (¸ pR)I (d) (· pR)I (d) (R¡)I (d; d0) = = = = = = = = = = 1 0 1 ¡ CI (d) minfCI (d); DI (d)g maxfCI (d); DI (d)g sup d02¢I fmin(RI (d; d0); CI (d0))g inf d02¢I fmax(1 ¡ RI (d; d0); CI (d0))g sup d1;d2;:::;dp2¢I fmin1p(RI (d; di)g inf d1;d2;:::;dp+12¢I fmax1p+1(1 ¡ RI (d; di)g
RI (d0; d)
A F SHIN knowledge base (KB) K is a triple K=hT ; R; Ai, where T , R and A are F SHIN TBox, RBox and ABox. The syntax and semantics of axioms in them are given in table 1. An interpretation I satisfies an axiom if it satisfies corresponding semantics restriction given in table 1. I satisfies (is a fuzzy model of) a KB K, iff I satisfies any axiom in T , R and A. K is satisfiable iff it has a fuzzy model. In this paper, we will propose a discrete tableau algorithm to decide satisfiability of F SHIN KBs, which is based on the ”semantical discretization” discussed in the following section. For any fuzzy model of F SHIN KBs, we discretize it into a special model, in which any value of membership degree functions belongs to a given discrete degree set S. And we call it a discrete model within S. Let us now proceed formally in the creation of S. Let Nd be the set of degrees appearing in ABox Nd = fnj® ./ n 2 Ag. From Nd, we define the degree closure Nd¤ = f0; 0:5; 1g[Nd[fnj1¡n 2 Ndg and order degrees in ascending order: Nd¤ = fn0; n1; : : : ; nsg, where for any 0 · i · s, ni < ni+1. For any two back-to-back elements ni, ni+1 2 Nd¤, we insert their median mi+1 = (ni + ni+1)=2 to get S = fn0; m1; n1; : : : ; ns¡1; ms; nsg. We call S a discrete degree set w.r.t K. Obviously for any 1 · i · s, mi + ms+1¡i = 1 and ni¡1 < mi < ni.
Theorem 1 For any K=hT ; R; Ai and any discrete degree set S w.r.t K, iff K has a fuzzy model, it has a discrete model within S.
Proof. Let I = h¢I ; ¢I i be a fuzzy model of K and the degree set S = fn0; m1; n1; : : : ; ns¡1; ms; nsg. Consider a translation function '() : [0; 1] ! S: '(x) = ½ ni mi if x = ni if ni¡1 < x < ni
Based on '(), we will construct a discrete model Ic = h¢Ic ; ¢Ic i within S from I = h¢I ; ¢I i: ² The interpretation domain ¢Ic is defined as: ¢Ic = ¢I ; ² The interpretation function ¢Ic is defined as: for any individual name a, aIc = aI ; for any concept name A and any role name R:
AIc () = '(AI ()) and RIc () = '(RI ()). 1. For any concept C and role R and any d; d0 2 ¢Ic , we show, on induction on the structure of C and R, that CIc (d) = '(CI (d)) and RIc (d; d0) = '(RI (d; d0)): ² ¸ pR: (¸ pR)I (d) = sup d1;d2;:::;dp2¢I fmin1p(RI (d; di))g.
Let f (d0) = RI (d; d0), and f ¤(d0) = '(f (d)). Assume there are p elements d1¤; d2¤; : : : ; d¤p with the maximum value of f (): for any other d0 in ¢I , f (di¤) ¸ f (d0). Obviously from the property of '( ), for any other d0 in ¢Ic , f ¤(di¤) = '(f (di¤)) ¸ '(f (d)) = f ¤(d0). Then we get (¸ pR)Ic (d) = sup d1;d2;:::;dp2¢Ic fmin1p(f ¤(di))g = min1p(f ¤(di¤)) = '(min1p(f (di¤))) = '(sup d1;d2;:::;dp2¢I fmin1p(RI (d; di))g) = '((¸ pR)I (d)) 2. We show Ic is a fuzzy model of K.
² C v D 2 T : Obviously, 8d 2 ¢I = ¢Ic ; CI (d) · DI (d).
And from 1, for any concept C, CIc (d) = '(CI (d)). Therefore, CIc (d) = '(CI (d)) · '(DI (d)) = DIc (d);
Discrete Tableau Algorithms for F S HI N For a KB K, let RK and OK be the sets of roles and individuals appearing in K, and sub(K) the set of sub-concepts of all concepts in K. We also introduce Trans(R) as a boolean value to tell whether R is transitive, ¤ and ¢ as two placeholders for the inequalities ¸, > and ·, <, and the symbols ./¡, ¤¡ and ¢¡ to denote their reflections. A discrete tableau T for K within a degree set S is a quadruple: hO, L, E , Vi, where ² O: a nonempty set of nodes; ² L:O ! 2M , M = sub(K) £ f¸; >; ·; <g £ S; ² E : RK ! 2Q, Q = fO £ Og £ f¸; >; ·; <g £ S; ² V:OK ! O, maps any individual into a corresponding node in O.
From the definition of T, each node d is labelled with a set L(d)
of degree triples: hC; ./; ni, which denotes the membership degree
of d being an instance of C ./ n. In a discrete tableau T, for any
d; d0 2 O, a; b 2 OK, C; D 2 sub(K) and R 2 RK, the following
conditions, a extension of tableau conditions in dealing without
TBox [
with hC; ·; ni and hD; ¸; ni in L(d).
NNF condition: If hC; ./; ni 2 L(d), then hnnf(:C); ./¡; 1 ¡ ni 2 L(d). Here we use nnf(:C) to denote the equivalent form of :C in Negation Normal Form (NNF).
Theorem 2 For any K =< T ; R; A > and any discrete degree set S w.r.t K, K has a discrete model within S iff it has a discrete tableau T within S.
From theorem 1 and 2, an algorithm that constructs a discrete tableau of K within S can be considered as a decision procedure for the satisfiability of K. The discrete tableau algorithm works on a completion forest FK with a set S6= to denote ”6=” relation between nodes. The algorithm expands the forest FK either by extending L(x) for the current node x or by adding new leaf node y with expansion rules in table 2. A node y is called an Rsuccessor of another node x and x is called a R-predecessor of y, if hR; ./; ni 2 L(hx; yi). Ancestor is the transitive closure of predecessor. And for any two connected nodes x and y, we define DR(x; y)=fh./; nijP v¤ R; hP; ./; ni 2 L(hx; yi) or hInv(P ); ./ ; ni 2 L(hy; xi)g. If DR(x; y) 6= ;, y is called a R-neighbor of x.
The tableau algorithm initializes FK to contain a root node xa for
each individual a 2 OK and labels xa with L(xa)= fhC; ./; nija :
C ./ n 2 Ag; for any pair hxa; xbi, Lhxa; xbi=fhR; ./; nijha; bi :
R ./ n 2 Ag; and for any a 6= b 2 A, hxa; xbi 2 S6=. As
inverse role and number restriction are allowed in SHIN , we make
use of pairwise blocking technique [
9¤ rule: ¸ pR¤ rule:
The following rules are applied to nodes x which is not indirectly blocked.
if C v D 2 T and there is no n with hC; ·; ni and hD; ¸; ni in L(x); then L(x) ! L(x) [ fhC; ·; ni hD; ¸; nig for some n 2 S. if hC; ./; ni 2 L(x) and hnnf(:C); ./¡; ni 2= L(x); then L(x) ! L(x) [ fhnnf(:C); ./¡; nig. if hC u D; ¤; ni 2 L(x), and hC; ¤; ni or hD; ¤; ni 2= L(x); then L(x) ! L(x) [ fhC; ¤; ni; hD; ¤; nig. if hC t D; ¤; ni 2 L(x), and hC; ¤; ni; hD; ¤; ni 2= L(x) then L(x) ! L(x) [ fT g, for some T 2 fhC; ¤; ni; hD; ¤; nig The following rules are applied to nodes x which is not blocked.
if h8R:C; ¤; ni 2 L(x), there is a R-neighbor y of x with h¤0; mi 2 DR(x; y), which is conjugated with h¤¡; 1 ¡ ni and hC; ¤; ni 2= L(y); then L(y) ! L(y) [ fhC; ¤; nig. if h8P:C; ¤; ni 2 L(x), there is a R-neighbor y of x with R v¤ P , Trans(R)=True and h¤0; mi 2 DR(x; y), h¤0; mi is conjugated with h¤¡; 1 ¡ ni and h8R:C; ¤; ni 2= L(y); L(y) ! L(y) [ fh8R:C; ¤; nig: if h· pR; ¤; n 2 L(x); there is p + 1 R-successors y1; y2; : : : ; yp+1 of x with hR; ¤i; mii 2 L(hx; yii) and h¤i; mii is conjugated with h¢¡; 1 ¡ ni for any 1 · i · p + 1; and hyi; yj i 2= S6= for some 1 · i < j · p + 1 then merge two nodes yi and yj into one : L(yi) ! L(yi) [ L(yj ); 8x; L(yi; x) ! L(yi; x) [ L(yj ; x), hyj ; xi 2 S6=, add hyi; xi in S6= if h9R:C; ¤; ni 2 L(x); there is not a R-neighbor y of x with h¤; ni 2 DR(x; y) and hC; ¤; ni 2 L(y). then add a new node z with hR; ¤; ni 2 L(hx; zi) and hC; ¤; ni 2 L(z). if h¸ pR; ¤; ni 2 L(x), there are not p R-neighbors y1; y2; : : : ; yp of x with hR; ¤; ni 2 L(hx; yii) and for any i 6= j, hyi; yj i 2 S6=. then add p new nodes z1; z2; : : : ; zp with hR; ¤; ni 2 L(hx; zii) and for any two node zi and zj , add hzi; zj i in S6=. Theorem 3 For any K =< T ; R; A > and any discrete degree set S w.r.t K, K has a discrete tableau within S iff the tableau algorithm can construct a complete and clash-free completion forest. 5
In FDLs area, we have introduced a lot of work in introduction, all
that work are based on Straccia’ fuzzification framework. Here we
get into reasoning issue for fuzzy DLs. The first reasoning
algorithm was represented in [
In this paper, we point out a novel semantical discretization to discretize membership degree values in fuzzy models of F SHIN KBs, hence yielding ”discrete models”. Based on this discretization technique, we design a discrete tableau algorithm to construct discrete tableaus, which are abstraction of discrete models. From the equivalence of existence between fuzzy models and discrete models, our algorithm is a decision procedure to achieve reasoning with general TBox in F SHIN KBs. Our work can be considered as a logical foundation to support reasoning with fuzzy ontologies.