We study the fuzzy extension of FL0 with semantics based on the Gdel t-norm. We show that gfp-subsumption w.r.t. a nite set of primitive denitions can be characterized by a relation on weighted automata, and use this result to provide tight complexity bounds for reasoning in this logic.
Introduction
Fuzzy Description Logics (DLs) have been introduced as extensions of classical
DLs [
In the cases where the Gdel t-norm is used, the complexity of reasoning is
typically the same as for its classical version, as shown for EL, which is
polynomial [
To prove this complexity result, we characterize the greatest xed-point
semantics of G-FL0 by means of weighted automata over lattices. We then show
that reasoning with these automata can be reduced to a linear number of
inclusion tests between unweighted automata, which can be solved using only
polynomial space [
Preliminaries
We rst introduce some basic notions of lattice theory. For a more comprehensive
overview on the topic, refer to [
A lattice is an algebraic structure (L; _; ^) with two commutative, associative and idempotent binary operations _ (supremum) and ^ (inmum) that distribute over each other. It is complete if suprema and inma of arbitrary subsets S L, denoted by Wx2S x and Vx2S x respectively, exist. In this case, the lattice is bounded by the greatest element 1 := Wx2L x and the least element 0 := Vx2L x. Lattices induce a natural partial ordering on the elements of L where x y i x ^ y = x.
Example 1. One common complete lattice used in fuzzy logics (see e.g. [
We are particularly interested in operators on complete lattices L and their properties.
Denition 2 (xed-point). Let L be a complete lattice. A xed-point of an operator T : L ! L is an element x 2 L such that T (x) = x. It is the greatest xed-point of T if for any xed-point y of T we have y x.
The operator T is monotone if for all x; y 2 L, x y implies T (x) T (y). It is downward !-continuous if for every decreasing chain x0 x1 x2 : : : in L we have T (Vi 0 xi) = Vi 0 T (xi).
If it exists, the greatest xed-point of T is unique and denoted by gfp(T ).
It is easy to verify that every downward !-continuous operator is also
monotone. By a fundamental result from [
Our fuzzy DL is based on the well-known Gdel semantics for fuzzy logics,
which is one of the main t-norm-based semantics used in Mathematical Fuzzy
Logic [
y otherwise.
It is a fundamental property of a t-norm and its residuum that for all values x; y; z 2 [0; 1] we have x ^ y z i y x ) z. As with the Gdel t-norm, its residuum preserves arbitrary inma in its second component. However, in the rst component the order on [0; 1] is reversed.
Proposition 4. For any index set I and values x; xi 2 [0; 1], i 2 I, we have x ) ^ xi i2I = ^(x ) xi) and i2I _ xi i2I ) x = ^(xi ) x): i2I This shows that the residuum is monotone in the second argument and antitone in the rst argument. The following reformulation of nested residua in terms of inma will also prove useful.
Proposition 5. For all values x; x1; : : : ; xn 2 [0; 1], we have (x1 ^
^ xn) ) x = x1 ) : : : (xn ) x) : : : : Proof. Both values are either x or 1, and they are 1 i one of the operands 1 i n, is smaller than or equal to x. xi, tu 3
Fuzzy FL0 The fuzzy description logic G-FL0 has the same syntax as classical FL0. The dierence lies in the interpretation of G-FL0-concepts.
Denition 6 (syntax). Let NC and NR be two non-empty, disjoint sets of concept names and role names, respectively. Concepts are built from concept names using the constructors > (top), C u D (conjunction), and 8r:C (value restriction for a role name r).
A (primitive concept) denition is of the form hA v C pi, where A 2 NC, C is a concept, and p 2 [0; 1]. A TBox is a nite set of denitions. Given a TBox T , a concept name is dened if it appears on the left-hand side of a denition in T , and primitive otherwise.
We use the expression 8w:C with w = r1r2 : : : rn 2 NR to abbreviate the concept 8r1:8r2: : : : 8rn:C. We also allow w = ", in which case 8w:C is simply C. We denote the set of concept names occurring in the TBox T by NTC , the set of dened concept names in NTC by NTD , and the set of primitive concept names in NTC by NT . Likewise, we collect all role names occurring in T into the set NT .
P R Denition 7 (semantics). An interpretation is a pair I = ( I ; I ), where
I is a non-empty set, called the domain of I, and the interpretation function I maps every concept name A to a fuzzy set AI : I ! [0; 1] and every role name r to a fuzzy binary relation rI : I I ! [0; 1]. This function is extended to concepts by setting >I (x) := 1, (C u D)I (x) := CI (x) ^ DI (x), and (8r:C)I (x) := Vy2 I (rI (x; y) ) CI (y)) for all x 2 I .
The interpretation I satises (or is a model of ) the denition hA v C pi if AI (x) ) CI (x) p holds for all x 2 I . It satises (or is a model of ) a TBox if it satises all its denitions.
For an interpretation I = ( ; I ), w = r1r2 : : : rn 2 NR, and elements x0; xn 2 , we set wI (x0; xn) := Wx1;:::;xn 12 (r1I (x0; x1) ^ ^ rnI (xn 1; xn)), and can thus treat 8w:C like an ordinary value restriction with (8w:C)I (x0) :=
^ (wI (x0; xn) ) CI (xn)) = = xn2
^ x1;:::;xn2
^ x1;:::;xn2 = (8r1: : : : 8rn:C)I (x0) r1I (x0; x1) ^ ^ rnI (xn 1; xn)
) CI (xn) r1I (x0; x1) ) : : : (rnI (xn 1; xn) ) CI (xn)) : : : for all x0 2 (see Propositions 4 and 5).
It is convenient to consider TBoxes in normal form. The TBox T is in normal form if all denitions in T are of the form hA v 8w:B pi, where A; B 2 NC, w 2 NR, and p 2 [0; 1], and there are no two denitions hA v 8w:B pi, hA v 8w:B p0i with p 6= p0. Every TBox can be transformed into an equivalent TBox in normal form, as follows. First, we distribute the value restrictions over the conjunctions.
Lemma 8. For every r 2 NR, concepts C; D, and interpretation I = ( ; I ), it holds that (8r:(C u D))I = (8r:C u 8r:D)I .
Thus, we can equivalently write the right-hand sides of the denitions in T in the form 8w1:B1 u u 8wn:Bn, where wi 2 NR and Bi 2 NC [ f>g; 1 i n. Since 8r:> is equivalent to >, we can remove all conjuncts of the form 8w:> from this representation. After this transformation, all the denitions in the TBox are of the form hA v 8w1:B1 u u 8wn:Bn pi with Bi 2 NC; 1 i n, or hA v > pi. The latter axioms are tautologies, and can hence be removed from the TBox without aecting the semantics.
It follows from Proposition 4 that an interpretation I satises the denition hA v 8w1:B1 u u 8wn:Bn pi i it satises all the axioms hA v 8wi:Bi pi, 1 i n. Thus, the former axiom can be equivalently replaced by the latter set of axioms.
After these simplication steps, the TBox contains only axioms of the form hA v 8w:B pi with A; B 2 NC, satisfying the rst condition of the denition of normal form. Suppose now that T contains two axioms of the form hA v 8w:B pi and hA v 8w:B p0i with p > p0. Then T is equivalent to the TBox T n fhA v 8w:B p0ig; which means that this axiom can be removed. It is clear that all of these transformations can be done in polynomial time in the size of the original TBox.
Concept denitions can be seen as a restriction of the interpretation of the dened concepts, depending on the interpretation of the primitive concepts. We use this intuition and consider greatest xed-point semantics, as described next.
A primitive interpretation is a pair J = ( ; J ) as in Denition 7, except that J is only dened for role names and the primitive concept names in NTP . Given such a J , we use functions f 2 ([0; 1] )NDT to describe the interpretation of the remaining (dened) concept names. Recall from Example 1 that these functions form a complete lattice. In the following, we use the abbreviation LTJ := ([0; 1] )NDT for this lattice. Given a primitive interpretation J and a function f 2 LT , the induced interpretation IJ ;f has the same domain as J
J and extends the interpretation function of J to the dened concepts names A 2 NTD by taking AIJ ;f := f (A). The interpretation of the remaining concept names, i.e. those that do not occur in T , is xed to 0.
We can describe the eect that the axioms in T have on LT by the operator TJT : LTJ ! LTJ , which is dened as follows for all f 2 LTJ , A 2J NTD , and x 2 : T T (f )(A)(x) :=
J
(p ) CIJ ;f (x)): ^ hAvC pi2T This operator computes new values of the dened concept names according to the old interpretation IJ ;f and their denitions in T .
We are interested in using the greatest xed-point of T T , for some primitive interpretation J , to dene a new semantics for TBoxes T inJG-FL0. Before being able to do this, we have to ensure that such a xed-point always exists. Lemma 9. Given a TBox T and a primitive interpretation J = ( ; J ), the operator T T on LT is downward !-continuous.
J J uPsreootfh.eCaobnbsriedveirataiodnescrfea: =sinVg ich0afini, If0:= IfJ1;f , afn2d I:i :::=oIfJfu;fnicftoironasllini LTJ0,. aWnde have to show that TJT (f ) = Vi 0 TJT (fi) holds.
First, we prove by induction on the structure of C that CI = Vi 0 CIi holds for all concepts C built from NTR and NT , where V is dened as usual over the C complete lattice [0; 1] .
For A 2 NT , by the denition of IJ ;f and IJ ;fi we have AI = AJ = AIi for
P all i 0, and thus AI = AJ = Vi 0 AIi . For A 2 NTD , we have
AI = f (A) = ^ fi (A) = i 0 ^ fi(A) = i 0 ^ AIi by the denition of complete lattice LT .
J
IJ ;f and IJ ;fi and the component-wise ordering on the
For concepts of the form C uD, by the induction hypothesis and associativity of ^ we have (C u D)I = CI ^ DI = ^ CIi ^ Consider now a value restriction 8r:C. Using Proposition 4 we get for all x 2 , (8r:C)I (x) = ^ (rI (x; y) ) CI (y)) = ^
rI (x; y) ) y2 y2 ^ CIi (y) by the induction hypothesis, and the component-wise ordering on [0; 1] .
Using this, we can now prove the actual claim of the lemma. For all A 2 NTD and all x 2 , we get, using again Proposition 4 and the previous claim TJT (f )(A)(x) = =
^ hAvC pi2T
^ hAvC pi2T i 0 (p ) CI (x)) = ^ (p ) CIi (x)) =
^ by the denition of T T , and the component-wise ordering on LT .
J J tu By Proposition 3, we know that gfp(TJT ) exists and is equal to Vi 0(TJT )i(1), where 1 is the greatest element of the lattice LT that maps all dened concept J names to >J . In the following, we denote by gfpT (J ) the interpretation IJ ;f for f := gfp(TJT ). Note that I := gfpT (J ) is actually a model of T since for every hA v C pi 2 T and every x 2 we have
AI (x) = f (A)(x) = TJT (f )(A)(x) = (p0 ) C0I (x))
p ) CI (x); ^ hAvC0 p0i2T and thus p ^ AI (x) CI (x), which is equivalent to p AI (x) ) CI (x).
We can now dene the reasoning problem in G-FL0 that we want to solve. Denition 10 (gfp-subsumption). An interpretation I is a gfp-model of a TBox T if there is a primitive interpretation J such that I = gfpT (J ). Given A; B 2 NC and p 2 [0; 1], we say that A is gfp-subsumed by B to degree p w.r.t. T , written T j=gfp hA v B pi, if for every gfp-model I of T and every x 2 I we have AI (x) ) BI (x) p.
Let now T be a TBox and T 0 the result of transforming T into normal form as described before. It is easy to verify that the operators T T and T T 0 coincide, and therefore the gfp-models of T are the same as those of TJ0. To solve the problem J of deciding gfp-subsumptions, it thus suces to consider TBoxes in normal form.
Characterizing Subsumption using Finite Automata
To decide gfp-subsumption between concept names, we employ an
automatabased approach following the ideas from [
Denition 11 (WWA). A weighted automaton with word transitions (WWA) is a tuple A = ( ; Q; q0; wt; qf ), where is a nite alphabet of input symbols, Q is a nite set of states, q0 2 Q is the initial state, wt : Q Q ! [0; 1] is the transition weight function with the property that its support supp(wt) := f(q; w; q0) 2 Q
Q j wt(q; w; q0) > 0g is nite, and qf 2 Q is the nal state .
A nite path in A is a sequence = q0w1q1w2 : : : wnqn, where qi 2 Q and wi 2 for all i 2 f1; : : : ; ng, and qn = qf . Its label is the nite word `( ) := w1w2 : : : wn. The weight of is dened as wt( ) := Vin=1 wt(qi 1; wi; qi). The set of all nite paths with label w in A is denoted by paths(A; w). The behavior kAk : ! [0; 1] of A is dened as follows for every word w 2 : kAk(w) := W 2paths(A;w) wt( ).
If the image of the transition weight function is included in f0; 1g, then we have a
classical nite automaton with word transitions (WA). In this case, wt is usually
described as a subset of Q Q and the behavior is characterized by the
set L(A), called the language of A, of all words for which the behavior is 1.
The inclusion problem for WA is to decide, given two such automata A and A0,
whether L(A) L(A0). This problem is known to be PSpace-complete [
Our goal is to describe the restrictions imposed by a G-FL0 TBox T using a WWA. For the rest of this paper, we assume w.l.o.g. that T is in normal form. Denition 12 (automata ATA;B). For concept names A; B 2 NTC , the WWA ATA;B = (NR; NTC ; A; wtT ; B) is dened by the transition weight function wtT (A0; w; B0) := (p if hA0 v 8w:B0 0 otherwise.
pi 2 T , Notice that for a given TBox T and concept names A; A0; B; B0 2 NT , the C automata ATA;B and ATA0;B0 dier only on the initial and nal states they dene; their sets of states and transition weight function are identical. Since T is in normal form, for any two concept names A0; B0 2 NTC and w 2 NR, there is at most one axiom hA0 v 8w:B0 pi in T , and hence the transition weight function is well-dened. This function has nite support since T is nite.
We now characterize the gfp-models of T by properties of the automata ATA;B. Lemma 13. For every gfp-model I = ( ; I ) of T , x 2 , and A 2 NT ,
C AI (x) = ^
^ Proof. If A is primitive, then the empty path = A 2 paths(ATA;A; ") has weight wtT ( ) = 1, and hence kATA;Ak(") = 1. We also have (8":A)I (x) = AI (x); thus, AI (x) = (1 ) AI (x)) V
B2NPT Vw2NR kATA;Bk(w) ) (8w:B)I (x) . Let now B 2 NTP and w 2 NR such that A 6= B or w 6= ". Since A is primitive, by Denition 12 any nite path in ATA;B with `( ) = w must have weight 0; i.e. kATA;Bk(w) = 0, and thus 0 ) (8w:B)I (x) = 1 AI (x). This shows that the whole inmum is equal to AI (x).
Consider now the case that A 2 NTD . Since I is a gfp-model of T , there is a primitive interpretation J such that I = gfpT (J ); let f := gfp(TJT ). Thus, we have AI = f (A) = TJT (f )(A) = Vi 0(TJT )i(1)(A) for all A 2 NTD . [ ] For the -direction, by Proposition 4 it suces to show that for all A 2 NTD , B 2 NTP , and all nite non-empty paths in ATA;B it holds that where w := `( ). This obviously holds for wtT ( ) = 0, and thus it remains to show this for paths with positive weight. Let = Aw1A1w2 : : : wnAn, where Ai 2 NTC and wi 2 NR for all i 2 f1; : : : ; ng and An = B is the only primitive concept name in this path. We prove (1) by induction on n. For n = 1, we have = Aw1B and wtT (A; w1; B) = wtT ( ) > 0, and thus T contains the denition hA v 8w1:B pi, with p := wtT (A; w1; B). By the denition of TJT , we obtain AI (x) = TJT (f )(A)(x)
p ) (8w1:B)I (x) = wtT ( ) ) (8w:B)I (x): For n > 1, consider the subpath 0 = A1w2 : : : wnB in ATA1;B with the label `( 0) = w0 := w2 : : : wn. For all y 2 , the induction hypothesis yields that A1I (y) wtT ( 0) ) (8w0:B)I (y). Again, p := wtT (A; w1; A1) wtT ( ) > 0, awntTd (th)u,swTI ,caonndtaPinrsopthoesidtieonnisti4onandhA5,vw8ewh1a:vAe1 pi. By the denitions of TJT , (1) AI (x) = TJT (f )(A)(x)
p ) (8w1:A1)I (x) = ^ p ) (w1I (x; y) ) A1I (y)) y2 ^ p ) y2 w1I (x; y) )
wtT ( 0) ) (8w0:B)I (y) ^ y2 = p ^ wtT ( 0) )
w1I (x; y) ) (8w0:B)I (y) = wtT ( ) ) (8w:B)I (x) [ ] For the -direction, we show by induction on i that for all x 2 and i 0, it holds that , A 2 NTD , (TJT )i(1)(A)(x) ^
^ For i = 0, we have (TJT )0(1)(A)(x) = 1(A)(x) = 1, which obviously satises (2). For i > 0, by Proposition 4 we obtain (3) pi 2 T .
= (TJT )i(1)(A)(x) = TJT ((TJT )i 1(1))(A)(x) ^
(p ) (8w0:A0)Ii 1 (x)); hAv8w0:A0 pi2T where Ii 1 := IJ ;(TJT )i 1(1). Consider now any denition hA v 8w0:A0 Then 0 = Aw0A0 is a nite path in ATA;A0 with label w0 and weight p.
If A0 is a primitive concept name, then we have p ) (8w0:A0)Ii 1 (x) = wtT ( 0) ) (8w0:A0)I (x) kATA;A0 k(w0) ) (8w0:A0)I (x) by the denition of kATA;A0 k(w0) and the fact that the interpretation of 8w0:A0 under Ii 1 and I only depends on J . If A0 is dened, then we similarly get p ) (8w0:A0)Ii 1 (x)
y2 B2NPT w2NR = ^ p ) y2 ^ ^ = ^ = ^
^ ^ w0I (x; y) ) (8w:B)I (y) y2 _ 2paths(ATA0;B;w) kATA;Bk(w0w) ) (8w0w:B)I (x) (wtT ( 0) ^ wtT ( )) ) (8w0w:B)I (x) by the induction hypothesis, Propositions 4 and 5, and the denition of kATA;Bk.
In both cases, p ) (8w0:A0)Ii 1 (x) is an upper bound for the inmum on the right-hand side of (2), and thus by (3) the same is true for (TJT )i(1)(A)(x). tu This allows us to prove gfp-subsumptions by comparing the behavior of WWA. Lemma 14. Let A; B 2 NTC and p 2 [0; 1]. Then T j=gfp hA v B C 2 NTP and w 2 NR it holds that p ^ kATB;C k(w) kATA;C k(w). Proof. Assume that there exist C 2 NT and w = r1 : : : rn 2 NR such that P p^kATB;C k(w) > kATA;C k(w). We dene the primitive interpretation J = ( ; J ) where := fx0; : : : ; xng, and for all D 2 NTP and r 2 NR, the interpretation function is given by
DJ (x) := (kATA;C k(w) if D = C and x = xn,
1 otherwise; and rJ (x; y) := (1 if x = xi 1, y = xi, and r = ri for some i 2 f1; : : : ; ng,
0 otherwise.
Consider now the gfp-model I := gfpT (J ) of T . By construction, for all pairs (w0; D) 2 NR NTP n f(w; C)g we have (8w0:D)I (x0) = 1. Moreover, we know that (8w:C)I (x0) is equal to kATA;C k(w), and thus strictly smaller than p and kATB;C k(w). By Lemma 13, all this implies that
AI (x0) = kATA;C k(w) ) (8w:C)I (x0) = 1 and
BI (x0) = kATB;C k(w) ) (8w:C)I (x0) = (8w:C)I (x0): Thus AI (x0) ) BI (x0) = (8w:C)I (x0) < p, and T 6j=gfp hA v B pi.
Conversely, assume that there are a primitive interpretation J = ( ; J ) and an element x 2 such that AI (x) ) BI (x) < p, where I := gfpT (J ). Thus, we have p ^ AI (x) > BI (x), which implies by Lemma 13 the existence of a C 2 NT P and a w 2 NR with p ^ AI (x) > kATB;C k(w) ) (8w:C)I (x). Again by Lemma 13, this implies that p ^ kATB;C k(w) > AI (x) ) (8w:C)I (x)
kATA;C k(w) ) (8w:C)I (x) ) (8w:C)I (x): In particular, the latter value cannot be 1, and thus it is equal to (8w:C)I (x). But this can only be the case if kATA;C k(w) (8w:C)I (x). To summarize, we obtain p ^ kATB;C k(w) > (8w:C)I (x) kATA;C k(w), as desired. tu Denote by VT := f0; 1g [ fp 2 [0; 1] j hA v 8w:B pi 2 T g the set of all values appearing in T , together with 0 and 1. Since wtT has nite support and takes only values from
VT , p ^ kATB;C k(w) > kATA;C k(w) holds i p0 ^ kATB;C k(w) > kATA;C k(w), where p0 is the smallest element of VT such that p0 p. This shows that it suces to be able to check gfp-subsumptions for the values in VT . We now show how to do this by simulating ATB;C and ATA;C by polynomially many unweighted automata.
Denition 15 (automata A p). Given a WWA A = ( ; Q; q0; wt; qf ) and a value p 2 [0; 1], the WA A p = ( ; Q; q0; wt p; qf ) is given by the transition relation wt p := f(q; w; q0) 2 Q Q j wt(q; w; q0) pg.
The language of this automaton has an obvious relation to the behavior of the original WWA.
Lemma 16. Let A be a WWA over the alphabet and p 2 [0; 1]. Then we have L(A p) = fw 2 j kAk(w) pg.
Proof. We have w 2 L(A p) i there is a nite path = q0w1q1 : : : wnqn in A with label w such that wt(qi 1; wi; qi) p holds for all i 2 f1; : : : ; ng. The latter condition is equivalent to the fact that wt( ) p. Thus, w 2 L(A p) implies that kAk(w) p. Conversely, since wt has nite support, there are only nitely many possible weights for any nite path in A, and thus kAk(w) p also implies that there exists a 2 paths(A; w) with wt( ) p, and thus w 2 L(A p). tu We thus obtain the following characterization of gfp-subsumption. Lemma 17. Let A; B 2 NTC and p 2 VT . Then T j=gfp hA v B C 2 NTP and p0 2 VT with p0 p it holds that L((ATB;C ) p0 ) L((ATA;C ) p0 ). For the value p0 := p ^ kATB;C k(w) 2 VT \ [0; p], we have kATB;C k(w) kATA;C k(w) < p0, and thus L((ATB;C ) p0 ) * L((ATA;C ) p0 ) by Lemma 16.
Proof. By the reductions above, it suces to decide the language inclusions
L((ATB;C ) p) L((ATA;C ) p) for all C 2 NTP and p 2 VT . These polynomially
many inclusion tests for WA can be done in polynomial space [
Conclusions We have studied the complexity of reasoning in G-FL0 w.r.t. primitive concept denitions under greatest xed-point semantics. More precisely, we have shown that gfp-subsumption between concept names can be reduced to a comparison of the behavior of weighted automata with word transitions. Moreover, the latter can be solved by a polynomial number of inclusion tests on unweighted automata. Overall, this shows that gfp-subsumption is PSpace-complete for this logic, just as in the classical case.
This complexity result is consistent with previous work on extensions of
description logics with Gdel semantics. Indeed, such extensions of EL [
We expect our results to generalize easily to any other set of truth degrees
that form a total order. However, the arguments used in this paper fail for
arbitrary lattices, where incomparable truth degrees might exist [