=Paper=
{{Paper
|id=Vol-1193/paper_3
|storemode=property
|title=Gödel FL_0 with Greatest Fixed-Point Semantics
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_3.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/BorgwardtGP14
}}
==Gödel FL_0 with Greatest Fixed-Point Semantics==
https://ceur-ws.org/Vol-1193/paper_3.pdf
Gödel FL0 with Greatest Fixed-Point Semantics?
Stefan Borgwardt1 , José A. Leyva Galano1 , and Rafael Peñaloza1,2
1
Theoretical Computer Science, TU Dresden, Germany
2
Center for Advancing Electronics Dresden
{stefborg,penaloza}@tcs.inf.tu-dresden.de jleyva1@gmail.com
Abstract. We study the fuzzy extension of FL0 with semantics based
on the Gödel t-norm. We show that gfp-subsumption w.r.t. a nite set
of primitive de nitions can be characterized by a relation on weighted
automata, and use this result to provide tight complexity bounds for
reasoning in this logic.
1 Introduction
Fuzzy Description Logics (DLs) have been introduced as extensions of classical
DLs [2] capable of representing and reasoning with vague or imprecise knowledge.
The main idea behind these logics is to allow for a set of truth degrees, beyond the
standard true and false. The area of fuzzy DLs recently experienced a shift, when
it was shown that reasoning in these logics easily becomes undecidable [3,6,8].
To guarantee decidability in fuzzy DLs, one can (i) restrict the semantics to
consider nitely many truth degrees [7]; (ii) allow only acyclic or unfoldable
ontologies [4,18]; or (iii) restrict to Zadeh or Gödel semantics [5,15,16,17].
In the cases where the Gödel t-norm is used, the complexity of reasoning is
typically the same as for its classical version, as shown for EL, which is poly-
nomial [15,16], and ALC , ExpTime-complete [5]. This latter result immediately
implies that reasoning in G-FL0 with general TBoxes is also ExpTime-complete.
On the other hand, if TBoxes are restricted to contain only (primitive) de ni-
tions, then deciding subsumption in classical FL0 under the greatest xed-point
semantics is known to be in PSpace [1]. We show that the same complexity
bound holds for the Gödel extension of this logic.
To prove this complexity result, we characterize the greatest xed-point se-
mantics 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 in-
clusion tests between unweighted automata, which can be solved using only
polynomial space [10].
?
Partially supported by the DFG under grant BA 1122/17-1, in the research train-
ing group 1763 (QuantLA), and the Cluster of Excellence `Center for Advancing
Electronics Dresden'.
2 Preliminaries
We rst introduce some basic notions of lattice theory. For a more comprehensive
overview on the topic, refer to [11]. Afterwards, we introduce fuzzy logics based
on Gödel semantics, which are studied in more detail in [9,12,14].
A lattice is an algebraic structure (L, ∨, ∧) with two commutative, associa-
tive and idempotent binary operations ∨ (supremum) and ∧ (in mum) that
W It is complete
distribute over each other. V if suprema and in ma of arbitrary sub-
sets S ⊆ L, denoted by x∈S x and x∈S x respectively, exist. In this case, the
latticeVis bounded by the greatest element 1 := x∈L x and the least element
W
0 := x∈L 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. [9,12])
is the interval [0, 1] with the usual order on the real numbers. Further complete
lattices relevant for this paper can be constructed as follows. Given a complete
lattice L and a set S , the set LS of all functions f : S → L is also a complete
lattice, if in mum and supremum are de ned component-wise. More precisely, for
any two f1 , f2 ∈ LS , we de ne f1 ∨f2 for all x ∈ S as (f1 ∨f2 )(x) := f1 (x)∨f2 (x).
If we similarly de ne the in mum, we obtain a lattice with the order f1 ≤ f2
i f1 (x) ≤ f2 (x) holds for all x ∈ S . It is easy to verify that in nite in ma and
suprema can then also be computed component-wise.
We are particularly interested in operators on complete lattices L and their
properties.
De nition 2 ( xed-point). Let L be a complete lattice. A xed-point of an
operator T : L → L is an element x ∈ 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 ∈ L, x ≤ y implies T (x) ≤ T (y).
It is downward ωV-continuousV if for every decreasing chain x0 ≥ x1 ≥ x2 ≥ . . .
in L we have T ( i≥0 xi ) = i≥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 mono-
tone. By a fundamental result from [20], every monotone operator T has a great-
est xed-point. If T is downward ω -continuous, then gfp(T ) corresponds to the
in mum of the decreasing chain 1 ≥ T (1) ≥ T (T (1)) ≥ · · · ≥ T i (1) ≥ . . . [13].
Proposition 3. If L is a complete lattice and T a downward ω-continuous op-
erator on L, then gfp(T ) = i≥0 T i (1).
V
Our fuzzy DL is based on the well-known Gödel semantics for fuzzy logics,
which is one of the main t-norm-based semantics used in Mathematical Fuzzy
Logic [9,12]. This semantics is based on the standard interval [0, 1]. The Gödel
t-norm is the binary minimum operator on this set. For consistency, we use
the lattice-theoretic notation ∧ instead of min. Two important properties of
this
V operator are V that itpreserves W
arbitrary in ma W and suprema on [0, 1], i.e.
and for any index
i∈I (x i ∧ x) = i∈I x i ∧ x i∈I (x i ∧ x) = i∈I x i ∧ x
set I and elements x, xi ∈ [0, 1] for all i ∈ I . In particular, this means that
the Gödel t-norm is monotone in both arguments. The residuum of the Gödel
t-norm is the binary operator ⇒ on [0, 1] de ned for all x, y ∈ [0, 1] by
if x ≤ y ,
(
1
x ⇒ y :=
y otherwise.
It is a fundamental property of a t-norm and its residuum that for all values
x, y, z ∈ [0, 1] we have x ∧ y ≤ z i y ≤ x ⇒ z . As with the Gödel t-norm, its
residuum preserves arbitrary in ma 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 ∈ [0, 1], i ∈ I , we have
and
^ ^ _ ^
x⇒ xi = (x ⇒ xi ) xi ⇒ x = (xi ⇒ x).
i∈I i∈I i∈I i∈I
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
in ma will also prove useful.
Proposition 5. For all values x, x1 , . . . , xn ∈ [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 xi ,
1 ≤ i ≤ n, is smaller than or equal to x. t
u
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.
De nition 6 (syntax). Let NC and NR be two non-empty, disjoint sets of con-
cept names and role names, respectively. Concepts are built from concept names
using the constructors > (top), C u D (conjunction), and ∀r.C (value restriction
for a role name r).
A (primitive concept) de nition is of the form hA v C ≥ pi, where A ∈ NC ,
C is a concept, and p ∈ [0, 1]. A TBox is a nite set of de nitions. Given
a TBox T , a concept name is de ned if it appears on the left-hand side of a
de nition in T , and primitive otherwise.
We use the expression ∀w.C with w = r1 r2 . . . rn ∈ N∗R to abbreviate the concept
∀r1 .∀r2 . . . . ∀rn .C . We also allow w = ε, in which case ∀w.C is simply C . We
denote the set of concept names occurring in the TBox T by NTC , the set of
de ned concept names in NTC by NTD , and the set of primitive concept names
in NTC by NTP . Likewise, we collect all role names occurring in T into the set NTR .
De nition 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 func-
tion ·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) := C I (x) ∧ DI (x), and
(∀r.C) (x) := y∈∆ (rI (x, y) ⇒ C I (y)) for all x ∈ ∆I .
I
V
I
The interpretation I satis es (or is a model of) the de nition hA v C ≥ pi
if AI (x) ⇒ C I (x) ≥ p holds for all x ∈ ∆I . It satis es (or is a model of) a
TBox if it satis es all its de nitions.
For an interpretation W
I = (∆, ·I ), w = r1 r2 . . . rn ∈ N∗R , and elements x0 , xn ∈ ∆,
we set w (x0 , xn ) := x1 ,...,xn−1 ∈∆ (r1I (x0 , x1 ) ∧ · · · ∧ rnI (xn−1 , xn )), and can thus
I
treat ∀w.C like an ordinary value restriction with
^
(∀w.C)I (x0 ) := (wI (x0 , xn ) ⇒ C I (xn ))
xn ∈∆
^
r1I (x0 , x1 ) ∧ · · · ∧ rnI (xn−1 , xn ) ⇒ C I (xn )
=
x1 ,...,xn ∈∆
^
r1I (x0 , x1 ) ⇒ . . . (rnI (xn−1 , xn ) ⇒ C I (xn )) . . .
=
x1 ,...,xn ∈∆
= (∀r1 . . . . ∀rn .C)I (x0 )
for all x0 ∈ ∆ (see Propositions 4 and 5).
It is convenient to consider TBoxes in normal form. The TBox T is in normal
form if all de nitions in T are of the form hA v ∀w.B ≥ pi, where A, B ∈ NC ,
w ∈ N∗R , and p ∈ [0, 1], and there are no two de nitions hA v ∀w.B ≥ pi,
hA v ∀w.B ≥ p0 i 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 ∈ NR , concepts C, D, and interpretation I = (∆, ·I ), it
holds that (∀r.(C u D))I = (∀r.C u ∀r.D)I .
Thus, we can equivalently write the right-hand sides of the de nitions in T in the
form ∀w1 .B1 u · · · u ∀wn .Bn , where wi ∈ N∗R and Bi ∈ NC ∪ {>}, 1 ≤ i ≤ n. Since
∀r.> is equivalent to >, we can remove all conjuncts of the form ∀w.> from
this representation. After this transformation, all the de nitions in the TBox
are of the form hA v ∀w1 .B1 u · · · u ∀wn .Bn ≥ pi with Bi ∈ 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 satis es the de nition
hA v ∀w1 .B1 u · · · u ∀wn .Bn ≥ pi i it satis es all the axioms hA v ∀wi .Bi ≥ pi,
1 ≤ i ≤ n. Thus, the former axiom can be equivalently replaced by the latter set
of axioms.
After these simpli cation steps, the TBox contains only axioms of the form
hA v ∀w.B ≥ pi with A, B ∈ NC , satisfying the rst condition of the de -
nition of normal form. Suppose now that T contains two axioms of the form
hA v ∀w.B ≥ pi and hA v ∀w.B ≥ p0 i with p > p0 . Then T is equivalent to the
TBox T \ {hA v ∀w.B ≥ p0 i}; 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 de nitions can be seen as a restriction of the interpretation of the
de ned 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 De nition 7, except
that ·J is only de ned for role names and the primitive concept names in NTP .
Given such a J , we use functions f ∈ ([0, 1]∆ )ND to describe the interpretation
T
of the remaining (de ned) concept names. Recall from Example 1 that these
functions form a complete lattice. In the following, we use the abbreviation
LTJ := ([0, 1]∆ )ND for this lattice. Given a primitive interpretation J and a
T
function f ∈ LTJ , the induced interpretation IJ ,f has the same domain as J
and extends the interpretation function of J to the de ned concepts names
A ∈ 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 LTJ by the operator
TJ : LTJ → LTJ , which is de ned as follows for all f ∈ LTJ , A ∈ NTD , and x ∈ ∆:
T
^
TJT (f )(A)(x) := (p ⇒ C IJ ,f (x)).
hAvC≥pi∈T
This operator computes new values of the de ned concept names according to
the old interpretation IJ ,f and their de nitions in T .
We are interested in using the greatest xed-point of TJT , for some primitive
interpretation J , to de ne a new semantics for TBoxes T in G-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 TJT on LTJ is downward ω-continuous.
Proof. Consider a decreasingV chain f0 ≥ f1 ≥ f2 ≥ . . . of functions in LJ . We
T
use the abbreviations f := i≥0 fi , I := IJ ,f , and Ii := IJ ,fi for all i ≥ 0, and
have to show that TJT (f ) = i≥0 TJT (fi ) holds.
V
First, we prove by induction on the structure ofVC that C I = i≥0 C Ii holds
V
for all concepts C built from NTR and NTC , where is de ned as usual over the
complete lattice [0, 1]∆ .
For A ∈ NTP , by the de nition
V of IJ ,f and IJ ,fi we have A = A = A for
I J Ii
all i ≥ 0, and thus AI = AJ = i≥0 AIi . For A ∈ NTD , we have
^ ^ ^
AI = f (A) = fi (A) = fi (A) = AIi
i≥0 i≥0 i≥0
by the de nition of IJ ,f and IJ ,fi and the component-wise ordering on the
complete lattice LTJ .
For concepts of the form C uD, by the induction hypothesis and associativity
of ∧ we have
^ ^ ^ ^
(C u D)I = C I ∧ DI = C Ii ∧ DIi = (C Ii ∧ DIi ) = (C u D)Ii .
i≥0 i≥0 i≥0 i≥0
Consider now a value restriction ∀r.C . Using Proposition 4 we get for all x ∈ ∆,
^ ^ ^
(∀r.C)I (x) = (rI (x, y) ⇒ C I (y)) = rI (x, y) ⇒ C Ii (y)
y∈∆ y∈∆ i≥0
^ ^ ^ ^
Ii Ii Ii
= (r (x, y) ⇒ C (y)) = (∀r.C) (x) = (∀r.C)Ii (x)
y∈∆ i≥0 i≥0 i≥0
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 ∈ NTD
and all x ∈ ∆, we get, using again Proposition 4 and the previous claim
^ ^ ^
TJT (f )(A)(x) = (p ⇒ C I (x)) = p⇒ C Ii (x)
hAvC≥pi∈T hAvC≥pi∈T i≥0
^ ^ ^
= (p ⇒ C Ii (x)) = TJT (fi ) (A)(x)
hAvC≥pi∈T i≥0 i≥0
by the de nition of TJT , and the component-wise ordering on LTJ . t
u
By Proposition 3, we know that gfp(TJT ) exists and is equal to i≥0 (TJT )i (1),
V
where 1 is the greatest element of the lattice LTJ that maps all de ned concept
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 ∈ T and every x ∈ ∆ we have
^
AI (x) = f (A)(x) = TJT (f )(A)(x) = (p0 ⇒ C 0I (x)) ≤ p ⇒ C I (x),
hAvC 0 ≥p0 i∈T
and thus p ∧ AI (x) ≤ C I (x), which is equivalent to p ≤ AI (x) ⇒ C I (x).
We can now de ne the reasoning problem in G-FL0 that we want to solve.
De nition 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 ∈ NC and p ∈ [0, 1], we say that A is gfp-subsumed by B to degree p
w.r.t. T , written T |=gfp hA v B ≥ pi, if for every gfp-model I of T and every
x ∈ ∆I we have AI (x) ⇒ B I (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 TJT and TJT coincide, and
0
therefore the gfp-models of T are the same as those of T 0 . To solve the problem
of deciding gfp-subsumptions, it thus su ces to consider TBoxes in normal form.
4 Characterizing Subsumption using Finite Automata
To decide gfp-subsumption between concept names, we employ an automata-
based approach following the ideas from [1]. In contrast to that paper, however,
we use a weighted automata model.
De nition 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 ∈ Q is the initial state, wt : Q × Σ ∗ × Q → [0, 1]
is the transition weight function with the property that its support
supp(wt) := {(q, w, q 0 ) ∈ Q × Σ ∗ × Q | wt(q, w, q 0 ) > 0}
is nite, and qf ∈ Q is the nal state.
A nite path in A is a sequence π = q0 w1 q1 w2 . . . wn qn , where qi ∈ Q
and wi ∈ Σ ∗ for all i ∈ {1, . . . , n}, and qn = qf . Its label
Vn is the nite word
`(π) := w1 w2 . . . wn . The weight of π is de ned as wt(π) := i=1 wt(qi−1 , wi , qi ).
The set of all nite paths with label w in A is denoted by paths(A, w). The be-
havior kAkW : Σ ∗ → [0, 1] of A is de ned as follows for every word w ∈ Σ ∗ :
kAk(w) := π∈paths(A,w) wt(π).
If the image of the transition weight function is included in {0, 1}, 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 [10].
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.
De nition 12 (automata ATA,B ). For concept names A, B ∈ NTC , the WWA
ATA,B = (NR , NTC , A, wtT , B) is de ned by the transition weight function
if hA0 v ∀w.B 0 ≥ pi ∈ T ,
(
0 0 p
wtT (A , w, B ) :=
0 otherwise.
Notice that for a given TBox T and concept names A, A0 , B, B 0 ∈ NTC , the
automata ATA,B and ATA0 ,B0 dier only on the initial and nal states they de ne;
their sets of states and transition weight function are identical. Since T is in
normal form, for any two concept names A0 , B 0 ∈ NTC and w ∈ N∗R , there is at
most one axiom hA0 v ∀w.B 0 ≥ pi in T , and hence the transition weight function
is well-de ned. 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 ∈ ∆, and A ∈ NTC ,
^ ^
AI (x) = kATA,B k(w) ⇒ (∀w.B)I (x) .
B∈NT
P
w∈N∗
R
Proof. If A is primitive, then the empty path π = A ∈ paths(ATA,A , ε) has
weight wtT (π) = 1, and hence kATA,A k(ε) = 1. We also have (∀ε.A)I (x) = AI (x);
thus, AI (x) = (1 ⇒ AI (x)) ≥ B∈NTP w∈N∗R kATA,B k(w) ⇒ (∀w.B)I (x) . Let
V V
now B ∈ NTP and w ∈ N∗R such that A 6= B or w 6= ε. Since A is primitive, by
De nition 12 any nite path π in ATA,B with `(π) = w must have weight 0; i.e.
kATA,B k(w) = 0, and thus 0 ⇒ (∀w.B)I (x) = 1 ≥ AI (x). This shows that the
whole in mum is equal to AI (x).
Consider now the case that A ∈ NTD . Since I is a gfp-model of T , there is a
primitive interpretation J such V
that I = gfpT (J ); let f := gfp(TJT ). Thus, we
have A = f (A) = TJ (f )(A) = i≥0 (TJT )i (1)(A) for all A ∈ NTD .
I T
[≤] For the ≤-direction, by Proposition 4 it su ces to show that for all x ∈ ∆,
A ∈ NTD , B ∈ NTP , and all nite non-empty paths π in ATA,B it holds that
AI (x) ≤ wtT (π) ⇒ (∀w.B)I (x), (1)
where w := `(π). This obviously holds for wtT (π) = 0, and thus it remains to
show this for paths with positive weight. Let π = Aw1 A1 w2 . . . wn An , where
Ai ∈ NTC and wi ∈ N∗R for all i ∈ {1, . . . , n} and An = B is the only primitive
concept name in this path. We prove (1) by induction on n. For n = 1, we have
π = Aw1 B and wtT (A, w1 , B) = wtT (π) > 0, and thus T contains the de nition
hA v ∀w1 .B ≥ pi, with p := wtT (A, w1 , B). By the de nition of TJT , we obtain
AI (x) = TJT (f )(A)(x) ≤ p ⇒ (∀w1 .B)I (x) = wtT (π) ⇒ (∀w.B)I (x).
For n > 1, consider the subpath π 0 = A1 w2 . . . wn B in ATA1 ,B with the label
`(π 0 ) = w0 := w2 . . . wn . For all y ∈ ∆, the induction hypothesis yields that
AI1 (y) ≤ wtT (π 0 ) ⇒ (∀w0 .B)I (y). Again, p := wtT (A, w1 , A1 ) ≥ wtT (π) > 0,
and thus T contains the de nition hA v ∀w1 .A1 ≥ pi. By the de nitions of TJT ,
wtT (π), wI , and Propositions 4 and 5, we have
AI (x) = TJT (f )(A)(x)
≤ p ⇒ (∀w1 .A1 )I (x)
^
p ⇒ (w1I (x, y) ⇒ AI1 (y))
=
y∈∆
^
≤ p ⇒ w1I (x, y) ⇒ wtT (π 0 ) ⇒ (∀w0 .B)I (y)
y∈∆
^
= p ∧ wtT (π 0 ) ⇒ w1I (x, y) ⇒ (∀w0 .B)I (y)
y∈∆
I
= wtT (π) ⇒ (∀w.B) (x)
[≥] For the ≥-direction, we show by induction on i that for all x ∈ ∆, A ∈ NTD ,
and i ≥ 0, it holds that
(2)
^ ^
(TJT )i (1)(A)(x) ≥ kATA,B k(w) ⇒ (∀w.B)I (x) .
B∈NT
P
w∈N∗
R
For i = 0, we have (TJT )0 (1)(A)(x) = 1(A)(x) = 1, which obviously satis es (2).
For i > 0, by Proposition 4 we obtain
(TJT )i (1)(A)(x) = TJT ((TJT )i−1 (1))(A)(x)
(3)
^
= (p ⇒ (∀w0 .A0 )Ii−1 (x)),
hAv∀w0 .A0 ≥pi∈T
where Ii−1 := IJ ,(TJT )i−1 (1) . Consider now any de nition hA v ∀w0 .A0 ≥ pi ∈ T .
Then π 0 = Aw0 A0 is a nite path in ATA,A0 with label w0 and weight p.
If A0 is a primitive concept name, then we have
p ⇒ (∀w0 .A0 )Ii−1 (x) = wtT (π 0 ) ⇒ (∀w0 .A0 )I (x) ≥ kATA,A0 k(w0 ) ⇒ (∀w0 .A0 )I (x)
by the de nition of kATA,A0 k(w0 ) and the fact that the interpretation of ∀w0 .A0
under Ii−1 and I only depends on J . If A0 is de ned, then we similarly get
p ⇒ (∀w0 .A0 )Ii−1 (x)
^
= p ⇒ w0J (x, y) ⇒ A0Ii−1 (y)
y∈∆
^ ^ ^
≥ p ⇒ w0I (x, y) ⇒ (kATA0 ,B k(w) ⇒ (∀w.B)I (y))
y∈∆ B∈NT
P
w∈N∗
R
^ ^ ^
p ∧ kATA0 ,B k(w) ⇒ w0I (x, y) ⇒ (∀w.B)I (y)
=
B∈NT
P
w∈N∗
R y∈∆
^ ^ _
= (wtT (π 0 ) ∧ wtT (π)) ⇒ (∀w0 w.B)I (x)
B∈NT w∈N∗
R π∈paths(AT ,w)
P A0 ,B
^ ^
kATA,B k(w0 w) ⇒ (∀w0 w.B)I (x)
≥
B∈NT
P
w∈N∗
R
by the induction hypothesis, Propositions 4 and 5, and the de nition of kATA,B k.
In both cases, p ⇒ (∀w0 .A0 )Ii−1 (x) is an upper bound for the in mum on the
right-hand side of (2), and thus by (3) the same is true for (TJT )i (1)(A)(x). t
u
This allows us to prove gfp-subsumptions by comparing the behavior of WWA.
Lemma 14. Let A, B ∈ NTC and p ∈ [0, 1]. Then T |=gfp hA v B ≥ pi i for all
C ∈ NTP and w ∈ N∗R it holds that p ∧ kATB,C k(w) ≤ kATA,C k(w).
Proof. Assume that there exist C ∈ NTP and w = r1 . . . rn ∈ N∗R such that
p∧kATB,C k(w) > kATA,C k(w). We de ne the primitive interpretation J = (∆, ·J )
where ∆ := {x0 , . . . , xn }, and for all D ∈ NTP and r ∈ NR , the interpretation
function is given by
kATA,C k(w) if D = C and x = xn ,
(
J
D (x) :=
1 otherwise; and
1 if x = xi−1 , y = xi , and r = ri for some i ∈ {1, . . . , n},
(
J
r (x, y) :=
0 otherwise.
Consider now the gfp-model I := gfpT (J ) of T . By construction, for all pairs
(w0 , D) ∈ N∗R × NTP \ {(w, C)} we have (∀w0 .D)I (x0 ) = 1. Moreover, we know
that (∀w.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) ⇒ (∀w.C)I (x0 ) = 1 and
B I (x0 ) = kATB,C k(w) ⇒ (∀w.C)I (x0 ) = (∀w.C)I (x0 ).
Thus AI (x0 ) ⇒ B I (x0 ) = (∀w.C)I (x0 ) < p, and T 6|=gfp hA v B ≥ pi.
Conversely, assume that there are a primitive interpretation J = (∆, ·J ) and
an element x ∈ ∆ such that AI (x) ⇒ B I (x) < p, where I := gfpT (J ). Thus, we
have p ∧ AI (x) > B I (x), which implies by Lemma 13 the existence of a C ∈ NTP
and a w ∈ N∗R with p ∧ AI (x) > kATB,C k(w) ⇒ (∀w.C)I (x). Again by Lemma 13,
this implies that
p ∧ kATB,C k(w) > AI (x) ⇒ (∀w.C)I (x)
≥ kATA,C k(w) ⇒ (∀w.C)I (x) ⇒ (∀w.C)I (x).
In particular, the latter value cannot be 1, and thus it is equal to (∀w.C)I (x).
But this can only be the case if kATA,C k(w) ≤ (∀w.C)I (x). To summarize, we
obtain p ∧ kATB,C k(w) > (∀w.C)I (x) ≥ kATA,C k(w), as desired. t
u
Denote by VT := {0, 1} ∪ {p ∈ [0, 1] | hA v ∀w.B ≥ pi ∈ T } the set of
all values appearing in T , together with 0 and 1. Since wtT has nite sup-
port 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 su ces 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.
De nition 15 (automata A≥p ). Given a WWA A = (Σ, Q, q0 , wt, qf ) and a
value p ∈ [0, 1], the WA A≥p = (Σ, Q, q0 , wt≥p , qf ) is given by the transition
relation wt≥p := {(q, w, q0 ) ∈ Q × Σ ∗ × Q | wt(q, w, q0 ) ≥ p}.
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 ∈ [0, 1]. Then we have
L(A≥p ) = {w ∈ Σ ∗ | kAk(w) ≥ p}.
Proof. We have w ∈ L(A≥p ) i there is a nite path π = q0 w1 q1 . . . wn qn in A
with label w such that wt(qi−1 , wi , qi ) ≥ p holds for all i ∈ {1, . . . , n}. The latter
condition is equivalent to the fact that wt(π) ≥ p. Thus, w ∈ 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 π ∈ paths(A, w) with wt(π) ≥ p, and thus w ∈ L(A≥p ). t u
We thus obtain the following characterization of gfp-subsumption.
Lemma 17. Let A, B ∈ NTC and p ∈ VT . Then T |=gfp hA v B ≥ pi i for all
C ∈ NTP and p0 ∈ VT with p0 ≤ p it holds that L((ATB,C )≥p ) ⊆ L((ATA,C )≥p ).
0 0
Proof. Assume that we have T |=gfp hA v B ≥ pi and consider any C ∈ NTP ,
w ∈ N∗R , and p0 ∈ VT ∩ [0, p] with w ∈ L((ATB,C )≥p0 ). By Lemma 16, we obtain
kATB,C k(w) ≥ p0 , and by Lemma 14 we have kATA,C k(w) ≥ p ∧ kATB,C k(w) ≥ p0 .
Thus, w ∈ L((ATA,C )≥p0 ).
Conversely, assume that T |=gfp hA v B ≥ pi does not hold. Then by
Lemma 14 there are C ∈ NTP and w ∈ N∗R such that p∧kATB,C k(w) > kATA,C k(w).
For the value p0 := p ∧ kATB,C k(w) ∈ VT ∩ [0, p], we have kATB,C k(w) ≥ p0 , but
kATA,C k(w) < p0 , and thus L((ATB,C )≥p0 ) * L((ATA,C )≥p0 ) by Lemma 16. t
u
A direct consequence of this lemma is that gfp-subsumption between concept
names in G-FL0 remains in the same complexity class as for classical FL0 .
Theorem 18. Deciding gfp-subsumption between concept names in G-FL0 is
PSpace-complete.
Proof. By the reductions above, it su ces to decide the language inclusions
L((ATB,C )≥p ) ⊆ L((ATA,C )≥p ) for all C ∈ NTP and p ∈ VT . These polynomially
many inclusion tests for WA can be done in polynomial space [10]. The problem is
PSpace-hard since gfp-subsumption in classical FL0 is already PSpace-hard [1].
This is a special case of our problem where the input TBox is restricted to the
values 0 and 1, and therefore all relevant WWA are already WA. t
u
5 Conclusions
We have studied the complexity of reasoning in G-FL0 w.r.t. primitive concept
de nitions 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 de-
scription logics with Gödel semantics. Indeed, such extensions of EL [15,16] and
ALC [5] have been shown to preserve the complexity of their classical counter-
part. Since reasoning in classical FL0 and in G-ALC w.r.t. general TBoxes is
in both cases ExpTime-complete, so is deciding subsumption in G-FL0 w.r.t.
general TBoxes.
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 [7,19]. Studying
these two cases in detail is a task for future work. We also plan to consider fuzzy
extensions of FL0 with semantics based on non-idempotent t-norms, such as the
ukasiewicz or product t-norms [12].
References
1. Baader, F.: Using automata theory for characterizing the semantics of terminolog-
ical cycles. Ann. Math. Artif. Intell. 18(2), 175219 (1996)
2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applica-
tions. Cambridge University Press, 2nd edn. (2007)
3. Baader, F., Peñaloza, R.: On the undecidability of fuzzy description logics with
GCIs and product t-norm. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Proc.
FroCoS'11, LNCS, vol. 6989, pp. 5570. Springer (2011)
4. Bobillo, F., Straccia, U.: Fuzzy description logics with general t-norms and
datatypes. Fuzzy Set. Syst. 160(23), 33823402 (2009)
5. Borgwardt, S., Distel, F., Peñaloza, R.: Decidable Gödel description logics without
the nitely-valued model property. In: Proc. KR'14. AAAI Press (2014), to appear.
6. Borgwardt, S., Peñaloza, R.: Undecidability of fuzzy description logics. In: Brewka,
G., Eiter, T., McIlraith, S.A. (eds.) Proc. KR'12. pp. 232242. AAAI Press (2012)
7. Borgwardt, S., Peñaloza, R.: The complexity of lattice-based fuzzy description
logics. J. Data Semant. 2(1), 119 (2013)
8. Cerami, M., Straccia, U.: On the (un)decidability of fuzzy description logics under
ukasiewicz t-norm. Inform. Sciences 227, 121 (2013)
9. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic,
Studies in Logic, vol. 3738. College Publications (2011)
10. Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory
of NP-Completeness. W. H. Freeman & Co., New York (1979)
11. Grätzer, G.: General Lattice Theory. Birkhäuser Verlag, 2nd edn. (2003)
12. Hájek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer (2001)
13. Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1952)
14. Klement, E.P., Mesiar, R., Pap, E.: Triangular Norms. Trends in Logic, Studia
Logica Library, Springer (2000)
15. Mailis, T., Stoilos, G., Simou, N., Stamou, G.B., Kollias, S.: Tractable reasoning
with vague knowledge using fuzzy EL++ . J. Intell. Inf. Syst. 39(2), 399440 (2012)
16. Stoilos, G., Stamou, G.B., Pan, J.Z.: Classifying fuzzy subsumption in fuzzy-EL+.
In: Baader, F., Lutz, C., Motik, B. (eds.) Proc. DL'08. CEUR-WS, vol. 353 (2008)
17. Stoilos, G., Straccia, U., Stamou, G.B., Pan, J.Z.: General concept inclusions in
fuzzy description logics. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P.
(eds.) Proc. ECAI'06. pp. 457461. IOS Press (2006)
18. Straccia, U.: Reasoning within fuzzy description logics. J. Artif. Intell. Res. 14,
137166 (2001)
19. Straccia, U.: Description logics over lattices. Int. J. Uncertain. Fuzz. 14(1), 116
(2006)
20. Tarski, A.: A lattice-theoretical xpoint theorem and its applications. Pac. J. Math.
5(2), 285309 (1955)