=Paper=
{{Paper
|id=Vol-1193/paper_4
|storemode=property
|title=Fuzzy DLs over Finite Lattices with Nominals
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_4.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/Borgwardt14
}}
==Fuzzy DLs over Finite Lattices with Nominals==
https://ceur-ws.org/Vol-1193/paper_4.pdf
Fuzzy DLs over Finite Lattices with Nominals?
Stefan Borgwardt
Theoretical Computer Science, TU Dresden, Germany
stefborg@tcs.inf.tu-dresden.de
Abstract. The complexity of reasoning in fuzzy description logics (DLs)
over a finite lattice L usually does not exceed that of the underlying clas-
sical DLs. This has recently been shown for the logics between L-IALC
and L-ISCHI using a combination of automata- and tableau-based tech-
niques. In this paper, this approach is modified to deal with nominals and
constants in L-ISCHOI. Reasoning w.r.t. general TBoxes is ExpTime-
complete, and PSpace-completeness is shown under the restriction to
acyclic terminologies in two sublogics. The latter implies two previously
unknown complexity results for the classical DLs ALCHO and SO.
1 Introduction
Fuzzy extensions of DLs have first been studied in [28,32,34] to model concepts
that do not have a precise meaning. Such concepts occur in many application
domains. For example, a physician may base a diagnosis on the patient having
a high fever, which is not clearly characterized even by the precise body tem-
perature. The main idea behind fuzzy DLs is that concepts are not interpreted
as sets, but rather as fuzzy sets, which assign a membership degree from [0, 1] to
each domain element. As a fuzzy concept, HighFever could assign degree 0.7 to a
patient with a body temperature of 38 ◦ C, and 0.9 when the body temperature
is 39 ◦ C.
The first fuzzy DLs were based on the so-called Zadeh semantics that is de-
rived from fuzzy set theory [35]. Later, it was proposed [19] to consider fuzzy DLs
from the point of view of Mathematical Fuzzy Logic [18] and t-norm-based se-
mantics were introduced. A t-norm is a binary operator on [0, 1] that determines
how the conjunction of two fuzzy statements is evaluated. Unfortunately, it was
shown that many t-norm-based fuzzy DLs allowing general TBoxes have unde-
cidable consistency problems [3,12,16]. This can be avoided by either choosing
a t-norm that allows the consistency problem to be trivially reduced to classi-
cal reasoning [10], restricting to acyclic TBoxes [5], or taking the truth values
from a finite structure, usually a total order [7,8,29] or a lattice [11,13,24,30].
Recently, it was shown that the complexity of reasoning in fuzzy DLs over finite
lattices with (generalized) t-norms often matches that of the underlying classical
DLs [13,14].
?
Partially supported by the DFG under grant BA 1122/17-1 and in the research
training group 1763 (QuantLA)
In this paper, we analyze the complexity of fuzzy extensions of SHOI using a
finite lattice L. In the classical case, deciding consistency of ontologies with gen-
eral TBoxes is ExpTime-complete in all logics between ALC and SHOI [20,26],
and we show that this also holds for L-ISCHOI. The additional letters I and C
in the name of the logic denote the presence of the constructors for implication
and involutive negation, respectively. This nomenclature was introduced to make
the subtle differences between different fuzzy DLs more explicit [12,15]. As all
fuzzy DLs considered in this paper have both I and C, it is safe to ignore these
letters here and simply read L-SHOI instead of L-ISCHOI.
Consistency remains ExpTime-complete in the classical DLs ALCOI and SH
even w.r.t. the empty TBox [22,31]. However, when restricting to acyclic (or
empty) TBoxes in SI, it is only PSpace-complete [1,23]. Similar results have
been shown before under finite lattice semantics in L-IALCHI and L-ISCI c [13].
The latter restricts all roles to be crisp, i.e. they are allowed to take only the two
classical truth values. Here, we extend these results to L-IALCHO and L-ISCOc ,
which also shows previously unknown complexity results for the classical DLs
ALCHO and SO with acyclic TBoxes. Due to space constraints, all proofs can
be found only in the accompanying technical report [9].
2 Preliminaries
We first introduce looping automata on infinite trees and several helpful notions
from [1], which will be used later for our reasoning procedures. Afterwards, we
briefly recall relevant definitions from lattice theory [17].
2.1 Looping Automata
We consider automata on the (unlabeled ) infinite tree of fixed arity k ∈ N,
represented by the set K ∗ of its nodes, where K abbreviates {1, . . . k}. Here, ε
represents the root node, and ui, i ∈ K, is the i-th successor of the node u ∈ K ∗ .
A path in this tree is a sequence u1 , . . . , um of nodes such that u1 = ε and, for
every i, 1 ≤ i ≤ m − 1, ui+1 is a successor of ui .
Definition 1 (looping automaton). A looping (tree) automaton is a tuple
A = (Q, I, ∆) where Q is a finite set of states, I ⊆ Q is a set of initial states,
and ∆ ⊆ Qk+1 is the transition relation. A run of A is a mapping r : K ∗ → Q
such that r(ε) ∈ I and (r(u), r(u1), . . . , r(uk)) ∈ ∆ for every u ∈ K ∗ . The
emptiness problem is to decide whether a given looping automaton has a run.
The emptiness problem for such automata is decidable in polynomial time [33].
However, the automata we construct in Section 4 are exponential in the size of
the input. In order to obtain PSpace decision procedures, we need to identify
the length of the longest possible path in a run that does not repeat any states.
Definition 2 (invariant, blocking). Let A = (Q, I, ∆) be a looping automaton
and a binary relation over Q, called the blocking relation. A is -invariant if
(q0 , q1 , . . . , qi , . . . , qk ) ∈ ∆ and qi qi0 always imply (q0 , q1 , . . . , qi0 , . . . , qk ) ∈ ∆.
If this is the case, then A is m-blocking for m ∈ N if in every path u1 , . . . , um of
length m in a run r of A there are two indices 1 ≤ i < j ≤ m with r(uj ) r(ui ).
The notion of blocking is similar to that used in tableau algorithms for DLs [4,23].
If q is blocked by its ancestor q 0 (q q 0 ), then we do not need to consider
the subtree below q since every transition involving q can be replaced by one
using q 0 instead. Of course, every looping automaton is =-invariant and |Q|-
blocking. However, as mentioned above the size of Q may already be exponential
in some external parameter. To obtain m-blocking automata with m bounded
polynomially in the size of the input, we can use a faithful family of functions
to prune the transition relation.
Definition 3 (faithful). Let A = (Q, I, ∆) be a looping automaton. A family
f = (fq )q∈Q of functions fq : Q → Q is called faithful (w.r.t. A) if
– for all (q, q1 , . . . , qk ) ∈ ∆, we have (q, fq (q1 ), . . . , fq (qk )) ∈ ∆, and
– for all (q0 , q1 , . . . , qk ) ∈ ∆, we have (fq (q0 ), fq (q1 ), . . . , fq (qk )) ∈ ∆.
The subautomaton Af := (Q, I, ∆f ) induced by f is defined by
∆f := {(q, fq (q1 ), . . . , fq (qk )) | (q, q1 , . . . , qk ) ∈ ∆}.
The name faithful reflects the fact that the resulting subautomaton simulates all
runs of A. The following connection between the two automata was shown in [1].
Proposition 4. Let A be a looping automaton and f be a faithful family of func-
tions for A. Then A has a run iff Af has a run.
Together with the following additional assumptions, polynomial blocking allows
us to test emptiness in polynomial space.
Definition 5 (PSpace on-the-fly construction). Let I be a set of inputs. A
construction that yields, for each i ∈ I, an mi -blocking looping automaton Ai over
ki -ary trees is called a PSpace on-the-fly construction if there is a polynomial P
such that, for every input i of size n,
(i) mi ≤ P (n) and ki ≤ P (n),
(ii) the size of every state of Ai is bounded by P (n), and
(iii) one can guess in time bounded by P (n) an initial state, and, given a state q,
a transition (q, q1 , . . . , qk ) of Ai .
The following result is again taken from [1].
Proposition 6. If the looping automata Ai are obtained by a PSpace on-the-fly
construction, then emptiness of Ai can be decided in PSpace in the size of i.
2.2 Residuated Lattices
A lattice is an algebraic structure (L, ∨, ∧) with two commutative, associative,
and idempotent binary operators, called supremum (∨) and infimum (∧), that
satisfy x ∧ (x ∨ y) = x and x ∨ (x ∧ y) = x for all x, y ∈ L. The natural partial
order on L is given by x ≤ y iff x ∧ y = x for all x, y ∈ L. An antichain is
a set S ⊆ L of incomparable elements. The width of a lattice is the maximal
cardinality of all its antichains. A lattice L is complete if W suprema andVinfima
of arbitrary subsets S ⊆ L exist; these are denoted by x∈S x and x∈S x,
respectively. It is distributive if ∧ and ∨ distribute over each other, finite if L is
finite, and bounded if it has a least element 0 and a greatest element 1.VEvery
W is complete, and every complete lattice is bounded by 0 := x∈L x
finite lattice
and 1 := x∈L x.
A De Morgan lattice is a distributive lattice L with a unary involutive
operator ∼ on L satisfying the De Morgan laws ∼(x ∨ y) = ∼x ∧ ∼y and
∼(x ∧ y) = ∼x ∨ ∼y for all x, y ∈ L. Such an operator is always antitone
and satisfies ∼0 = 1. A t-norm over a bounded lattice L is a commutative, as-
sociative, monotone binary operator ⊗ on L that has 1 as its unit. A residuated
lattice is a bounded lattice L with a t-norm ⊗ and a residuum ⇒ : L × L → L
satisfying (x ⊗ y) ≤ z iff y ≤ (x ⇒ z) y, z ∈ L. We always assume that
x, W
W for all
⊗ is join-preserving, that is, x ⊗ y∈S y = y∈S (x ⊗ y) holds for all x ∈ L
and S ⊆ L. This is a natural assumption that corresponds to the left-continuity
assumption for t-norms over the standard fuzzy interval [0, 1] [18].
3 L-ISCHOI
Since fuzzy DLs over infinite lattices easily become undecidable when dealing
with GCIs [3,12,14,16], we now fix a finite residuated De Morgan lattice L. For
the complexity analysis, we assume that L is given as a list of its elements and
that all lattice operations are computable in polynomial time.1
The syntax of the fuzzy description logic L-ISCHOI is similar to that of
classical SHOI: complex roles and concepts are constructed from disjoint sets
NC of concept names, NR of role names, and NI of individual names.
Definition 7 (syntax). The set N− R of (complex) roles is {r, r
−
| r ∈ NR }.
The set of (complex) concepts is constructed as follows:
– every concept name is a concept, and
– for concepts C, D, r ∈ N−
R , a ∈ NI , and p ∈ L, the following are also concepts:
p (constant), {a} (nominal), ¬C (negation), C u D (conjunction), C → D
(implication), ∃r.C (existential restriction), and ∀r.C (value restriction).
For a complex role s, the inverse of s (written s) is s− if s ∈ NR and r if s = r− .
1
If instead the size of the input encoding of L is logarithmic in the cardinality of L,
then all complexity results except Theorem 18 remain valid.
Definition 8 (semantics). A (fuzzy) interpretation I = (∆I , ·I ) consists of a
non-empty domain ∆I and an interpretation function ·I that assigns to every
A ∈ NC a fuzzy set AI : ∆I → L, to every r ∈ NR a fuzzy binary relation
rI : ∆I × ∆I → L, and to every a ∈ NI a domain element aI ∈ ∆I . This
function is extended to complex roles and concepts as follows for all x, y ∈ ∆I :
– (r− )I (x, y) := rI (y, x);
– pI (x) := p;
– {a}I (x) := 1 if x = aI , and {a}I (x) := 0 otherwise;
– (¬C)I (x) := ∼C I (x);
– (C u D)I (x) := C I (x) ⊗ DI (x);
– (C → D)I (x) := I I
W C (x) ⇒ D (x);
– (∃r.C)I (x) := y∈∆I rI (x, y) ⊗ C I (y); and
– (∀r.C)I (x) := y∈∆I rI (x, y) ⇒ C I (y).
V
One can express fuzzy nominals [6] of the form {p1 /a1 , . . . , pn /an } with pi ∈ L
and ai ∈ NI , 1 ≤ i ≤ n, by ({a1 }up1 )t· · ·t({an }upn ), where C tD abbreviates
¬(¬C u ¬D). Unlike in classical DLs, existential and value restrictions need not
be dual to each other, i.e. in general we have (¬∃r.C)I 6= (∀r.¬C)I .
Definition 9 (ontology). An axiom α is a concept assertion ha:C ./ pi, a con-
.
cept definition hA = C ≥ pi, a general concept inclusion (GCI) hC v D ≥ pi, a
role inclusion hr v si, or a transitivity axiom trans(r), where C, D are concepts,
r, s ∈ N−R , a ∈ NI , A ∈ NC , p ∈ L, and ./ ∈ {<, ≤, =, ≥, >}. An interpreta-
tion I satisfies α if C I (aI ) ./ p, (AI (x) ⇒ C I (x)) ⊗ (C I (x) ⇒ AI (x)) ≥ p,
C I (x) ⇒ DI (x) ≥ p, rI (x, y) ≤ sI (x, y), or rI (x, y) ⊗ rI (y, z) ≤ rI (x, z),
respectively, hold for all x, y, z ∈ ∆I .
An acyclic TBox is a finite set T of concept definitions where every A ∈ NC
.
has at most one definition hA = C ≥ pi in T and the relation >T on NC is
acyclic, where A >T B iff B occurs in the definition of A. A general TBox is
a finite set of GCIs, an ABox a finite set of concept assertions, and an RBox
a finite set of role inclusions and transitivity axioms. An ontology is a triple
(A, T , R) consisting of an ABox A, an (acyclic or general) TBox T , and an
RBox R. An interpretation is a model of this ontology if it satisfies all its axioms.
We denote by NI (O) and NR (O) the sets of individual names and role names,
respectively, occurring in an ontology O, and set N− −
R (O) := {r, r | r ∈ NR (O)}.
As usual, for an ontology O = (A, T , R) we define the role hierarchy vR as the
reflexive transitive closure of {(r, s) ∈ N−R (O) | r vR s ∈ R or r vR s ∈ R},
and we call a role r transitive if either trans(r) ∈ R or trans(r) ∈ R.
We do not consider role assertions of the form h(a, b):r ./ pi since in the pres-
ence of nominals they can be simulated by concept assertions, e.g. ha:∃r.{b} ./ pi.
The reasoning problem we consider in this paper is consistency, i.e. deciding
the existence of a model for a given ontology. Due to the expressivity of our asser-
tions, other reasoning problems such as satisfiability, subsumption, and instance
checking can be reduced to consistency in linear time. For example, a concept C
is p-subsumed by D w.r.t. O = (A, T , R), i.e. we have C I (x) ⇒ DI (x) ≥ p for all
models I of O and all x ∈ ∆I , iff (A ∪ {ha:C → D < pi}, T , R) is inconsistent,
where a is a fresh individual name.
4 Deciding Consistency
Consistency in L-ISCHOI with general TBoxes is ExpTime-complete, matching
the complexity of classical SHOI [20]. To show this, we adapt the automata-
based procedures from [1,13] to this more expressive logic. The conditions for
the role hierarchy, inverse roles, and transitive roles are similar to the tableaux
rules from [23]. To deal with nominals, we employ pre-completions inspired by the
approaches in [2,14,21]. In Section 5, we derive complexity results for consistency
in the sublogics L-IALCHO (without transitivity and inverse roles) and L-ISCOc
(without role inclusions, inverse roles, and fuzzy roles) with acyclic TBoxes.
It was shown in [13] that over a finite lattice L every interpretation I is
n-witnessed, where n is the width of the lattice. This means that for every
concept C, r ∈WN− I I
R , and x ∈ ∆ there are n witnesses y1 , . . . , yn ∈ ∆ such that
I n I I
(∃r.C) (x) = i=1 r (x, yi )⊗C (yi ), and similarly for the value restrictions. For
the sake of simplicity, we present the following reasoning procedure only for the
case of n = 1, i.e. we assume that all interpretations are (1-)witnessed. It can be
generalized to handle arbitrary n by easy adaptations of the following definitions,
in particular the introduction of more than one witness in Definition 12.
We now consider an ontology O = (A, T , R) that we want to test for con-
sistency. The main idea of the algorithm is to find an abstract representation
of a tree-shaped model of O, a so-called Hintikka tree. Every node of this tree
consists of a Hintikka function that describes the values of all relevant concepts
for one domain element of the model. Additionally, each Hintikka function stores
the values of all role connections from the parent node. We define the set sub(O)
to contain all subconcepts of concepts occurring in O, together with all ∃s.C
(and ∀s.C) for which ∃r.C (∀r.C) occurs in O, s vR r, and s is transitive.
Definition 10 (Hintikka function). A Hintikka function for O is a partial
function H : sub(O) ∪ N−
R (O) → L satisfying the following conditions:
– H(s) is defined for all s ∈ N−
R (O);
– if H(p) is defined, then H(p) = p;
– if H({a}) is defined, then H({a}) ∈ {0, 1};
– if H(C u D) is defined, then H(C) and H(D) are also defined and it holds
that H(C u D) = H(C) ⊗ H(D); and similarly for ¬C and C → D.
This function is compatible with
– an assertion ha:C ./ `i if, whenever H({a}) = 1, then H(C) is defined and
H(C) ./ `.
.
– a concept definition hA = C ≥ `i if, whenever H(A) is defined, then H(C)
is defined and (H(A) ⇒ H(C)) ⊗ (H(C) ⇒ H(A)) ≥ `.
– a GCI hC v D ≥ `i if H(C) and H(D) are defined and H(C) ⇒ H(D) ≥ `.
– a role inclusion r v s if H(r) ≤ H(s).
– an ABox/TBox/RBox/ontology if it is compatible with all axioms in it.
The support of H is the set supp(H) of all C ∈ sub(O) for which H is defined,
and Ind(H) is the set of all a ∈ NI (O) for which H({a}) = 1.
To deal with nominals, our algorithm maintains a polynomial amount of global
information about the named domain elements, called a pre-completion. Since
one domain element can have several names, we first consider a partition of NI (O)
that specifies which names are interpreted by the same elements. The pre-
completion further contains one Hintikka function for each named individual,
and the values of all role connections between them.
Definition 11 (pre-completion). A pre-completion for the ontology O is a
triple P = (P, HP , RP ), where P is a partition of NI (O), HP = (HX )X∈P is a
family of Hintikka functions for O, and RP = (rP )r∈NR (O) is a family of fuzzy
binary relations rP : P ×P → L, such that, for all X ∈ P, we have Ind(HX ) = X
and HX is compatible with O. A Hintikka function H for O is compatible with P
if for all a ∈ Ind(H), we have H|sub(O) = H[a]P |sub(O) .
−
We further set rP (X, Y ) := rP (Y, X) for all X, Y ∈ P and r ∈ NR (O).
The arity k of our Hintikka trees is the number of existential and value
restrictions in sub(O). Each successor in the tree describes the witness for one
restriction. For the following definition, we consider K := {1, . . . , k} as before
and fix a bijection ϕ : {C | C ∈ sub(O) is of the form ∃r.D or ∀r.D} → K.
Definition 12 (Hintikka condition). The tuple (H0 , H1 , . . . , Hk ) of Hintikka
functions for O satisfies the Hintikka condition if the following hold:
a) For every existential restriction ∃r.C ∈ sub(O):
– If ∃r.C ∈ supp(H0 ) and i = ϕ(∃r.C), then we have C ∈ supp(Hi ) and
H0 (∃r.C) = Hi (r) ⊗ Hi (C).
– If ∃r.C ∈ supp(H0 ), then for all i ∈ K, we have C ∈ supp(Hi ) and
H0 (∃r.C) ≥ Hi (r) ⊗ Hi (C); moreover, for all transitive roles s vR r,
we have ∃s.C ∈ supp(Hi ) and H0 (∃r.C) ≥ Hi (s) ⊗ Hi (∃s.C).
– For all i ∈ K with ∃r.C ∈ supp(Hi ), we have C ∈ supp(H0 ) and
Hi (∃r.C) ≥ Hi (r) ⊗ H0 (C); moreover, for all transitive roles s vR r,
we have ∃s.C ∈ supp(H0 ) and Hi (∃r.C) ≥ Hi (s) ⊗ H0 (∃s.C).
b) For every value restriction ∀r.C ∈ sub(O):
– If ∀r.C ∈ supp(H0 ) and i = ϕ(∀r.C), then we have C ∈ supp(Hi ) and
H0 (∀r.C) = Hi (r) ⇒ Hi (C).
– If ∀r.C ∈ supp(H0 ), then for all i ∈ K, we have C ∈ supp(Hi ) and
H0 (∀r.C) ≤ Hi (r) ⇒ Hi (C); moreover, for all transitive roles s vR r,
we have ∀s.C ∈ supp(Hi ) and H0 (∀r.C) ≤ Hi (s) ⇒ Hi (∀s.C).
– For all i ∈ K with ∀r.C ∈ supp(Hi ), we have C ∈ supp(H0 ) and
Hi (∀r.C) ≤ Hi (r) ⇒ H0 (C); moreover, for all transitive roles s vR r,
we have ∀s.C ∈ supp(H0 ) and Hi (∀r.C) ≤ Hi (s) ⇒ H0 (∀s.C).
c) For all r ∈ N− R (O) and i, j ∈ K such that a ∈ Ind(Hi ), b ∈ Ind(Hj ), and
[a]P = [b]P , we have Hi (r) = Hj (r).
d) For all a ∈ Ind(H0 ), r ∈ N− R (O), i ∈ K, and b ∈ Ind(Hi ), it holds that
Hi (r) = rP ([a]P , [b]P ).
Intuitively, Condition a) ensures that the designated successor satisfies the wit-
nessing condition for ∃r.C, and that the other successors do not interfere; this
includes the parent node, which is a r-predecessor. Additionally, existential re-
strictions are transferred along transitive roles, as in the ∀+ -rule from [23]. Con-
ditions c) and d) are concerned with the behavior of named successors; in par-
ticular, the values for the role connections between named individuals specified
by the pre-completion should be respected.
Given a pre-completion P = (P, HP , RP ), a Hintikka tree for O starting
with HX , X ∈ P, is a mapping T that assigns to each u ∈ K ∗ a Hintikka
function T(u) for O that is compatible with T , R, and P such that T(ε) = HX
and every tuple (T(u), T(u1), . . . , T(uk)) satisfies the Hintikka condition.
The proof of the following lemma can be found in [9].
Lemma 13. O is consistent iff there exist a pre-completion P = (P, HP , RP )
for O and, for each X ∈ P, a Hintikka tree for O starting with HX .
The Hintikka automaton for O and HX is the LA AO,HX := (QO , IHX , ∆O ),
where QO consists of all pairs (H, i) of Hintikka functions H for O that are
compatible with T , R, and P and indices i ∈ K, IHX := {(HX , 1)}, and ∆O
is the set of all tuples ((H0 , i0 ), (H1 , 1), . . . , (Hk , k)) such that (H0 , . . . , Hk ) sat-
isfies the Hintikka condition. It is easy to see that the first components of the
runs of AO,HX are exactly the Hintikka trees for O starting with HX , and the
second components simply store the index of the existential or value restriction
for which the state acts as a witness. By Lemma 13, consistency of O is thus
equivalent to the existence of a pre-completion and the non-emptiness of the
Hintikka automata AO,HX for each equivalence class X.
Since the number of pre-completions is bounded exponentially in the size of
the input (O and L) and each pre-completion is of size polynomial in the size of
the input, we can enumerate all pre-completions in exponential time and for each
of them check emptiness of the polynomially many automata AO,HX . Since the
size of these automata is exponential in the size of the input, by [33] we obtain
the following complexity result. ExpTime-hardness holds already in ALC [26].
Theorem 14. In L-ISCHOI over a finite residuated De Morgan lattice L, con-
sistency w.r.t. general TBoxes is ExpTime-complete.
5 Acyclic TBoxes
We now extend the previous complexity results for lattice-based fuzzy DLs with
acyclic TBoxes [13,14] by showing that consistency in L-IALCHO and L-ISCOc
is PSpace-complete in this setting. Recall that in L-ISCOc , roles must always
be interpreted as crisp functions that only take the values 0 and 1. Due to the
absence of inverse roles, in the following we can restrict all definitions to use
NR (O) instead of N−
R (O), and we can remove Condition d) and the last items of
Conditions a) and b) from Definition 12 [9].
Let now O = (A, T , R) be such that T is acyclic. We can guess a triple
P = (P, HP , RP ) and verify the conditions of Definition 11 in (nondeterminis-
tic) polynomial space. Thus, if emptiness of the polynomially many Hintikka au-
tomata AO,HX could be decided in polynomial space, we would obtain a PSpace
upper bound for consistency [25]. The idea is to modify the construction of AO,HX
using a faithful family of functions to obtain a PSpace on-the-fly construction.
As in [13], these automata already satisfy most of Definition 5, except the poly-
nomial bound on the maximal length a path before (equality) blocking occurs.
The faithful families of functions we use are very similar to those employed in [13]
for L-IALCHI and L-ISCI c .
For the subsequent constructions to work, we need to change the notion of
compatibility of a Hintikka function H with P to a weaker variant: we only
require that for every a ∈ Ind(H) and every C ∈ sub(O) for which H(C) is
defined, H[a]P (C) is also defined and H(C) = H[a]P (C). This new definition does
not work in the presence of inverse roles. However, in L-IALCHO and L-ISCOc ,
all previous results remain valid [9].
We now present a faithful family of functions for the case that O is formulated
in L-IALCHO. For this, we denote by rdT (C) the role depth of the unfolding of
a concept C w.r.t. the acyclic TBox T , by rdT (H) for a Hintikka function H the
maximal rdT (C) of a concept C ∈ supp(H), and by sub≤n (O) the restriction of
sub(O) to concepts C with rdT (C) ≤ n.
Definition 15 (family f). We define f = (fq )q∈QO for all q = (H, i) ∈ QO with
n := rdT (H) and all q 0 = (H 0 , i0 ) ∈ QO by fq (q 0 ) := (H 00 , i0 ), where, for every
C ∈ sub(O) and r ∈ NR (O),
( (
00 H 0 (C) if C ∈ sub≤n−1 (O), 00 H 0 (r) if supp(H) 6= ∅,
H (C) := H (r) :=
undefined otherwise; 0 otherwise.
For all q, q 0 ∈ QO , we have that fq (q 0 ) is again a state of AO,HX (according to the
new definition of compatibility with P). The idea is to reduce the maximal role
depth of the Hintikka function in every transition of the automaton. This works
since in the absence of transitive roles the Hintikka condition only constrains the
values of C for restrictions ∃r.C or ∀r.C that appear in the parent node. Thus,
(equality) blocking occurs after polynomially many transitions.
We show in [9] that f is faithful w.r.t. AO,HX and the construction of the in-
duced subautomaton AfO,HX from L, O, and HX constitutes a PSpace on-the-fly
construction. By Propositions 4 and 6, we obtain the desired complexity result;
PSpace-hardness holds already in classical ALC w.r.t. the empty TBox [27].
Theorem 16. In L-IALCHO over a finite residuated De Morgan lattice L, con-
sistency w.r.t. acyclic TBoxes is PSpace-complete.
For L-ISCOc , the construction is a little more involved. Since now the interpre-
tations of roles are restricted to 0 and 1, all Hintikka functions H for O need to
satisfy the additional condition that H(r) ∈ {0, 1} for all r ∈ NR (O). We further
denote by ϕr (O) for r ∈ NR (O) the set of all indices i ∈ K such that i = ϕ(C)
for a concept C of the form ∃r.D or ∀r.D. We then replace K in Definition 12
by ϕr (O). The idea is that in the absence of role inclusions it suffices to consider
one role for each successor. The resulting definition is closer to the Hintikka
condition from [13]. Lemma 13 remains valid under these modifications [9].
Given a Hintikka function H for O and a role name r, we define the set
H|r := {C ∈ supp(H) | C = ∃r.D or C = ∀r.D}.
Definition 17 (family g). We define g = (gq )q∈QO for all q = (H, i) ∈ QO with
n := rdT (H) and all q 0 = (H 0 , i0 ) ∈ QO and r0 ∈ NR (O) such that i0 ∈ ϕr0 (O) by
gq (q 0 ) := (H 00 , i0 ), where, for all C ∈ sub(O) and r ∈ NR (O):
(
sub≤n (O) ∩ H 0 |r0 if r0 is transitive,
P :=
∅ otherwise;
(
H 0 (C) if C ∈ sub≤n−1 (O) ∪ P ,
H 00 (C) :=
undefined otherwise;
(
H 0 (r) if supp(H) 6= ∅ and r = r0 ,
H 00 (r) :=
0 otherwise.
Again, the resulting pair (H 00 , i0 ) is an element of QO . Here, we cannot always
reduce the role depth of the Hintikka functions, but have to keep all existential
and value restrictions that are transferred along a transitive role r0 to ensure
that the family g is faithful w.r.t. AO,HX .
To prove that the induced subautomaton AgO,HX is obtained by a PSpace
on-the-fly construction, we have to employ a complicated blocking condition
that extends the one used for L-ISCI c in [13]. The main problem is to show
that every path in a run of this automaton involving the same transitive role r
can be blocked after polynomially many steps. The idea is that along such a
path, only the values of the concepts in H|r and their direct subconcepts are
relevant. Polynomial blocking follows from the facts that r is crisp and the
Hintikka condition thus guarantees the values of all these concepts to behave
monotonically along this path. For details, see the full proof in [9].
Propositions 4 and 6 and [27] now entail the following result.
Theorem 18. In L-ISCOc over a finite residuated De Morgan lattice L, consis-
tency w.r.t. acyclic TBoxes is PSpace-complete.
As a side effect, we obtain new, albeit not surprising, complexity results for the
underlying classical description logics.
Corollary 19. In classical ALCHO and SO, consistency w.r.t. acyclic TBoxes
is PSpace-complete.
SHOI
ALCHOI SOI SHO SHI
ALCOI ALCHO ALCHI SO SI SH
ALCO ALCI ALCH S
ALC
Fig. 1. The PSpace/ExpTime boundary in classical DLs with acyclic TBoxes
6 Conclusions
We have extended previous complexity results about fuzzy DLs with finite lat-
tice semantics to cover nominals. This required extensive adaptations of the
automata-based algorithm used for L-ISCHI and its sublogics in [13]. We em-
ployed pre-completions similar to those in [2,14,21] to show complexity results for
ontology consistency. Due to the expressivity of our ABoxes, these easily transfer
to other standard reasoning problems. In particular, we have shown that con-
sistency in L-ISCHOI w.r.t. general TBoxes can be decided in ExpTime. This
drops to PSpace when restricting to acyclic TBoxes in the sublogics L-IALCHO
and L-ISCOc . To the best of our knowledge, only the sublogics SI [1,23] and
ALCHI [13,14] of classical SHOI were known to have PSpace-complete rea-
soning problems w.r.t. acyclic TBoxes. On the other hand, in ALCOI and SH
reasoning is already ExpTime-hard without any TBox [22,31]. The present re-
sults for ALCHO and SO thus complete the picture about reasoning w.r.t. acyclic
TBoxes in the logics between ALC and SHOI (see Figure 1).
It would be interesting to extend the presented results to deal with fuzzy
role inclusions (hr v s ≥ pi) or cardinality restrictions (≥n r.C), although it is
not clear how to define the semantics of the latter in a setting where already
a simple existential restriction may entail the existence of n > 1 witnessing
role successors. We also plan to extend the automata-based algorithm for the
fuzzy DL G-IALC based on the so-called Gödel t-norm over the truth degrees
from [0, 1] to more expressive logics using the ideas presented here and in [13,14].
Acknowledgments
The author is indebted to Rafael Peñaloza for many discussions on the topics of
(fuzzy) DLs in general and automata-based reasoning procedures in particular.
References
1. Baader, F., Hladik, J., Peñaloza, R.: Automata can show PSPACE results for
description logics. Inform. Comput. 206(9-10), 1045–1056 (2008)
2. Baader, F., Lutz, C., Miličić, M., Sattler, U., Wolter, F.: Integrating description
logics and action formalisms for reasoning about web services. LTCS-Report 05-02,
Chair for Automata Theory, TU Dresden, Germany (2005), see http://lat.inf.tu-
dresden.de/research/reports.html
3. Baader, F., Peñaloza, R.: On the undecidability of fuzzy description logics with
GCIs and product t-norm. In: Proc. FroCoS’11, LNCS, vol. 6989, pp. 55–70.
Springer (2011)
4. Baader, F., Sattler, U.: An overview of tableau algorithms for description logics.
Studia Logica 69(1), 5–40 (2001)
5. Bobillo, F., Bou, F., Straccia, U.: On the failure of the finite model property in
some fuzzy description logics. Fuzzy Set. Syst. 172(1), 1–12 (2011)
6. Bobillo, F., Delgado, M., Gómez-Romero, J.: A crisp representation for fuzzy
SHOIN with fuzzy nominals and general concept inclusions. In: Uncertainty Rea-
soning for the Semantic Web I. LNAI, vol. 5327, pp. 174–188. Springer (2008)
7. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Joining Gödel and Zadeh
fuzzy logics in fuzzy description logics. Int. J. Uncertain. Fuzz. 20(4), 475–508
(2012)
8. Bobillo, F., Straccia, U.: Finite fuzzy description logics and crisp representations.
In: Uncertainty Reasoning for the Semantic Web II, LNCS, vol. 7123, pp. 102–121.
Springer (2013)
9. Borgwardt, S.: The complexity of fuzzy description logics over finite lattices with
nominals. LTCS-Report 14-02, Chair for Automata Theory, TU Dresden, Germany
(2014), see http://lat.inf.tu-dresden.de/research/reports.html.
10. Borgwardt, S., Distel, F., Peñaloza, R.: How fuzzy is my fuzzy description logic?
In: Proc. IJCAR’12. LNAI, vol. 7364, pp. 82–96. Springer (2012)
11. Borgwardt, S., Peñaloza, R.: Description logics over lattices with multi-valued on-
tologies. In: Proc. IJCAI’11. pp. 768–773. AAAI Press (2011)
12. Borgwardt, S., Peñaloza, R.: Undecidability of fuzzy description logics. In: Proc.
KR’12. pp. 232–242. AAAI Press (2012)
13. Borgwardt, S., Peñaloza, R.: The complexity of lattice-based fuzzy description
logics. J. Data Semant. 2(1), 1–19 (2013)
14. Borgwardt, S., Peñaloza, R.: Consistency reasoning in lattice-based fuzzy descrip-
tion logics. Int. J. Approx. Reason. (2014), in press.
15. Cerami, M., Garcia-Cerdaña, À., Esteva, F.: From classical description logic to
n-graded fuzzy description logic. In: Proc. FUZZ-IEEE’10. pp. 1–8. IEEE Press
(2010)
16. Cerami, M., Straccia, U.: On the (un)decidability of fuzzy description logics under
Łukasiewicz t-norm. Inform. Sciences 227, 1–21 (2013)
17. Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic
Glimpse at Substructural Logics, Studies in Logic and the Foundations of Mathe-
matics, vol. 151. Elsevier (2007)
18. Hájek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer (2001)
19. Hájek, P.: Making fuzzy description logic more general. Fuzzy Set. Syst. 154(1),
1–15 (2005)
20. Hladik, J.: To and Fro Between Tableaus and Automata for Description Logics.
Ph.D. thesis, Technische Universität Dresden, Germany (2007)
21. Hollunder, B.: Consistency checking reduced to satisfiability of concepts in termi-
nological systems. Ann. Math. Artif. Intell. 18(2-4), 133–157 (1996)
22. Horrocks, I.: Optimising Tableaux Decision Procedures for Description Logics.
Ph.D. thesis, University of Manchester, UK (1997)
23. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip-
tion logics. L. J. IGPL 8(3), 239–263 (2000)
24. Jiang, Y., Tang, Y., Wang, J., Deng, P., Tang, S.: Expressive fuzzy description
logics over lattices. Knowl.-Based Syst. 23(2), 150–161 (2010)
25. Savitch, W.J.: Relationships between nondeterministic and deterministic tape com-
plexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)
26. Schild, K.: A correspondence theory for terminological logics: Preliminary report.
In: Proc. IJCAI’91. pp. 466–471. Morgan Kaufmann (1991)
27. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with comple-
ments. Artif. Intell. 48(1), 1–26 (1991)
28. Straccia, U.: A fuzzy description logic. In: Proc. AAAI’98. pp. 594–599 (1998)
29. Straccia, U.: Transforming fuzzy description logics into classical description logics.
In: Proc. JELIA’04. LNCS, vol. 3229, pp. 385–399. Springer (2004)
30. Straccia, U.: Uncertainty in description logics: A lattice-based approach. In: Proc.
IPMU’04. pp. 251–258 (2004)
31. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals
in expressive description logics. J. Artif. Intell. Res. 12, 199–217 (2000)
32. Tresp, C.B., Molitor, R.: A description logic for vague knowledge. In: Proc.
ECAI’98. pp. 361–365. John Wiley and Sons (1998)
33. Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of pro-
grams. J. Comput. Syst. Sci. 32(2), 183–221 (1986)
34. Yen, J.: Generalizing term subsumption languages to fuzzy logic. In: Proc. IJ-
CAI’91. pp. 472–477. Morgan Kaufmann (1991)
35. Zadeh, L.A.: Fuzzy sets. Inform. Control 8(3), 338–353 (1965)