=Paper=
{{Paper
|id=Vol-1577/paper_2
|storemode=property
|title=Reasoning in Expressive Gödel Description Logics
|pdfUrl=https://ceur-ws.org/Vol-1577/paper_2.pdf
|volume=Vol-1577
|authors=Stefan Borgwardt,Rafael Peñaloza
|dblpUrl=https://dblp.org/rec/conf/dlog/BorgwardtP16
}}
==Reasoning in Expressive Gödel Description Logics==
https://ceur-ws.org/Vol-1577/paper_2.pdf
Reasoning in Expressive Gödel Description Logics
Stefan Borgwardt1 and Rafael Peñaloza2
1
Chair for Automata Theory, Theoretical Computer Science, TU Dresden, Germany
stefan.borgwardt@tu-dresden.de
2
KRDB Research Centre, Free University of Bozen-Bolzano, Italy
rafael.penaloza@unibz.it
Abstract. Fuzzy description logics (FDLs) are knowledge representation
formalisms capable of dealing with imprecise knowledge by allowing
intermediate membership degrees in the interpretation of concepts and
roles. One option for dealing with these intermediate degrees is to use
the so-called Gödel semantics, under which conjunction is interpreted by
the minimum of the degrees. Despite its apparent simplicity, developing
reasoning techniques for expressive FDLs under this semantics is a hard
task. In this paper, we illustrate two algorithms for deciding consistency
in (sublogics of) SROIQ under Gödel semantics.
1 Introduction
As it has been widely argued in the literature, one of the important deficits of
classical logic is the inability to handle imprecise concepts for which a clear-
cut characterization is impossible [15, 21]. To cover this gap, the semantics of
DLs has been extended following the ideas of mathematical fuzzy logic [13, 15].
Briefly, fuzzy description logics allow intermediate truth degrees—usually rational
numbers between 0 (false) and 1 (true)—to be used in the definition of imprecise
knowledge [1]. To interpret these intermediate degrees, the logical connectives
need to be extended accordingly. In general, there are many possible extensions
that can be used; hence, each DL gives rise to a family of FDLs. However, for
most of these extensions, reasoning becomes undecidable, even if the underlying
DL is relatively inexpressive [6]. In fact, the only decidable expressive FDLs are
those based on the Gödel semantics, and the related Zadeh semantics. Extensions
of classical DLs with the Gödel semantics are typically denoted by the prefix “G-”.
Developing a reasoning algorithm for classical SROIQ is far from trivial,
as one needs to handle all possible interactions between the constructors, e.g.
nominals and number restrictions. This difficulty is accentuated when the Gödel
semantics are considered, since this logic does not have the finitely valued model
property [5]. This means that there are ontologies whose models must use infinitely
many truth degrees. Indeed, this is one of the reasons why the crispification
approach as described in [4, 7, 23] is only correct under finitely valued semantics.
The study of reasoning algorithms for expressive Gödel FDLs started in [5,11],
where an automata-based approach was developed, showing that the loss of the
finitely valued model property does not affect the complexity of reasoning in
G-ALC. Rather than trying to find a model directly, this algorithm produces
an abstract representation of a large class of models. In this representation, the
actual degrees of truth used in a model are abstracted to consider only the order
among them. This abstraction from the actual degrees is also exploited by an
extension of the crispification approach [8, 9], which translates a fuzzy ontology
into a classical ontology by using concepts that simulate the order between the
relevant truth degrees. As an added benefit, considering only the order between
concepts allows for a more flexible representation of the domain knowledge in
which, for instance, one can express that an individual is taller than another,
without having to specify explicit degrees of tallness.
Although they provide good theoretical results such as tight complexity
bounds for reasoning, these approaches are restricted to sublogics of G-SROIQ
having the forest-model property, and there is no obvious way to extend them
to the full expressivity of G-SROIQ. In [10], we have developed a new tableau
algorithm to deal with full G-SROIQ. The new algorithm combines the ideas
of the classical tableau approach for SROIQ with the order-based abstraction
developed in [5, 9]. It inherits the pay-as-you-go behavior from the classical
tableau algorithms, and is the first reasoning algorithm that can handle the full
expressivity of fuzzy SROIQ under Gödel semantics. Due to space restrictions,
in this paper we only illustrate the core ideas of the two algorithms from [9, 10]
on an example.
2 Preliminaries
The two basic operators of Gödel fuzzy logic are conjunction and implication,
interpreted by the Gödel t-norm and residuum, respectively. The Gödel t-norm
of two fuzzy degrees x, y ∈ [0, 1] is defined as minimum function min{x, y}. The
residuum ⇒ is uniquely defined by the equivalence min{x, y} 6 z iff y 6 (x ⇒ z)
for all x, y, z ∈ [0, 1], and can be computed as
(
1 if x 6 y,
x⇒y=
y otherwise.
We consider both the residual negation (that maps each value x to x ⇒ 0) and
the involutive negation (that maps x to 1 − x) in this paper.
An order structure is a finite set S containing at least the numbers 0, 0.5, and 1,
together with an involutive unary operation inv : S → S such that inv(x) = 1 − x
for all rational numbers x ∈ S ∩ [0, 1]. A total preorder (on S) is a transitive and
total binary relation 4∗ ⊆ S × S. The set order(S) contains exactly those total
preorders 4∗ over S which
– have 0 and 1 as least and greatest element, respectively,
– coincide with the order of the rational numbers on S ∩ [0, 1], and
– satisfy α 4∗ β iff inv(β) 4∗ inv(α) for all α, β ∈ S.
Given 4∗ ∈ order(S), the following functions extend the operators of Gödel fuzzy
logic from S ∩ [0, 1] to S:
( (
α if α 4∗ β 1 if α 4∗ β
min∗ {α, β} := α ⇒∗ β :=
β otherwise, β otherwise.
An order assertion (over S) is an expression of the form α ./ β, where α, β ∈ S
and ./ ∈ {<, 6, =, >, >}. An order formula is a Boolean combination of order
assertions. The satisfaction of an order formula by an element 4∗ ∈ order(S) is
defined in the obvious way, and can be extended to more complex expressions like
α > min{β, γ} or α = (β ⇒ γ) using the operators min∗ and ⇒∗ . A set of order
assertions Φ is satisfiable if it has a model 4∗ ∈ order(S). Satisfiability of order
assertions can be decided in polynomial time by checking for cycles involving
strict order assertions.
2.1 G-SROIQ
The syntax of concepts and roles in G-SROIQ extends that of classical SROIQ,
based on the sets NI , NC , and NR of individual names, concept names, and role
names, respectively. The set NR includes the universal role ru , and N− R denotes
the set of all (atomic and inverse) roles. Additionally, we allow truth constants p
with p ∈ [0, 1] and implication C → D as concept constructors. The semantics is
based on G-interpretations I = (∆I , ·I ) over a non-empty domain ∆I , which
assign to each individual name a ∈ NI an element aI ∈ ∆I , to each concept name
A ∈ NC a fuzzy set AI : ∆I → [0, 1], and to each role name r ∈ NR a fuzzy binary
relation rI : ∆I × ∆I → [0, 1]. This G-interpretation is extended to complex
concepts and roles as defined in the last column of Table 1, for all d, e ∈ ∆I .
We can express the common DL constructors > := 1 (top), ⊥ := 0 (bottom),
C t D := ¬(¬C u ¬D) (disjunction), and 6n s.C := ¬(>(n + 1) s.C) (at-most re-
striction). In some previous work on fuzzy extensions of SROIQ (e.g. [4]), the lat-
ter are defined using the residual negation; that is 6n s.C := (>(n + 1) s.C) → ⊥.
This has the effect that the value of 6n r.C is always either 0 or 1. However,
this discrepancy in definitions is not an issue since our algorithms can handle
both the involutive and the residual negation. The use of truth constants p for
p ∈ [0, 1] is not standard in FDLs, but it allows us to simulate fuzzy nominals [2]
of the form {p1 /a1 , . . . , pn /an } with pi ∈ [0, 1] and ai ∈ NI , 1 6 i 6 n, using the
concept ({a1 } u p1 ) t · · · t ({an } u pn ). Recall that we use only rational numbers.
A (classical) assertion is either a concept assertion of the form C(a) or a role
assertion of the form r(a, b) for a, b ∈ NI , a concept C, and a role r. A (fuzzy)
assertion is of the form α ./ p or α ./ β, where α, β are classical assertions,
./ ∈ {<, 6, =, >, >}, and p ∈ [0, 1]. An ABox is a finite set of fuzzy assertions
and individual (in)equality assertions of the form a ≈ b (a 6≈ b) for a, b ∈ NI . A
TBox is a finite set of general concept inclusions (GCIs) of the form C v D > p
for concepts C, D and p ∈ (0, 1]. A role hierarchy Rh is a finite set of (complex)
role inclusions of the form w v r > p, where r is a role name different from the
universal role, w ∈ (N− +
R ) is a non-empty role chain not including the universal
Table 1. Syntax and semantics of G-SROIQ
Name Syntax Semantics (C I (d) / rI (d, e))
concept name A AI (d) ∈ [0, 1]
truth constant p p
conjunction C uD min{C I (d), DI (d)}
implication C→D C I (d) ⇒ DI (d)
negation ¬C 1 − C I (d)
existential restriction ∃r.C sup min{rI (d, e), C I (e)}
e∈∆I
value restriction ∀r.C inf rI (d, e) ⇒ C I (e)
e∈∆I
(
1 if d = aI
nominal {a}
0 otherwise
n
at-least restriction >n s.C sup min min{sI (d, ei ), C I (ei )}
I i=1
e1 ,...,en ∈∆
pairwise different
I
local reflexivity ∃s.Self r (d, d)
role name r rI (d, e) ∈ [0, 1]
inverse role r− rI (e, d)
universal role ru 1
role, and p ∈ (0, 1]. The notions of regularity and simple roles are defined w.r.t. a
given role hierarchy Rh as for classical SROIQ [3,18,19], and we adopt the same
syntactical restrictions, e.g. that number restrictions can only contain simple
roles, to avoid undecidability. An RBox R = Rh ∪ Ra consists of a regular
role hierarchy Rh and a finite set Ra of disjoint role axioms dis(s1 , s2 ) > p
and reflexivity axioms ref(r) > p, where r is a role, s1 , s2 are simple roles, and
p ∈ (0, 1]. An ontology O = (A, T , R) consists of an ABox A, a TBox T , and an
RBox R.
A G-interpretation I satisfies (or is a model of)
– the fuzzy assertion α ./ β if αI ./ β I , where we set (C(a))I := C I (aI ),
(r(a, b))I := rI (aI , bI ), and pI := p for all p ∈ [0, 1];
– the (in)equality assertion a ≈ b (a 6≈ b) if aI = bI (aI 6= bI );
– the GCI C v D > p iff C I (d) ⇒ DI (d) > p for all d ∈ ∆I ;
– the role inclusion r1 . . . rn v r > p iff (r1 . . . rn )I (d0 , dn ) ⇒ rI (d0 , dn ) > p
for all d0 , dn ∈ ∆I , where
n
(r1 . . . rn )I (d0 , dn ) := sup min riI (di−1 , di );
d1 ,...,dn−1 ∈∆I i=1
– the disjoint role axiom dis(s1 , s2 ) > p iff min{sI1 (d, e), sI2 (d, e)} 6 1 − p for
all d, e ∈ ∆I ;
– the reflexivity axiom ref(r) > p iff rI (d, d) > p for all d ∈ ∆I ;
– an ontology if it satisfies all its axioms.
We can simulate other axioms of SROIQ [4, 17] as follows:
– transitivity axioms tra(r) > p by rr v r > p;
– symmetry axioms sym(r) > p by r− v r > p;
– asymmetry axioms asy(s) > p by dis(s, s− ) > p;
– irreflexivity axioms irr(s) > p by ∃s.Self v ¬p > 1; and
– negated role assertions ¬r(a, b) > p by r(a, b) 6 1 − p.
As usual for FDLs, we consider only witnessed G-interpretations [16]. Intu-
itively, this ensures that the suprema and infima in the semantics of the concept
constructors are in fact maxima and minima, respectively. In other words, the
degrees of these constructors are witnessed by elements of the domain. Note that
this restriction is not without loss of generality. Formally, a G-interpretation I
is witnessed if, for every d ∈ ∆I , n > 0, r ∈ N− −
R , simple s ∈ NR , and concept C,
there are e, e0 , e1 , . . . , en ∈ ∆I such that e1 , . . . , en are pairwise different,
(∃r.C)I (d) = min{rI (d, e), C I (e)},
(∀r.C)I (d) = rI (d, e0 ) ⇒ C I (e0 ), and
n
(>n s.C)I (d) = min min{sI (d, ei ), C I (ei )}.
i=1
We could also require witnesses for role chains in complex role inclusions, but this
is not usually done, and not necessary for our algorithms. A G-SROIQ ontology
is consistent if it has a witnessed G-model.
Other common reasoning problems for FDLs, such as concept satisfiability
and subsumption can be reduced to consistency in linear time [11]. For instance,
the subsumption between C and D to degree p w.r.t. a TBox T and an RBox R
is equivalent to the inconsistency of ({(C → D)(a) < p}, T , R), where a is a
fresh individual name. Likewise, the satisfiability of C to degree p w.r.t. T and R
is equivalent to the consistency of ({C(a) > p}, T , R). One can even show that
the best satisfiability and subsumption degrees are always values occurring in the
input ontology, and can be computed using linearly many consistency tests [11].
Hence, we restrict our attention to the problem of deciding consistency of fuzzy
ontologies.
3 The Algorithms
The main idea for both our algorithms is that, instead of explicitly defining the
degrees of all concepts and roles for all domain elements, we only represent the
order between different values. For example, to satisfy the semantics of →, i.e.
(C → D)I (x) = C I (x) ⇒ DI (x), it suffices to consider the two cases
– (C → D)I (x) = 1 and C I (x) 6 DI (x); or
– (C → D)I (x) = DI (x) and C I (x) > DI (x).
In both cases, it is irrelevant what the actual values of C I (x) and DI (x) are, as
long as they satisfy a certain order relationship. We exploit this property of the
Gödel operators in the following constructions, by using order structures and
order assertions to represent the semantics of concepts. This idea has also been
used for other reasoning problems based on the Gödel semantics [14].
For the nonce, we use the small example ontology O := (A, T , ∅), where
A := {(∃r.A)(a) > pA , (∃r.B)(a) > pB , (61 r.C)(a) > pC },
T := {A v C > 1, B v C > 1},
and pA , pB , pC are arbitrary values, to illustrate the algorithms.
3.1 Reduction to Classical DLs
Our first algorithm is based on a reduction of the fuzzy ontology O to a classical
ontology red(O). We use special concept names to express order assertions over
a specific order structure U. This order structure contains all values occurring
in O, all relevant subconcepts and roles, e.g. ∃r.A1 and r, relevant assertions
over known individuals, such as (61 r.C)(a), and special role assertions of the
form r(∗, a), as explained below. For example, the concept name C > (∃r.A)(a)
expresses that the value of C at the current domain element should exceed the
value of ∃r.A at a. We call these concept names order concepts and, to improve
readability, will denote them always with a surrounding box. This approach can
be seen as an extension of previous algorithms for reasoning in fuzzy DLs based
on reductions to classical DLs [2, 4, 7], which use cut-concepts of the form A > p ,
but are applicable only for fuzzy semantics based on finitely many values.
To achieve the correct behavior, our reduction explicitly specifies the semantics
of the order structure and the concept constructors. For example, we use the
classical axioms > v α 6 β t β 6 α , for all α, β ∈ U to express that 6 should
be total. The assertions in our ABox A are translated into classical assertions,
e.g. (∃r.A)(a) > pA (a). To ensure that (∃r.A)(a) actually represents the value
of the existential restriction ∃r.A at the individual a, we use the additional
assertion (∃r.A)(a) = (∃r.A) (a). The GCIs from our example ontology have the
straightforward translations
> v A ⇒ C > 1 and > v B ⇒ C > 1 ,
which require that they are satisfied in every element of the domain.
In the reduction, domain elements are connected via only one special role,
denoted by r. This role is used to transfer information between domain elements.
The goal is that, except for the named individuals, the role r will generate a
forest-shaped structure in the classical interpretation; hence this approach is
restricted to logics having the forest-model property, i.e. SRIQ, SROQ, and
SROI [12].
Information about the named individuals is transferred to all r-connected
domain elements using GCIs like (∃r.A)(a) > (∃r.B)(a) v ∀r. (∃r.A)(a) > (∃r.B)(a) ,
i.e. whenever a domain element x “knows” something about the behavior of a, then
all r-successors of x share that knowledge. Special elements of U of the form hCi↑
are used to refer to the value of a concept C at the parent node in the tree. These
elements are restricted by axioms like (∃r.B) 6 C v ∀r. AN → h∃r.Bi↑ 6 hCi↑ ,
which express that order relations between concepts of the parent are known
by all child nodes, i.e. r-successors. The special concept name AN is used to
distinguish anonymous domain elements from those that are designated by an
individual name (and are hence not part of the forest).
In our example, to generate a witness for the existential restriction ∃r.A at a
(and all other domain elements), we introduce the axiom
> v ∃r. AN u h∃r.Ai↑ 6 min{r, A} t ∃r.{a} u (∃r.A) 6 min{r(∗, a), A(a)} .
That is, either a has an anonymous (AN) r-successor at which the value of ∃r.A at
the parent node (h∃r.Ai↑ ), in this case a, is bounded by the minimum between the
r-connection to the parent node (r) and the value of A at the current node (A);
or there is an r-successor that satisfies {a}, i.e. a itself, and the value of ∃r.A at a
is bounded by the minimum between the value of the role connection from the
current node (represented by ∗) to a and the value of A at a (A(a)). In general,
the second part has to consider all named domain elements as possible successors;
in our example we have only a.
On the other hand, all r-successors have to be restricted to not exceed the
value of ∃r.A using the similar axioms
> v ∀r. AN → h∃r.Ai↑ > min{r, A} and ∃r.{a} v (∃r.A) > min{r(∗, a), A(a)} .
Similar axioms are introduced to express the semantics of ∃r.B.
For the number restriction 61 r.C = ¬>2 r.C, we first create witnesses as for
the existential restrictions above:
> v >2 r. AN u h>2 r.Ci↑ 6 min{r, C} t
>1 r. AN u h>2 r.Ci↑ 6 min{r, C} u (>2 r.C) 6 min{r(∗, a), C(a)}
That is, either there exist two anonymous witnesses for the value of >2 r.C, or
one anonymous witness and a serves as another witness. In general, the reduction
needs to consider all possible (exponentially many) combinations of named and
unnamed domain elements as witnesses for number restrictions; in this example
there are only 2 cases. Dually, there can be at most one r-successor that exceeds
the value given by >2 r.C at a, which is encoded in the assertion
61 r. AN u h>2 r.Ci↑ < min{r, C} t ¬AN u (>2 r.C)(a) < min{r(a, ∗), C} (a).
All the axioms listed above are collected into a classical ontology red(O), and
any classical model of this ontology obtained by a classical reasoner can be used
to construct a G-model of O. Hence, while this reduction incurs an exponential
blow-up in the size of the ontology due to the interaction of nominals and number
restrictions, it enables us to use existing optimized reasoners to decide consistency
of G-SROIQ ontologies.
3.2 The Tableau Algorithm
In contrast, our tableau algorithm explicitly creates a G-model of O by introducing
new domain elements, which we call nodes. It uses an order structure that is
similar to the one used for the reduction described above. The main difference
is that the order structure now also contains concept and role assertions of the
form B(x) and r(x, y), where x and y are nodes. In this way, we can express the
semantics directly using order assertions, e.g. (∃r.A)(x) > min{r(x, y), A(y)} for
all nodes x and y. However, the latter expression is not fully determined: that is,
we do not know whether (∃r.A)(x) > r(x, y), or (∃r.A)(x) > A(y) holds. In our
tableau algorithm, we resolve this nondeterminism by considering only atomic
order assertions, i.e. without using the abbreviations min and ⇒. In order to
guarantee that these sets can be used to construct a G-model of O, we need to
ensure that they remain satisfiable.
In our example, the tableau algorithm is initialized with one node a repre-
senting the individual of the same name, and the order assertions from A, where
the at-most assertion is equivalent to an upper bound on the corresponding
at-least-restriction: (>2 r.C)(a) 6 1 − pC . Afterwards, (nondeterministic) tableau
rules are applied exhaustively to create new nodes and order assertions; we only
present a few selected nondeterministic choices here. Similar to classical tableau
algorithms, first the (∃)-rule creates two witnesses x and y for the existential
restrictions ∃r.A and ∃r.B, respectively, at a. For example, we need to ensure
that (∃r.A)(a) = min{r(a, x), A(x)} is satisfied. One possibility is to introduce
the order assertions
(∃r.A)(a) = r(a, x) and (∃r.A)(a) 6 A(x),
expressing that the above minimum is realized by the value of the role connection
from a to x. Although it does not seem necessary, we need to have equality here
in order to prove completeness of the algorithm. Likewise, for y we assert that
(∃r.B)(a) 6 r(a, y) and (∃r.B)(a) = B(y).
Moreover, the supremum-based semantics of existential restrictions also imposes
an upper bound on all other r-successors, similar to the behavior of classical
value restrictions. Hence, we also assert that
(∃r.B)(a) > B(x) and (∃r.A)(a) > r(a, y).
In the next step, the GCIs are applied to all nodes; we ignore a here since it
is not relevant for this example. For the node x, we know already that
B(x) 6 (∃r.B)(a) 6 r(a, y) 6 (∃r.A)(a) 6 A(x),
and hence it suffices to assert in addition that A(x) 6 C(x), which then implies
that also B(x) 6 C(x) holds. For y, we introduce the order assertions
A(y) 6 C(y) and B(y) 6 C(y).
1
C(x)
A(x)
(∃r.A)(a), r(a, x) C(y)
r(a, y)
(∃r.B)(a), B(y)
B(x) A(y)
0
Fig. 1. Order diagram of the preorder induced by the order assertions produced in the
example by the first applications of tableau rules.
The resulting set of assertions entails the preorder depicted in Figure 1, where we
ignore pA , pB , pC , and all irrelevant elements of the order structure. Note that,
although we consider as models only total preorders, the assertions themselves
need not define a single total order over all elements of the order structure.
Now we deal with the number restriction (61 r.C)(a). In the following, we
ignore the required witnesses, as they are not essential for the example. As in the
classical tableau algorithm, we use a tableau rule that forces each r-successor of a
to choose whether it wants to “challenge” the number restriction or not. In the
classical setting, this means choosing whether to satisfy C or not. Here, we have
to decide whether ¬(61 r.C)(a) < min{r(a, x), C(x)} holds. If this inequality
holds for at least 2 nodes, then the supremum in the semantics of the at-least
restriction (>2 r.C) = ¬(61 r.C) is violated. We analyze several possibilities:
– If it holds that (>2 r.C)(a) > r(a, x) = min{r(a, x), C(x)} and additionally
(>2 r.C)(a) < min{r(a, y), C(y)}, then
r(a, y) 6 (∃r.A)(a) = r(a, x) 6 (>2 r.C)(a) < min{r(a, y), C(y)} 6 r(a, y).
In this case, the resulting set of order assertions is not satisfiable anymore.
– If (>2 r.C)(a) < r(a, x) and (>2 r.C)(a) > min{r(a, y), C(y)}, then it de-
pends on the values of pA , pB , and pC whether we can build a G-model.
If (>2 r.C)(a) 6 1 − pC < pB 6 (∃r.B)(a) 6 (>2 r.C)(a), then this is
obviously not possible. On the other hand, supposing that pA = 12 and
pC = pB = 14 , we can construct a G-model by assigning the value 14 to
A(y), B(x), B(y), r(a, y), C(y) and 12 to r(a, x), A(x), C(x). This means that
(∃r.A)(a) evaluates to 12 , (∃r.B)(a) to 14 , and (61 r.C)(a) to 14 , and hence O
is satisfied.
– If (>2 r.C)(a) < r(a, x) and (>2 r.C)(a) < min{r(a, y), C(y)}, then the at-
least restriction is violated. Thus, we have to apply another rule to merge
the node y into x (or vice versa), which essentially amounts to discarding
the node y and replacing all occurrences of y in the order assertions by x.
Hence, almost all relevant elements of the order structure become equivalent,
the only exception being (>2 r.C)(a), which must be strictly smaller than
all other elements. A possible resulting G-model could simply assign 1 to
A(x), B(x), C(x), r(a, x), which would result in (>2 r.C)(a) being evaluated
to 0. Again, all axioms of O are satisfied.
3.3 Complex Role Inclusions
For the tableau algorithm in [18], certain finite automata are constructed in order
to deal with complex role inclusions. For each role r, the automaton Ar reads role
chains, i.e. words over the alphabet of all roles, and recognizes exactly those role
chains that imply r. In [18], these automata are then used in concept expressions
of the form ∀A.C with the intuitive semantics that all domain elements connected
by a chain of roles recognized by A to the current domain element should satisfy C.
This allows to decompose inferences about complex role inclusions into single
0
steps by enforcing certain connections between ∀Aq .C and ∀Aq .C, where Aq
denotes the automaton A with q as initial state, and q 0 is a successor state of q.
For example, if q 0 is reachable via an r-transition from q and the current domain
0
element “satisfies” ∀Aq .C, then any r-successor has to satisfy ∀Aq .C
For our setting, we generalize this construction to weighted finite automata
recognizing the degree to which a given role chain implies a certain role r [9].
We closely follow the ideas from [18], but need to incorporate the degrees to
which the role inclusions hold to the transitions of the automata. As in [18], the
construction of Ar causes an exponential blowup in the size of R. However, it is
known that such a blowup cannot be avoided [20].
3.4 Results
In addition to the blow-up from this automata construction, our first algorithm,
based on the reduction to a classical ontology, produces an exponential blowup in
the (binary encoding of) the largest number n involved in a number restriction
in O, and in the number of individual names occurring in O. However, we can
avoid both if either nominals or number restrictions are disallowed.
In the reduction, from O we always obtain a classical ALCOQ ontology
red(O), regardless of whether O uses inverse roles or nominals. However, if O
does not use number restrictions, then red(O) is an ALCO ontology. As mentioned
before, the reduction is only correct for logics having the forest-model property,
i.e. G-SRIQ, G-SROQ, and G-SROI and their sublogics [12]. We can thus lift
the following complexity results from classical DLs.
Theorem 1. Deciding consistency is
– 2-ExpTime-complete in G-SRIQ, G-SROI, and G-SROQ, and
– ExpTime-complete in all FDLs between G-ALC and G-SHOI or G-SHIQ.
Proof. The consistency of the ALCOQ ontology red(O) is decidable in exponential
time in the size of red(O) [12]. The first upper bound thus follows from the fact
that the size of red(O) is exponential in the size of O. 2-ExpTime-hardness, even
without involutive negation and assertions restricted to the form α > p, follows
from classical results [20] since in this case reasoning in sublogics of G-SROIQ
is equivalent to reasoning in the underlying classical DLs [6].
Without complex role inclusions, i.e. restricting to simple role inclusions and
transitivity axioms, the size of the automata Ar is polynomial in the size of R [18].
The other exponential blowup can be avoided by disallowing nominals or number
restrictions. Hence, for G-SHOI and G-SHIQ, the size of red(O) is polynomial
in the size of O, and the lower bound follows again from the reduction in [6] and
ExpTime-hardness of consistency in classical ALC [22]. t
u
These results hold regardless of whether the numbers in number restrictions are
encoded in unary or in binary. We leave open the complexity of consistency in
G-SHOQ, which is ExpTime-complete in the classical case [12].
The tableau algorithm does not allow us to derive a tight bound on the
complexity of G-SROIQ since it may create triply exponentially many nodes in
the size of O. The resulting worst-case complexity of 3-NExpTime is the same
bound that is obtained from the classical tableau algorithm for SROIQ [17].
This is in contrast to 2-NExpTime-completeness of classical SROIQ [20], where
the upper bound is obtained by a reduction to the two-variable fragment of
first-order logic with counting quantifiers. The 2-NExpTime-hardness can again
be transferred to our setting via the reduction in [6].
4 Conclusions
We have described two algorithms for deciding consistency of (sublogics of) fuzzy
SROIQ under infinitely valued Gödel semantics. The first approach involves
an exponential blowup in the “depth” of the role hierarchy (which cannot be
avoided [20]) and in the number of individual names if number restrictions and
nominals are combined. However, it allows to directly exploit optimized classical
reasoners for FDL reasoning, like the previous crispification algorithms for finitely
valued FDLs [2, 4, 7, 23]. The tableau-based algorithm is more goal-oriented, but
has not been implemented yet. While it also uses the automata-based encoding
of role inclusions, it has the same complexity as the classical tableau algorithm
for SROIQ [17].
In this paper, our goal was to provide a general intuition of the two algorithms
via a simple example. For the full details of the algorithms, including proofs of
correctness, we refer the interested reader to [8–10].
References
1. Bobillo, F., Cerami, M., Esteva, F., García-Cerdaña, À., Peñaloza, R., Straccia, U.:
Fuzzy description logic. In: Cintula, P., Fermüller, C.G., Noguera, C. (eds.) Hand-
book of Mathematical Fuzzy Logic, Studies in Logic, vol. 3. College Publications
(2016)
2. Bobillo, F., Delgado, M., Gómez-Romero, J.: A crisp representation for fuzzy
SHOIN with fuzzy nominals and general concept inclusions. In: da Costa, P.C.G.,
d’Amato, C., Fanizzi, N., Laskey, K.B., Laskey, K.J., Lukasiewicz, T., Nickles, M.,
Pool, M. (eds.) Uncertainty Reasoning for the Semantic Web I. Lecture Notes in
Artificial Intelligence, vol. 5327, pp. 174–188. Springer-Verlag (2008)
3. Bobillo, F., Delgado, M., Gómez-Romero, J.: Optimizing the crisp representation of
the fuzzy description logic SROIQ. In: da Costa, P.C.G., d’Amato, C., Fanizzi, N.,
Laskey, K.B., Laskey, K.J., Lukasiewicz, T., Nickles, M., Pool, M. (eds.) Uncertainty
Reasoning for the Semantic Web I. Lecture Notes in Artificial Intelligence, vol.
5327, pp. 189–206. Springer-Verlag (2008)
4. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Joining Gödel and
Zadeh fuzzy logics in fuzzy description logics. International Journal of Uncertainty,
Fuzziness and Knowledge-Based Systems 20(4), 475–508 (2012)
5. Borgwardt, S., Distel, F., Peñaloza, R.: Decidable Gödel description logics with-
out the finitely-valued model property. In: Baral, C., De Giacomo, G., Eiter, T.
(eds.) Proc. of the 14th Int. Conf. on Principles of Knowledge Representation and
Reasoning (KR’14). pp. 228–237. AAAI Press (2014), http://www.aaai.org/ocs/
index.php/KR/KR14/paper/view/7803
6. Borgwardt, S., Distel, F., Peñaloza, R.: The limits of decidability in fuzzy description
logics with general concept inclusions. Artificial Intelligence 218, 23–55 (2015)
7. Borgwardt, S., Mailis, T., Peñaloza, R., Turhan, A.Y.: Answering fuzzy conjunctive
queries over finitely valued fuzzy ontologies. Journal on Data Semantics (2016), in
press. DOI: 10.1007/s13740-015-0055-y
8. Borgwardt, S., Peñaloza, R.: Infinitely valued Gödel semantics for expressive de-
scription logics. LTCS-Report 15-11, Chair for Automata Theory, TU Dresden,
Germany (2015), see http://lat.inf.tu-dresden.de/research/reports.html.
9. Borgwardt, S., Peñaloza, R.: Reasoning in expressive description logics under
infinitely valued Gödel semantics. In: Lutz, C., Ranise, S. (eds.) Proc. of the 10th
Int. Symp. on Frontiers of Combining Systems (FroCoS’15). Lecture Notes in
Artificial Intelligence, vol. 9322, pp. 49–65. Springer-Verlag (2015)
10. Borgwardt, S., Peñaloza, R.: A tableau algorithm for SROIQ under infinitely
valued Gödel semantics. LTCS-Report 15-18, Chair for Automata Theory, TU
Dresden, Germany (2015), see http://lat.inf.tu-dresden.de/research/reports.html.
11. Borgwardt, S., Peñaloza, R.: Reasoning in fuzzy description logics using automata.
Fuzzy Sets and Systems (2016), in press.
12. Calvanese, D., Eiter, T., Ortiz, M.: Regular path queries in expressive description
logics with nominals. In: Boutilier, C. (ed.) Proc. of the 21st Int. Joint Conf. on
Artificial Intelligence (IJCAI’09). pp. 714–720. AAAI Press (2009), http://ijcai.
org/papers09/Papers/IJCAI09-124.pdf
13. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic,
Studies in Logic, vol. 37–38. College Publications (2011), 2 volumes.
14. Guller, D.: On the satisfiability and validity problems in the propositional Gödel
logic. Computational Intelligence 399, 211–227 (2012)
15. Hájek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer-Verlag
(2001)
16. Hájek, P.: Making fuzzy description logic more general. Fuzzy Sets and Systems
154(1), 1–15 (2005)
17. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty,
P., Mylopoulos, J., Welty, C. (eds.) Proc. of the 10th Int. Conf. on Principles of
Knowledge Representation and Reasoning (KR’06). pp. 57–67. AAAI Press (2006),
http://www.aaai.org/Library/KR/2006/kr06-009.php
18. Horrocks, I., Sattler, U.: Decidability of SHIQ with complex role inclusion axioms.
Artificial Intelligence 160(1–2), 79–104 (2004)
19. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip-
tion logics. Logic Journal of the Interest Group in Pure and Applied Logic 8(3),
239–263 (2000)
20. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Brewka, G., Lang,
J. (eds.) Proc. of the 11th Int. Conf. on Principles of Knowledge Representation
and Reasoning (KR’08). pp. 274–284. AAAI Press (2008), http://www.aaai.org/
Library/KR/2008/kr08-027.php
21. Lukasiewicz, T., Straccia, U.: Managing uncertainty and vagueness in description
logics for the semantic web. Journal of Web Semantics 6(4), 291–308 (2008)
22. Schild, K.: A correspondence theory for terminological logics: Preliminary report.
In: Mylopoulos, J., Reiter, R. (eds.) Proc. of the 12th Int. Joint Conf. on Artificial
Intelligence (IJCAI’91). pp. 466–471. Morgan Kaufmann (1991), http://ijcai.
org/Past%20Proceedings/IJCAI-91-VOL1/PDF/072.pdf
23. Straccia, U.: Transforming fuzzy description logics into classical description logics.
In: Alferes, J.J., Leite, J.A. (eds.) Proc. of the 9th Eur. Conf. on Logics in Artificial
Intelligence (JELIA’04). Lecture Notes in Computer Science, vol. 3229, pp. 385–399.
Springer-Verlag (2004)