=Paper=
{{Paper
|id=None
|storemode=property
|title=Gödel Negation Makes Unwitnessed Consistency Crisp
|pdfUrl=https://ceur-ws.org/Vol-846/paper_13.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/BorgwardtDP12
}}
==Gödel Negation Makes Unwitnessed Consistency Crisp==
https://ceur-ws.org/Vol-846/paper_13.pdf
Gödel Negation Makes
Unwitnessed Consistency Crisp?
Stefan Borgwardt, Felix Distel, and Rafael Peñaloza
Faculty of Computer Science
TU Dresden, Dresden, Germany
[stefborg,felix,penaloza]@tcs.inf.tu-dresden.de
Abstract. Ontology consistency has been shown to be undecidable for
a wide variety of fairly inexpressive fuzzy Description Logics (DLs). In
particular, for any t-norm “starting with” the Lukasiewicz t-norm, con-
sistency of crisp ontologies (w.r.t. witnessed models) is undecidable in
any fuzzy DL with conjunction, existential restrictions, and (residual)
negation. In this paper we show that for any t-norm with Gödel negation,
that is, any t-norm not starting with Lukasiewicz, ontology consistency
for a variant of fuzzy SHOI is linearly reducible to crisp reasoning, and
hence decidable in exponential time. Our results hold even if reasoning
is not restricted to the class of witnessed models only.
1 Introduction
Fuzzy Description Logics (DLs) were introduced over a decade ago to represent
and reason with vague or imprecise knowledge. Since their introduction, several
variants of these logics have been studied; in fact, in addition to the constructors
and kinds of axioms used, fuzzy DLs have an additional degree of liberty in the
choice of the t-norm that specifies the semantics. An extensive, although slightly
outdated survey of the area can be found in [18].
Very recently, it was shown that some fuzzy DLs lose the finite model property
in the presence of GCIs [3]. This eventually led to a series of undecidability
results [1, 2, 12, 10]. Most notably, for t-norms that “start with” the Lukasiewicz
t-norm, consistency of crisp ontologies becomes undecidable for the inexpressive
fuzzy DL ⊗-NEL, which allows only the constructors conjunction, existential
restrictions and (residual) negation [10].
So far, the only known decidability results for fuzzy DLs rely on a restriction
of the expressivity: either by allowing only finitely-valued semantics [6, 8], by
limiting the terminological knowledge to be acyclic or unfoldable [14, 11, 5], or
by using the very simple Gödel semantics [4, 21–23]. Moreover, with very few
exceptions [6, 8], reasoning is usually restricted to the class of witnessed mod-
els.1 In fact, witnessed models were introduced in [14] to correct the previous
algorithms for fuzzy DL reasoning.
?
Partially supported by the DFG under grant BA 1122/17-1 and in the Collaborative
Research Center 912 “Highly Adaptive Energy-Efficient Computing”.
1
All fuzzy logics with finitely-valued semantics have the witnessed model property.
Table 1. The three fundamental continuous t-norms
Name t-norm (x ⊗ y) t-conorm (x ⊕ y) residuum
( (x ⇒ y)
1 if x ≤ y
Gödel min{x, y} max{x, y}
y otherwise
(
1 if x ≤ y
product x·y x+y−x·y
y/x otherwise
Lukasiewicz max{x + y − 1, 0} min{x + y, 1} min{1 − x + y, 1}
In this paper we show that for any t-norm with Gödel negation, ontology
consistency is decidable in the very expressive fuzzy DL ⊗-SHOI −∀ , which is the
sub-logic of ⊗-SHOI where value restrictions ∀ are not allowed. For these logics,
ontology consistency w.r.t. general models is linearly reducible to consistency of
a crisp SHOI ontology, and hence decidable in exponential time. In particular,
this holds for the product t-norm. We emphasize that our proofs do not depend
on the models being witnessed or not, hence decidability is shown for reasoning
w.r.t. both, general models and witnessed models.
Since a t-norm has Gödel negation iff it does not start with the Lukasiewicz
t-norm [17], this yields a full characterization of the decidability of ontology
consistency (w.r.t. witnessed models) for all fuzzy DLs between ⊗-NEL and
⊗-SHOI −∀ . We also provide the first decidability results w.r.t. general models
for infinitely-valued, non-idempotent fuzzy DLs.
2 T-norms without Zero Divisors
Mathematical fuzzy logic [13] generalizes classical logic by allowing all the real
numbers from the interval [0, 1] as truth values. The interpretation of the differ-
ent logical constructors depends on the choice of a triangular norm (t-norm for
short). A t-norm is an associative, commutative, and monotone binary operator
on [0, 1] that has 1 as its unit element. The dual operator of a t-norm ⊗ is the
t-conorm ⊕ defined as x ⊕ y = 1 − ((1 − x) ⊗ (1 − y)). Notice that 0 is the unit
of the t-conorm, and hence
x ⊕ y = 0 iff x = 0 and y = 0. (1)
Every continuous t-norm ⊗ defines a unique residuum ⇒ such that x ⊗ y ≤ z
iff y ≤ x ⇒ z for all x, y, z ∈ [0, 1]. It is easy to see that for all x, y ∈ [0, 1]
– x ⇒ y = sup{z ∈ [0, 1] | x ⊗ z ≤ y},
– 1 ⇒ x = x, and
– x ≤ y iff x ⇒ y = 1.
Based on the residuum, one can define the unary precomplement x = x ⇒ 0.
Three important continuous t-norms are the Gödel, product and Lukasiewicz
t-norms shown in Table 1, together with their t-conorms and residua. These are
fundamental in the sense that every continuous t-norm can be described as an
ordinal sum of copies of these t-norms [20].
In this paper, we are interested in t-norms that do not have zero divisors. An
element x ∈ (0, 1) is called a zero divisor for ⊗ if there is a z ∈ (0, 1) such that
x ⊗ z = 0. Of the three fundamental continuous t-norms, only the Lukasiewicz
t-norm has zero divisors. In fact, every element of the interval (0, 1) is a zero
divisor for this t-norm. The Gödel and product t-norms are just two elements of
the uncountable class of continuous t-norms without zero divisors.
Proposition 1. For any t-norm ⊗ without zero divisors and every x ∈ [0, 1],
1. x ⇒ y = 0 iff x > 0 and y = 0, and
2. x = 0 iff x > 0.
Proof. For the first claim, we prove only the if direction, since the other direction
is known to hold for every t-norm [17]. Assume that x > 0 and y = 0. Then
x ⇒ y = x ⇒ 0 = sup{z | z ⊗ x = 0}. Since ⊗ has no zero divisors, z ⊗ x > 0
for all z > 0. Therefore {z | z ⊗ x = 0} = {0} and thus x ⇒ y = 0. The second
statement follows from the first one since x = x ⇒ 0. t
u
In particular, this implies that if the t-norm ⊗ does not have zero divisors, then
its precomplement is the so-called Gödel negation, i.e. for every x ∈ [0, 1],
(
0 if x > 0
x=
1 otherwise.
It can be shown that the converse also holds: if the precomplement is the Gödel
negation, then the t-norm has no zero divisors.
We now define the function 1 that maps fuzzy truth values to crisp truth
values by setting, for all x ∈ [0, 1],
(
1 if x > 0
1(x) =
0 if x = 0.
For a t-norm without zero divisors it follows from Proposition 1 that 1(x) = x
for all x ∈ [0, 1]. This function is compatible with negation, the t-norm, the
corresponding t-conorm, implication and suprema.
Lemma 2. Let ⊗ be a t-norm without zero divisors. For all x, y ∈ [0, 1] and all
non-empty sets X ⊆ [0, 1] it holds that
1. 1( x) = 1(x),
2. 1(x ⊗ y) = 1(x) ⊗ 1(y),
3. 1(x ⊕ y) = 1(x) ⊕ 1(y),
4. 1(x ⇒ y) = 1(x) ⇒ 1(y), and
5. 1 (sup{x | x ∈ X}) = sup{1(x) | x ∈ X}.
Proof. It holds that 1( x) = x = 1(x) which proves 1. Since ⊗ does not
have zero divisors, x ⊗ y = 0 iff x = 0 or y = 0. This shows that
1(x ⊗ y) = 0 iff 1(x) ⊗ 1(y) = 0. (2)
Both 1(x ⊗ y) and 1(x) ⊗ 1(y) can only have the values 0 or 1. Hence, (2)
proves the second statement. Following similar arguments we obtain from (1)
that 1(x ⊕ y) = 0 holds iff 1(x) ⊕ 1(y) = 0, thus proving 3. We use Proposition 1
to prove 4:
( (
1 iff x = 0 or y > 0 1 iff 1(x) = 0 or 1(y) = 1
1(x ⇒ y) = =
0 iff x > 0 and y = 0 0 iff 1(x) = 1 and 1(y) = 0
= 1(x) ⇒ 1(y).
To prove 5, observe that sup X = 0 iff X = {0}. Thus,
1 sup X = 0 ⇔ sup X = 0 ⇔ X = {0}
⇔ {1(x) | x ∈ X} = {0} ⇔ sup{1(x) | x ∈ X} = 0.
t
u
Notice that in general 1 is not compatible with the infimum. Consider for
example the set X = { n1 | n ∈ N}. Then inf X = 0 and hence 1(inf X) = 0, but
inf{1( n1 ) | n ∈ N} = inf{1} = 1.
3 The Fuzzy DL ⊗-SHOI −∀
A fuzzy description logic usually inherits its syntax from the underlying crisp
description logic. We consider the constructors of SHOI with the addition of
→, which in the crisp case can be expressed by t and ¬.
Definition 3 (syntax). Let NC , NR , and NI , be disjoint sets of concept, role,
and individual names, respectively, and N+ R ⊆ NR be a set of transitive role
names. The set of (complex) roles is NR ∪ {r− | r ∈ NR }. ⊗-SHOI (complex)
concepts are constructed by the following syntax rule:
C ::= A | > | ⊥ | {a} | ¬C | C u C | C t C | C → C | ∃s.C | ∀s.C,
where A is a concept name, a is an individual name, and s is a complex role.
The inverse of a complex role s (denoted by s) is s− if s ∈ NR and r if s = r− .
A role s is transitive if either s or s belongs to N+
R.
Given a continuous t-norm ⊗, concepts in the fuzzy DL ⊗-SHOI are inter-
preted by functions specifying the membership degree of each domain element
to the concept. The interpretation of the constructors is based on the t-norm ⊗
and the induced operators ⊕, ⇒, and .
Definition 4 (semantics). An interpretation is a pair I = (∆I , ·I ), where the
domain ∆I is a non-empty set and ·I is a function that assigns to every concept
name A a function AI : ∆I → [0, 1], to every individual name a an element
aI ∈ ∆I , and to every role name r a function rI : ∆I × ∆I → [0, 1] such that
rI (x, y) ⊗ rI (y, z) ≤ rI (x, z) holds for all x, y, z ∈ ∆I if r ∈ N+
R . The function
·I is extended to complex roles and concepts as follows for every x, y ∈ ∆I ,
– (r− )I (x, y) = rI (y, x),
– >I (x) = 1, ⊥I (x) = 0,
– {a}I (x) = 1 if aI = x and 0 otherwise,
– (¬C)I (x) = C I (x),
– (C1 u C2 )I (x) = C1I (x) ⊗ C2I (x), (C1 t C2 )I (x) = C1I (x) ⊕ C2I (x),
– (C1 → C2 )I (x) = C1I (x) ⇒ C2I (x),
– (∃s.C)I (x) = supz∈∆I sI (x, z) ⊗ C I (z), and
– (∀s.C)I (x) = inf z∈∆I sI (x, z) ⇒ C I (z).
I is finite if its domain ∆I is finite, and crisp if AI (x), rI (x, y) ∈ {0, 1} for all
A ∈ NC , r ∈ NR , and x, y ∈ ∆I .
Recall from the previous section that ¬ is interpreted by the Gödel negation iff
the t-norm ⊗ does not have zero divisors. In particular, (¬C)I (x) ∈ {0, 1} holds
for every concept C, interpretation I, and x ∈ ∆I , i.e. the value of ¬C is always
crisp.
Knowledge is encoded using axioms, which restrict the class of interpretations
that are considered and specify a degree to which the restrictions should hold.
Definition 5 (axioms). A ⊗-SHOI-axiom is either an assertion of the form
ha :C, `i or h(a, b) : s, `i, a GCI of the form hC v D, `i, or a role inclusion of
the form hs v t, `i, where C and D are ⊗-SHOI-concepts, a, b ∈ NI , s, t are
complex roles, and ` ∈ (0, 1]. An axiom is called crisp if ` = 1.
An interpretation I satisfies an assertion ha: C, `i if C I (aI ) ≥ ` and an
assertion h(a, b) :s, `i if sI (aI , bI ) ≥ `. It satisfies the GCI hC v D, `i if
C I (x) ⇒ DI (x) ≥ ` holds for all x ∈ ∆I . It satisfies a role inclusion hs v t, `i
if sI (x, y) ⇒ tI (x, y) ≥ ` holds for all x, y ∈ ∆I .
A ⊗-SHOI-ontology (A, T , R) is defined by a finite set A of assertions
(ABox), a finite set T of GCIs (TBox), and a finite set R of role inclusions
(RBox). It is crisp if every axiom in A, T , and R is crisp. An interpretation I
is a model of this ontology if it satisfies all its axioms.
We consider also the logic ⊗-SHOI −∀ , which restricts ⊗-SHOI by disallow-
ing the constructor ∀. ⊗-SHOI −∀ -concepts, axioms and ontologies are defined
in the obvious way. Notice that, contrary to the crisp case, value- and existential-
restrictions are not dual. In fact, we will show in Section 4 that for every t-norm
⊗ without zero divisors ⊗-SHOI is strictly more expressive than ⊗-SHOI −∀ .
Several reasoning problems are of interest in the area of fuzzy DLs. Here
we focus only on deciding whether a ⊗-SHOI (or ⊗-SHOI −∀ ) ontology is
consistent; that is, whether it has a model. We will show that, if the t-norm
⊗ has no zero divisors, then consistency in ⊗-SHOI −∀ is effectively the same
problem as consistency in crisp SHOI. Moreover, the precise values appearing
in the axioms in the ontology are then irrelevant. The same is not true, however,
for consistency in ⊗-SHOI.
Recall that the semantics of the quantifiers require the computation of a
supremum or infimum of the membership degrees of a possibly infinite set of
elements of the domain. In the fuzzy DL community it is customary to restrict
reasoning to a special kind of models, called witnessed models [14].
Definition 6 (witnessed). An interpretation I is called witnessed if for every
x ∈ ∆I , every role s and every concept C there are y1 , y2 ∈ ∆I such that
(∃s.C)I (x) = sI (x, y1 ) ⊗ C I (y1 ), (∀s.C)I (x) = sI (x, y2 ) ⇒ C I (y2 ).
In particular, if an interpretation I is crisp or finite, then it is also witnessed.
Witnessed models were introduced to simplify the reasoning tasks. In fact, al-
though this concept was only formalized in [14], the earlier reasoning algorithms
for fuzzy DLs semantics based on the Gödel t-norm (e.g. [23]) implicitly used
only witnessed models. We show that consistency of ⊗-SHOI −∀ -ontologies can
be decided in exponential time, without restricting to witnessed models.
4 The Crisp Model Property
The existing undecidability results for fuzzy DLs all rely heavily on the fact
that one can design ontologies that allow only models with infinitely many truth
values. We shall see that for t-norms without zero divisors one cannot construct
such an ontology in ⊗-SHOI −∀ . It is even true that all consistent ⊗-SHOI −∀ -
ontologies have a crisp model; that is, using at most two truth values.
Definition 7. A fuzzy DL L has the crisp model property if every consistent
L-ontology has a crisp model.
For the rest of this paper we assume that ⊗ is a continuous t-norm that does
not have zero divisors, and hence has the properties described in Section 2. In
particular, Lemma 2 allows us to construct a crisp interpretation from a fuzzy
interpretation by simply applying the function 1.
Let I be a fuzzy interpretation for the concept names NC and role names
NR . We construct the interpretation J = (∆J , ·J ), where ∆J := ∆I and for all
concept names A ∈ NC , all role names r ∈ NR , and all x, y ∈ ∆I ,
AJ (x) := 1 AI (x) and rJ (x, y) := 1 rI (x, y) .
To show that J is a valid interpretation, we first verify the transitivity condition
for all r ∈ N+ J
R and all x, y, z ∈ ∆ . From Lemma 2, we obtain
rJ (x, y) ⊗ rJ (y, z) = 1 rI (x, y) ⊗ 1 rI (y, z) = 1 rI (x, y) ⊗ rI (y, z) .
Since I satisfies the transitivity condition and 1 is monotonic, we have
1 rI (x, y) ⊗ rI (y, z) ≤ 1 rI (x, z) = rJ (x, z),
and thus rJ (x, y) ⊗ rJ (y, z) ≤ rJ (x, z).
Lemma 8. For all complex roles s and x, y ∈ ∆I , sJ (x, y) = 1(sI (x, y)).
Proof. If s is a role name, this follows directly from the definition of J . If s = r−
for some r ∈ NR , then sJ (x, y) = rJ (y, x) = 1(rI (y, x)) = 1(sI (x, y)). t
u
The interpretation J preserves the compatibility of 1 with all the construc-
tors of ⊗-SHOI −∀ .
Lemma 9. For every ⊗-SHOI −∀ -concept C and x ∈ ∆I , C J (x) = 1 C I (x) .
Proof. We use induction over the structure of C. The claim holds trivially for
C = ⊥ and C = >. For C = A ∈ NC it follows immediately from the definition
of J . It also holds for C = {a}, a ∈ NI , because {a}I (x) can only take the values
0 or 1 for all x ∈ ∆I .
Assume now that the concepts D and E satisfy DJ (x) = 1(DI (x)) and
E (x) = 1(E I (x)) for all x ∈ ∆I . In the case where C = D u E, Lemma 2
J
yields that for all x ∈ ∆I
C J (x) = DJ (x) ⊗ E J (x) = 1 DI (x) ⊗ 1 E I (x)
= 1 DI (x) ⊗ E I (x) = 1 C I (x) .
Likewise, the compatibility of 1 with the t-conorm, the residuum, and the nega-
tion entails the result for the cases C = D t E, C = D → E, and C = ¬D.
For C = ∃s.D, where s is a complex role and D is a concept description
satisfying DJ (x) = 1(DI (x)) for all x ∈ ∆I , we obtain
1 C I (x) = 1 (∃s.D)I (x) = 1 sup sI (x, y) ⊗ DI (y)
y∈∆I
1 sI (x, y) ⊗ 1 DI (y)
= sup (3)
y∈∆I
because 1 is compatible with the supremum and the t-norm. Lemma 8 yields
sup 1(rI (x, y)) ⊗ 1(DI (y)) = sup rJ (x, y) ⊗ DJ (y) = (∃r.D)J (x). (4)
y∈∆I y∈∆I
Equations (3) and (4) prove 1(C I (x)) = C J (x) for C = ∃r.D. t
u
We can use this lemma to show that the crisp interpretation J satisfies all
the axioms that are satisfied by I.
Lemma 10. Let O = (A, T , R) be a ⊗-SHOI −∀ -ontology. If I is a model of
O, then J is also a model of O.
Proof. We prove that J satisfies all assertions, GCIs, and role inclusions from
O. Let ha :C, `i, ` ∈ (0, 1], be a concept assertion from A. Since the assertion
is satisfied by I, C I (aI ) ≥ ` > 0 holds. Lemma 9 yields C J (aJ ) = 1 ≥ `. The
same argument can be used for role assertions.
Let now hC v D, `i be a GCI in T and x ∈ ∆I . Since I satisfies the GCI,
we get C I (x) ⇒ DI (x) ≥ ` > 0. By Lemmata 2 and 9, we obtain
C J (x) ⇒ DJ (x) = 1(C I (x)) ⇒ 1(DI (x)) = 1(C I (x) ⇒ DI (x)) = 1 ≥ `,
and thus J satisfies the GCI hC v D, `i. A similar argument, using Lemma 8
instead of Lemma 9, shows that J satisfies all role inclusions in R. t
u
The previous results show that by applying 1 to the truth degrees we obtain
a crisp model J from any fuzzy model I of a ⊗-SHOI −∀ -ontology O.
Theorem 11. If ⊗ is a t-norm without zero divisors, then ⊗-SHOI −∀ has the
crisp model property.
A trivial consequence of this theorem is that every consistent ⊗-SHOI −∀ -
ontology has also a witnessed model, since every crisp model is also crisp.
Corollary 12. If ⊗ is a t-norm without zero divisors, then ⊗-SHOI −∀ has the
witnessed model property.
In the next section we will use this result from Theorem 11 to show that
⊗-SHOI −∀ ontology consistency can be decided in exponential time, by testing
consistency of a (crisp) SHOI ontology. But first, we show that value restrictions
destroy the crisp model property, even if only crisp axioms are used.
Example 13. Consider the ⊗-SHOI-ontology
O = {h> v ¬¬A, 1i, ha :¬∀r.A, 1i}.
The interpretation I = (∆I , ·I ) with ∆I = N (the set of all natural numbers),
aI = 1, AI (n) = 1/(n + 1), rI (1, n) = 1, and rI (n0 , n) = 0 for all n, n0 ∈ N with
n0 > 1 is a model of O, and hence O is consistent.
Let now J be a crisp interpretation satisfying the first axiom in O. Then,
AJ (x) = 1 for all x ∈ ∆J . This implies that
(∀r.A)J (aJ ) = inf rJ (aJ , y) ⇒ AJ (y)
y∈∆J
= inf rJ (aJ , y) ⇒ 1
y∈∆J
= 1.
And thus, (¬∀r.A)J (aJ ) = 0, violating the second axiom. This means that O
has no crisp model.
The example shows that no fuzzy DL with the constructor ∀ and Gödel
negation2 has the crisp model property. A similar example in [14] demonstrates
that no fuzzy DL with the constructors ∃ and ∀ and Gödel negation has the
witnessed model property.
Theorem 14. For any continuous t-norm ⊗ and any fuzzy DL ⊗-L having the
constructors >, ¬, and ∀, ⊗-L does not have the crisp model property.
In particular, this means that ⊗-SHOI does not have the crisp model prop-
erty and is strictly more expressive than ⊗-SHOI −∀ .
Corollary 15. If ⊗ is a t-norm without zero divisors, then ⊗-SHOI is strictly
more expressive than ⊗-SHOI −∀ .
5 Deciding Consistency
For a given ⊗-SHOI −∀ -ontology O, we define crisp(O) to be the crisp SHOI-
ontology that is obtained from O by replacing all the truth values appearing in
the axioms by 1. For example, for the ontology
O = ha :C, 0.2i, h(a, b) : r, 0.8i, hC v D, 0.5i, hr v s, 0.1i
we obtain
crisp(O) = ha : C, 1i, h(a, b) :r, 1i, hC v D, 1i, hr v s, 1i .
Lemma 16. Let O be a ⊗-SHOI −∀ -ontology and I be a crisp interpretation.
Then I is a model of O iff it is a model of crisp(O).
Proof. Assume that crisp(O) has a model I. Let hC v D, `i, ` > 0, be an axiom
from O. Since I is a model of crisp(O), it must satisfy hC v D, 1i; that is,
C I (x) ⇒ DI (x) ≥ 1 ≥ ` holds for all x ∈ ∆I . Thus I satisfies hC v D, `i. The
proof that I satisfies assertions and role inclusions is analogous. Hence I is also
a model of O.
For the other direction, assume that I satisfies hC v D, `i with ` > 0. As I
is a crisp interpretation it holds that C I (x) ⇒ DI (x) ∈ {0, 1} for all x ∈ ∆I .
Together with C I (x) ⇒ DI (x) ≥ ` > 0 we obtain C I (x) ⇒ DI (x) = 1. Thus, I
satisfies the GCI hC v D, 1i. The same argument can be used for role inclusions
and assertions. Thus, I is also a model of crisp(O). t
u
In particular, a ⊗-SHOI −∀ -ontology O has a crisp model iff crisp(O) has a
crisp model. Together with Theorem 11, this shows that a ⊗-SHOI −∀ -ontology
O is consistent iff crisp(O) has a crisp model. Therefore, one can use any reason-
ing procedure for crisp SHOI to decide consistency of ⊗-SHOI −∀ -ontologies.
Reasoning in crisp SHOI is known to be ExpTime-complete [15]. Recall that
under crisp semantics, value restrictions can be expressed by negation and exis-
tential restrictions, and hence, crisp SHOI is equivalent to crisp SHOI −∀ .
2
Recall that a fuzzy DL has Gödel negation iff its semantics is based on a t-norm
without zero divisors.
Corollary 17. Deciding consistency in ⊗-SHOI −∀ is ExpTime-complete.
Lemma 16 and Theorem 11 still hold when we restrict the semantics to the
slightly less expressive logics ⊗-SHO−∀ , which does not allow for inverse roles,
or ⊗-SI −∀ which does not allow for nominals and role hierarchies. The crisp DLs
SHO and SI are known to have the finite model property [16, 19], and ⊗-SI −∀
and ⊗-SHO−∀ inherit the finite model property from their crisp counterparts.
Theorem 18. The logics ⊗-SHO−∀ and ⊗-SI −∀ and their sublogics have the
finite model property.
6 Conclusions
In this paper we have described a family of expressive fuzzy DLs for which
ontology consistency is decidable. More precisely, we have shown that if ⊗ is a
t-norm without zero divisors, consistency of ⊗-SHOI −∀ ontologies is ExpTime-
complete, and hence as hard as consistency of (crisp) SHOI ontologies. Our
construction shows that the fuzzy values appearing in ⊗-SHOI −∀ ontologies
are irrelevant for consistency: a ⊗-SHOI −∀ ontology O has a (fuzzy) model iff
its crisp variant crisp(O), where the degrees of all the axioms in O are changed to
1, has a crisp model. This implies that ⊗-SHOI −∀ has the crisp model property,
and hence also the witnessed model property. If the constructor ∀ is also allowed,
hence obtaining the logic ⊗-SHOI, then these properties do not hold anymore.
For other reasoning problems such as entailment and subsumption it is un-
known whether they are decidable in ⊗-SHOI −∀ . In [7] it is shown for ⊗-SHOI
with witnessed models that subsumption and entailment, as well as computing
the best subsumption and entailment degrees, cannot be reduced to crisp rea-
soning by simply mapping all nonzero truth degrees to 1. We conjecture that
this is also the case in ⊗-SHOI −∀ .
It has recently been shown that if the t-norm ⊗ has zero divisors, then
consistency of crisp ontologies in the very inexpressive fuzzy DL ⊗-NEL w.r.t.
witnessed models [10] and w.r.t. general models [9] is undecidable.3 Combining
these results, we obtain a characterization of the decidability of consistency w.r.t.
witnessed and general models for all fuzzy DLs between ⊗-NEL and ⊗-SHOI −∀ :
it is decidable (in ExpTime) iff ⊗ has no zero divisors.
In future work, we plan to study reasoning problems in fuzzy DLs allowing for
value restrictions without the restriction to witnessed models. In this direction
it is worth looking at the decidability results for ⊗-ALC with product t-norm
w.r.t. quasi-witnessed models [11].
References
1. Baader, F., Peñaloza, R.: Are fuzzy description logics with general concept inclu-
sion axioms decidable? In: Proc. of the 2011 IEEE Int. Conf. on Fuzzy Systems
(FUZZ-IEEE’11). pp. 1735–1742. IEEE Press (2011)
3
⊗-NEL is the sublogic of ⊗-SHOI −∀ that allows only the constructors >, ¬ and ∃.
2. Baader, F., Peñaloza, R.: On the undecidability of fuzzy description logics with
GCIs and product t-norm. In: Proc. of 8th Int. Symp. Frontiers of Combining
Systems (FroCoS’11). pp. 55–70. Springer-Verlag (2011)
3. Bobillo, F., Bou, F., Straccia, U.: On the failure of the finite model property in
some fuzzy description logics. Fuzzy Sets and Systems 172(23), 1–12 (2011)
4. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Fuzzy description logics
under Gödel semantics. Int. J. of Approx. Reasoning 50(3), 494–514 (2009)
5. Bobillo, F., Straccia, U.: Fuzzy description logics with general t-norms and
datatypes. Fuzzy Sets and Systems 160(23), 3382–3402 (2009)
6. Bobillo, F., Straccia, U.: Reasoning with the finitely many-valued Lukasiewicz fuzzy
description logic SROIQ. Information Sciences 181, 758–778 (2011)
7. Borgwardt, S., Distel, F., Peñaloza, R.: How fuzzy is my fuzzy description logic?
In: Proc. of the 6th Int. Joint Conf. on Autom. Reas. (IJCAR’12) (2012), to appear
8. Borgwardt, S., Peñaloza, R.: Description logics over lattices with multi-valued on-
tologies. In: Proc. of the 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11).
pp. 768–773. AAAI Press (2011)
9. Borgwardt, S., Peñaloza, R.: Non-Gödel negation makes unwitnessed consistency
undecidable. In: Proc. of the 25th Int. Workshop on Description Logics (DL 2012).
CEUR Workshop Proceedings, Rome, Italy (2012), to appear
10. Borgwardt, S., Peñaloza, R.: Undecidability of fuzzy description logics. In: Proc.
of the 13th Int. Conf. on Principles of Knowledge Representation and Reasoning
(KR 2012). AAAI Press, Rome, Italy (2012), to appear
11. Cerami, M., Esteva, F., Bou, F.: Decidability of a description logic over infinite-
valued product logic. In: Proc. of the 12th Int. Conf. on Principles of Knowledge
Representation and Reasoning (KR 2010). AAAI Press (2010)
12. Cerami, M., Straccia, U.: On the undecidability of fuzzy description logics with
GCIs with Lukasiewicz t-norm. Tech. rep., Computing Research Repository (2011),
arXiv:1107.4212v3 [cs.LO]. An extended version of this paper has been submit-
ted to a journal.
13. Hájek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer-Verlag
(2001)
14. Hájek, P.: Making fuzzy description logic more general. Fuzzy Sets and Systems
154(1), 1–15 (2005)
15. Hladik, J.: To and Fro Between Tableaus and Automata for Description Logics.
Ph.D. thesis, Dresden University of Technology, Germany (2007)
16. Horrocks, I., Sattler, U., Tobies, S.: A PSpace-algorithm for deciding ALCN I R+ -
satisfiability. LTCS-Report 98-08, RWTH Aachen, Germany (1998)
17. Klement, E.P., Mesiar, R., Pap, E.: Triangular Norms. Springer-Verlag (2000)
18. Lukasiewicz, T., Straccia, U.: Managing uncertainty and vagueness in description
logics for the semantic web. Journal of Web Semantics 6(4), 291–308 (2008)
19. Lutz, C., Areces, C., Horrocks, I., Sattler, U.: Keys, nominals, and concrete do-
mains. Journal of Artificial Intelligence Research 23, 667–726 (2004)
20. Mostert, P.S., Shields, A.L.: On the structure of semigroups on a compact manifold
with boundary. Annals of Mathematics 65, 117–143 (1957)
21. Stoilos, G., Stamou, G.B., Pan, J.Z., Tzouvaras, V., Horrocks, I.: Reasoning with
very expressive fuzzy description logics. JAIR 30, 273–320 (2007)
22. Straccia, U.: Reasoning within fuzzy description logics. Journal of Artificial Intel-
ligence Research 14, 137–166 (2001)
23. Tresp, C.B., Molitor, R.: A description logic for vague knowledge. In: Proc. of the
13th Eur. Conf. on Artificial Intelligence (ECAI’98). pp. 361–365. J. Wiley and
Sons, Brighton, UK (1998)