=Paper=
{{Paper
|id=None
|storemode=property
|title=Combining DL-Lite with Spatial Calculi for Feasible Geo-thematic Query Answering
|pdfUrl=https://ceur-ws.org/Vol-846/paper_23.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/OzcepM12
}}
==Combining DL-Lite with Spatial Calculi for Feasible Geo-thematic Query Answering==
https://ceur-ws.org/Vol-846/paper_23.pdf
Combining DL-Lite with Spatial Calculi for
Feasible Geo-thematic Query Answering
Özgür Lütfü Özçep and Ralf Möller
Institute for Software Systems (STS)
Hamburg University of Technology
Hamburg, Germany
{oezguer.oezcep,moeller}@tu-harburg.de
Abstract. First order logic (FOL) rewritability is a desirable feature
for query answering over geo-thematic ontologies because in most geo-
processing scenarios one has to cope with large data volume. Hence,
there is a need for combined geo-thematic logics that provide a suf-
ficiently expressive query language allowing for FOL rewritability. The
DL-Lite family of description logics is tailored towards FOL rewritability
of query answering for unions of conjunctive queries, hence it is a suit-
able candidate for the thematic component of a combined geo-thematic
logic. We show that a weak coupling of DL-Lite with the expressive
region connection calculus RCC8 allows for FOL rewritability under a
spatial completeness condition for the ABox. Stronger couplings allow-
ing for FOL rewritability are possible only for spatial calculi as weak
as the low-resolution calculus RCC2. Already a strong combination of
DL-Lite with the low-resolution calculus RCC3 does not allow for FOL
rewritability.
Keywords: FOL rewritability, region connection calculus, qualitative
spatial reasoning, GIS, combinations
1 Introduction
Query answering over a database becomes far more difficult if the extensional
knowledge in the database is extended by constraints in an ontology. The reason
is that a database plus an ontology may have many different models, hence
ontology based query answering has to compute the answers w.r.t. to all models
and build their intersection (certain answer semantics). But in some cases—when
using a lightweight logic like DL-Lite for the representation of the ontology and
a restricted query language like unions of conjunctive queries—query answering
w.r.t. an ontology can be reduced to model checking. This is formalized by the
notion of FOL (first order logic) rewritability: a given query can be rewritten
into a FOL query in which the intensional knowledge of the ontology is captured.
Though the rewritten queries may become exponentially bigger than the original
queries, there exist optimizations [13]. So, FOL rewritability means a benefit.
DL-Lite per se [2] is not sufficient for use in scenarios of geographic informa-
tion processing, as these demand among others the representation and deduction
over spatial concepts. Though there exists related work combining spatial and
thematic reasoning [4], [15], [6], it is not aimed at FOL rewritability. Hence, there
is still a need for investigating combinations of logics that, on the one hand, are
sufficiently expressive to fit the representation’s needs in geographical informa-
tion processing and that, on the other hand, allow for computationally feasible
(in particular FOL rewritable) satisfiability checking and query answering.
Continuing previous work [7, 8], we investigate combinations of logics in the
DL-Lite family with different members of the region connection calculus (RCC)
family [9], a well-known family of calculi for qualitative spatial reasoning. The
DL-Lite logic we are using as thematic part differs from the known members
of the DL-Lite family as it also allows for concept conjunctions on the left-
hand side of general inclusion axioms. In previous work [8], we focussed on
the FOL rewritability aspects for weak combinations of DL-Lite with RCC8;
these combinations are weak in so far as they do not allow for the construction
of arbitrary RCC8 constraint networks in the intensional part (TBox) of the
ontology. In this paper we focus on strong combinations of DL-Lite with the
weaker fragments RCC3 and RCC2, and prove that DL-Liteu F ,R (RCC3) does
not allow for FOL rewritability of satisfiability checking while the weaker DL-
LiteuF ,R (RCC2) does.
The paper is structured as follows. Section 2 collects technical details on the
region connection calculus and the DL-Lite family of description logics. Weak
combinations of DL-Lite with the region connection calculus are described in
Sect. 3. In Sect. 4, the last section before the conclusion, we consider strong
combinations of DL-Lite with weaker fragments of the region connection calculus.
2 Logical Preliminaries
We recapitulate the main logical notation and concepts used in this paper; the
region connection calculus and DL-Lite.
2.1 The Region Connection Calculus
We will consider different fragments of the region connection calculus [9] as po-
tential candidates for the spatial logic to be combined with DL-Lite. Randell
and colleagues’ axiom system [9] is based on a primitive binary relation C in-
tended to denote a connectedness relation which is specified to be reflexive and
symmetric. On the basis of C other binary relations between regions which are
called base relations are explained. One set of base relations is the set BRCC8 ,
which is the main component of the most expressive region connection calculus
RCC8. The base relations of BRCC8 and their intended meanings are given as
follows: BRCC8 = {DC (disconnected), EC (externally connected), EQ (equal),
PO (partially overlapping), NTPP (non-tangential proper part), TPP (tangen-
tial proper part), NTPPi (inverse of NTPP), TPPi (inverse of TPP)}. We skip
the concrete definitions of the base relations by the connectedness relation C
(see, e.g., [11, p. 45]), as we—in contrast to the axiom system of Randell and
colleagues—consider the following axiom system schema AxRCCi , which directly
specifies the properties of the base relations in BRCCi .
Definition 1 (Axiom system schema AxRCCi ). For all i ∈ {2, 3, 5, 8} the
axiom set AxRCCi contains the following axioms:
W
{∀x, y. Vr∈BRCCi r(x, y)} ∪ (joint exhaustivity)
{∀x, y. r1 ,r2 ∈BRCCi ,r1 6=r2 r1 (x, y) → ¬r2 (x, y)} ∪ (pairwise disjointness)
{∀x, y, z.r1 (x, y) ∧ r2 (y, z) → r31 (x, z) ∨ · · · ∨ r3k (x, z) | r1 ; r2 = {r31 , . . . , r3k }}
(weak composition axioms)
For i ∈ {3, 5, 8} additionally the axiom ∀xEQ(x, x) (reflexivity of EQ) is con-
tained. For i = 2 one has instead the axiom ∀xO(x, x) (reflexivity of O).
In particular, the axioms state the JEPD-property of the base relations (each
pair of regions x, y is related over exactly one base relation) and describe the
(weak) composition of two base relations (denoted by ;) according to the compo-
sition table for RCCi. With the composition of two base relations, in most cases,
only indefinite knowledge of spatial configurations follows. The spatial config-
uration r1 (x, z) ∨ · · · ∨ rn (x, z) for base relations rj in BRCCi is also written
as {r1 , . . . , rn }(x, z), and the set {r1 , . . . , rn } is called a general RCCi relation.
Let Rel RCCi be the set of all 2i general RCCi relations. An RCCi (constraint)
network consists of assertions of the form {r1 , . . . , rn }(x, y).
We mention here the composition table for the low resolution logics RCC2
and RCC3. Their base relations are given by the sets BRCC3 = {DR, EQ, ONE}
and BRCC2 = {DR, O}, and their weak compositions are defined as shown in
Fig. 1. The discreteness relation DR is the same as {DC, EC}, the overlapping-
but-not-equal relation ONE is equal to {PO, NTPP, TPP, NTPPi, TPPi} and the
overlapping relation O is given by {ONE, EQ}.
; DR ONE EQ
; DR O
DR BRCC3 {DR, ONE} DR
DR BRCC2 BRCC2
ONE {DR, ONE} BRCC3 ONE
O BRCC2 BRCC2
EQ DR ONE EQ
Fig. 1. Composition tables for RCC2 and RCC3
Note that in the definitions of the base relations (of RCC3 and RCC2) we
followed the author of [14]. The base relations of the low resolution calculus of
[3] are different from those of RCC2; the authors of [3] consider the two base
relations DC and {EC, O}. But as we do not deal with the exact definitions of
the base relations referring to the connectedness relation C but with the axiom
systems referring to the composition table this difference has no effect—the low
resolution calculus of [3] has the same trivial composition table as RCC2. For
the composition tables of RCC5 and RCC8 have a look at [12, p. 45].
2.2 DL-Lite
The family of DL-Lite description logics [2] is an appropriate candidate for the
thematic component of the envisioned geo-thematic logic as it offers computa-
tionally feasible satisfiability checking and query answering over ontologies and
data stored in a relational database. More concretely, satisfiability checking and
query answering (for unions of conjunctive queries) are first order logic (FOL)
rewritable. In this paper, we will mainly deal with a member of the extended
DL-Lite family which we termed DL-Liteu F ,R , and which allows functional roles,
role hierarchies and role inverses as well as the conjunction of basic concepts on
the left-hand side of GCIs (general concept inclusions). The syntax is given in
Def. 2. The semantics of this logic is defined in the usual way—but imposing the
unique name assumption (UNA).
Definition 2 (DL-Liteu F ,R ). Let RN be the set of role symbols and P ∈ RN ,
CN be a set of concept symbols and A ∈ CN , Const be a set of individual
constants and a, b ∈ Const.
R −→ P | P − B −→ A | ∃R Cl −→ B | Cl u B Cr −→ B | ¬B
TBox∗) : Cl v Cr , (funct R), R1 v R2
ABox: A(a), R(a, b)
*) Restriction: If R occurs in a functionality axiom, then R and its inverse
do not occur on the right-hand side of a role inclusion axiom R1 v R2 .
FOL rewritability also holds for the logic DL-Liteu F ,R which follows from the
corresponding FOL rewritability results for the Datalog extension Datalog± [1].
We assume that the reader is familiar with the notion of FOL queries, conjunctive
queries (CQ) and unions of conjunctive queries (UCQ), their semantics and the
notion of certain answers cert(Q, A ∪ T ) of a query w.r.t. to the union of a
TBox and an ABox T ∪ A [2]. Let DB(A) be the minimal Herbrand model of
A. Checking the satisfiability of ontologies is FOL rewritable iff for all TBoxes
T there is a boolean FOL query QT s.t. for all ABoxes A: the ontology T ∪ A
is satisfiable iff DB(A) 6|= QT . Answering queries from a subclass C of FOL
queries w.r.t. to ontologies is FOL rewritable iff for all TBoxes T and queries
Q = ψ(x) in C there is a FOL query QT such that for all ABoxes A it is the case
DB(A)
that cert(Q, T ∪ A) = QT . For DL-Lite, FOL-rewritability can be proved
w.r.t. to satisfiability as well as w.r.t. answering UCQs [2, Thm 4.14, Thm 5.15].
A crucial part of the proof for FOL rewritability w.r.t. query answering is the
perfect rewriting algorithm [2, Fig. 2]. This algorithm works by using positive
inclusion axioms of the form A1 v A2 as rewriting rules from right to left so
that for example an atom A2 (x) occurring in a CQ would produce a new CQ
containing A1 (x) instead of A2 (x).
3 Weak Combinations of DL-Lite with RCC
In this section, we recapitulate the results concerning a weak coupling of DL-Lite
with the most expressive region connection calculus fragment RCC8, which we
introduced in [7, 8], and provide an example for its use(fulness). This will give us
the opportunity to introduce further concepts that are necessary to understand
the following discussions on stronger couplings of DL-Lite with the weaker region
connection calculi RCC2 and RCC3.
The combination paradigm follows that of Lutz and Miličič [6] who combine
ALC with the RCC8 and, more generally, with ω-admissible concrete domains
[6, Def. 5, p. 7]. The combined logic ALC(RCC8) of [6] is well behaved in so far
as testing concept subsumption is decidable. As we aim at FOL rewritability we
have to be even more careful in choosing the right combination method.
We use an axiom set Tω with corresponding properties of an ω-admissible do-
main for coupling with DL-Lite because axioms are more appropriate for rewrit-
ing investigations. The axiom sets AxRCCi will instantiate Tω .
We recapitulate the syntax and the semantics of the constructors of [6] that
are used for the coupling of the thematic and the spatial domain. A path U (of
length at most 2) is defined as l for a fixed attribute l (“has location”) or as
R ◦ l, the composition of the role symbol R with l. We abbreviate R ◦ l with
R̃ in this paper. The usual notion of an interpretation I in our combined logic
is slightly modified by using two separate domains ∆I and (∆∗ )I . All symbols
of the theory Tω are interpreted relative to (∆∗ )I . Let r be an RCC-relation of
some RCC-fragment. That is, let be given a set of base relations BRCCi and r =
{r1 , . . . rn } ≡ r1 ∨· · ·∨rn for ri ∈ BRCCi . Then lI ⊆ ∆I ×(∆∗ )I ; rI = r1I ∪· · ·∪rnI ;
(R◦l)I ={(d, e∗ ) ∈ ∆I ×(∆∗ )I | there is an e s.t. (d, e) ∈ RI and (e, e∗ ) ∈ lI };
(∃U1 , U2 .r)I ={d ∈ ∆I | there exist e∗1 , e∗2 s.t. (d, e∗1 ) ∈ U1I , (d, e∗2 ) ∈ U2I and
(e∗1 , e∗2 ) ∈ rI }; (∀U1 , U2 .r)I ={d ∈ ∆I | for all e∗1 , e∗2 s.t. (d, e∗1 ) ∈ U1I , (d, e∗2 ) ∈
U2I it holds that (e∗1 , e∗2 ) ∈ rI }.
Now we can define the following combined geo-thematic logic (where a∗ , b∗
stand for constants intended to be interpreted by regions):
Definition 3 (DL-Liteu F ,R (RCC8)). Let r ∈ Rel RCC8 and Tω = AxRCC8 .
−
R −→ P | P U −→ R | R̃ B −→ A | ∃R | ∃l
Cl −→ B | Cl u B Cr −→ B | ¬B | ∃U1 , U2 .r
TBox∗) : Cl v Cr , (funct l), (funct R), R1 v R2
ABox: A(a), R(a, b), l(a, a∗ ), r(a∗ , b∗ )
*) Restriction: If (funct R) ∈ T , then R and R− do not occur on the right-
hand side of a role inclusion axiom or in a concept of the form ∃U1 , U2 .r.
As satisfiability checking of RCC8 constraint networks is NP-complete, there
is only a chance to reach FOL rewritability if we assume within the ABox a
constraint network which is consistent and complete, i.e., only base relations are
allowed as labels; in this case the ABox is called spatially complete. It seems to
us that for cadastral maps or maps containing areas of administration one can
assume pretty safely (almost) spatial completeness. The coupling with RCC8 is
so weak that FOL rewritability of satisfiability follows.
Proposition 1. Checking the satisfiability of DL − Lite u
F ,R (RCC8) ontologies
that have a spatially complete ABox is FOL rewritable.
The FOL rewritability holds also for query rewriting w.r.t. to a restricted
class of treelike queries (termed GCQ+ ). The result is achieved by an adapted
perfect rewriting algorithm PerfectRef [2, Fig. 13].
Theorem 1. Answering GCQ + -queries w.r.t. DL − Lite u F ,R (RCC8) ontologies
that have a spatially complete ABox is FOL rewritable.
DL-Liteu F ,R (RCC8) as well as the logics introduced below are suited for use in
scenarios such as that of an engineering bureau planning additional parks in
a city [7]. Assume, the bureau has stored geographical data in some database
and declares relevant concepts in the TBox: Park+Lake v Park; Park4Playing v
Park; Park+Lake v ∃hasLake◦l, l.TPP; Park4Playing v ∃hasPlAr◦l, l.TPP. The
ABox A is derived virtually by mappings from geographical data in a database.
In particular, assume that {Park+Lake(a), Park4Playing(a)} ⊆ A. According to
A, the object a is a park with a lake and a park with a playing area but its
spatial extension is not known. Now, the engineering bureau asks for all parks
with lakes and playing areas such that the playing area is not contained as island
in the lake. This can be formalized by the GCQ+ query: Q =Park(x)∧∃hasLake◦
l, hasPlAr ◦ l.(BRCC8 \ {NTPP})(x). Using the composition entry TPP; TPPi =
{DC, EC, PO, TPP, TPPi, EQ} ⊆ BRCC8 \ {NTPP}, the reformulation algorithm
produces a UCQ that contains the following CQ: Q0 = (∃hasLake ◦ l, l.TPP)(x) ∧
(∃l, hasPlAr ◦ l.TPPi)(x). Rewriting ∃l, hasPlAr ◦ l.TPPi to ∃hasPlAr ◦ l, l.TPP
in combination with the rewriting rule for A1 v A2 we get another CQ Q00 =
Park+Lake(x) ∧ Park4Playing(x). Now, Q00 captures (as desired) the object a.
4 Strong Combinations of DL-Lite with RCC
Another way of reaching FOL rewritability for combinations of DL-Lite with
RCC is weakening the expressivity of the spatial component. Hence, one may
ask whether a combination with the calculus RCC3 or RCC2 [15], both fragments
with weak expressibility, allows for weak FOL rewritability w.r.t. satisfiability
checks (and query answering). Their potential use as logics for approximating
[5] ontologies in more expressible combined logics like ALC(RCC8) makes the
investigation valuable. The logics DL-Liteu,+ u,+
F ,R (RCC2) and DL-LiteF ,R (RCC3)
are defined as follows (’+’ indicates the strong combination):
Definition 4 (DL-Liteu,+ u,+
F ,R (RCC2) and DL-LiteF ,R (RCC3)). Let Tω =
AxRCC2 resp. Tω = AxRCC3 and r ∈ BRCC2 resp. r ∈ BRCC3
R −→ P | P − U −→ l | R̃ B −→ A | ∃R
Cl −→ B | Cl u B Cr −→ B | ¬B | ∃U1 , U2 .r
TBox∗) : Cl v Cr , (funct l, R), R1 v R2
ABox: A(a), R(a, b), l(a, a∗ ), r(a∗ , b∗ )
*) Restriction: If (funct R) ∈ T , then R and R− do not occur on the right-
hand side of a role inclusion axiom.
For RCC3 the strong combination with DL-Liteu F ,R leads to non-FOL rewrita-
bility. The reason lies in the fact that testing the satisfiability of RCC3 is not in
the complexity class AC0 as shown by the following lemma.
Lemma 1. Checking satisfiability of RCC3 networks is Logspace hard.
Proof. As is known, the reachability problem in symmetric (undirected) graphs is
logspace complete [10]—where graph reachability asks whether for nodes s, t in G
there is a path between s and t. By reducing this problem to the satisfiability test
for RCC3 networks we will have shown that the latter problem is Logspace hard
itself. So let be given a (symmetric) graph G = (V, E) and nodes s, t ∈ V . We
define the network N in the following way (see Figure 2): Let V = {v1 , . . . , vn }
be an enumeration of the nodes of G; w.l.o.g. let s = v1 and t = vn and let
B = BRCC3 . Nodes of N are given by V ∪ {a} where a ∈ / V . Labelled edges of
N are given by: s{DR}a; t{ONE}a; vi {B}a for all i 6= 1, n; vi {EQ}vj if E(vi , vj );
vi {B}vj if ¬E(vi , vj ). Now we show that the network N is satisfiable iff s and t are
!"
)*" B B B +,-"
-4"56"B -4"56"B -4"56"B
/"/"/"
#"$"%&" %." %0" %1(2&3" '"$"%("
Fig. 2. Network N used in proof of Lemma 1
connected in G. Assume that s and t are connected; then there is an EQ-path in N
between them, hence s{EQ}t follows. But this contradicts s{DR}a and t{ONE}a.
Now assume that s and t are not connected; then there is no path consisting only
of EQ-labels between s and t. The graph G consists of at least 2 components, and
s, t are in different components. We define a consistent configuration as follows:
For all nodes v, v 0 in the component in which s is contained, let v{DR}a and
v{EQ}v 0 . For all nodes v, v 0 in the component of t let v{ONE}a and v{EQ}v 0 .
For all nodes v, v 0 in the other components let v{DR}a and v{EQ}v 0 . For all
nodes v, v 0 which have not a label yet, let v{DR}v 0 . (Two remarks : 1) EQ-edges
for edges E(vi , vj ) in G with j > i + 1 are not shown in Fig. 2. 2) We inserted
edges labelled B for better illustrations. But these are not needed.)
This lemma immediately entails the fact that satisfiability checking for on-
tologies over the logic DL-Liteu,+
F ,R (RCC3) is not FOL rewritable. This problem
does not vanish if we presuppose that the ABox A is spatially complete—as
shown by the following proposition.
Proposition 2. Satisfiability checking of ontologies in DL-Liteu,+
F ,R (RCC3) with
spatially complete ABoxes is not FOL rewritable.
Proof. We construct a generic TBox Tg that allows one to encode any RCC3
constraint network so that checking the consistency of RCC3 constraint networks
is reducible to a satisfiability check of this TBox and a spatially complete ABox.
Let for every r ∈ Rel RCC3 be given role symbols Rr1 , Rr2 . The generic TBox Tg
has for every r ∈ Rel RCC3 a concept symbol Ar and a corresponding axiom with
the content that all instances of Ar have paths over the abstract features R1
resp. R2 to regions that are r-related.
Tg = {Ar v ∃R̃r1 , R̃r2 .r, (funct l, Rr1 , Rr2 ) | r ∈ RelRCC3 } (1)
Now, let N be an arbitrary RCC3 constraint network which has to be tested for
relational consistency. Let AN be an ABox such that for every r(a, b) in N three
new constants are introduced: xab , xa , xb .
AN = {Ar (xab ), Rr1 (xab , xa ), Rr2 (xab , xb ) | r(a, b) ∈ N } (2)
The construction entails: Tg ∪ AN ∪ AxRCC3 is satisfiable iff N ∪ AxRCC3 is sat-
u,+
isfiable. If the data complexity of the satisfiability check for DL-LiteF ,R (RCC3)-
0
ontologies were in AC , then the consistency of constraint networks could be
tested in AC0 , too. (Note that Tg is a fixed TBox.) But checking the consistency
of RCC3 constraint networks is Logspace-hard and AC0 ( Logspace.
As a corollary to this proposition we get the assertion that strong combi-
nations of RCC5 and RCC8 into DL-Liteu,+ u,+
F ,R (RCC5) and DL-LiteF ,R (RCC8),
respectively—which are defined in the same manner as in Definition 4—do not
allow for FOL rewritability of satisfiability checking.
The low resolution calculus RCC2 is quite more inexpressive than RCC3
due to the fact that the composition table does not allow for the propagation
of information: All compositions of DR, O result in the maximally unspecified
relation {DR, O}. Hence, FOL rewritability of satisfiability testing follows easily
considering the query Q = ∃x, y[O(x, y) ∧ DR(x, y)] ∨ ∃x[DR(x, x)].
Proposition 3. Testing the satisfiability of RCC2 networks is FOL rewritable.
But in combination with functionality axioms of the TBox one could have the
problem that the ABox may lead to identifications of regions. The identified
regions are not allowed to have edges labelled O, DR resp. to the same region.
Though this can be tested, the problem arises when a chain of regions is identified
by the TBox and the ABox, because we do not know the length of the chain
in advance. More formally: In addition to RCC2 constraint-network assertions
we allow identity assertions v = w for regions v, w. As we can assume that all
nodes in a RCC2 network are connected by an edge labelled O, DR or BRCC2
we use a more intuitive formalism where, for every assertion v = w, the label of
the edge between v and w is marked with an =; e.g., an edge between v, w with
label DR= stands for DR(v, w) ∧ v = w. We call such a network an =-marked
RCC2 network (a RCC= 2 network for short). Let B = BRCC2 in the following.
Proposition 4. An RCC= 2 constraint network N is unsatisfiable iff
1. N contains DR(v, v) or DR= (v, v) for some node v; or
2. N contains DR= (v, w); or
3. N contains a cycle in which there is DR(v, w) and in which there is a path
from v to w such that every label on the path is B = or O= ; or
4. N contains a cycle in which there is DR(v, w) and in which there is a path
from v to w s.t. every label on the path is B = or O= except one which is O.
Proof. Sufficiency of the condition for unsatisfiability is clear. The proof for
necessity is done by induction on the number of =-marked labels. So let be
given a RCC= network N . We may assume, that the network has for every pair
of nodes exactly one labelled edge between; we assume the edges to be undirected
as all relations are symmetric.
Base case: Assume that none of the four conditions hold. As there are no
marked labels, then N unsatisfiability can occur only, if N contains DR(v, v) for
some node v (first condition) or DR(v, w) and O(v, w) (fourth condition). But
these cases are excluded by assumption.
Induction step: Let N contain n marked labelled edges and assume that for
all networks N 0 with n−1 marked labelled edges unsatisfiability of N 0 implies one
of the conditions. Now, assume that for N no one of the four conditions holds.
We have to show that N is satisfiable. Take an arbitrary =-marked labelled edge
between nodes v, w. The label λ of this edge is either O= or B = . We define a
new network N 0 which results as a contraction from N by identifying v and w to
the node z. For N 0 we may assume again that it contains for every pair of nodes
exactly one labelled edge: If in N we have r1 (v, k) and r2 (w, k), then the edge
between z and k in N 0 results as r1 ∩ r2 and is =-marked iff r1 or r2 is marked.
Clearly r1 ∩ r2 is not empty, as otherwise we would have a contradiction to the
fact that N does not fulfill conditions 3 and 4. Clearly N is satisfiable iff N 0 is
satisfiable. Assume to the contrary that N 0 is unsatisfiable. Hence, one of the
four conditions holds for N 0 : 1) Assume N 0 contains DR(v 0 , v 0 ) or DR= (v 0 , v 0 ) for
some node v 0 . If v 0 is not z, then also DR(v 0 , v 0 ) ∈ N resp. DR= (v 0 , v 0 ) ∈ N —
contradicting the fact that N does not fulfill condition 1. Otherwise v 0 = z, but
this cannot be the case either, as there are no self-loops DR(v, v), DR= (v, v),
DR(w, w), DR= (w, w) in N nor DR(v, w) or DR(v, w). 2) Assume N 0 contains
DR= (v 0 , w0 ). If neither v 0 nor w0 is z, this contradicts the fact that N does not
fulfill the 2. condition. Otherwise v 0 = w0 = z, leading to a contradiction with
the fact that N does not fulfill condition 1. 3) Assume N 0 contains a cycle in
which there is DR(v 0 , w0 ) and there is a path from v 0 to w0 such that every label
on the path is B = or O= . The case that the path does not contain z immediately
leads to a contradiction. Otherwise, the path extends to a path in N fulfilling
the 3. condition—contradiction. Similarly, if N 0 fulfills condition 4, the verifying
path can be extended to a path in N fulfilling condition 4—contradiction.
Proposition 4 shows that adding identity assertions to an RCC2 network may
require checking the existence of identity chains of arbitrary length. Hence, in
principle it is possible that the functional roles used in DL-Liteu,+
F ,R (RCC2) may
lead to identity chains. But as we want to show in the following proposition,
this cannot be the case: The identity paths induced by functionalities in DL-
Liteu,+
F ,R (RCC2) can have only a maximal length of one.
Proposition 5. Satisfiability checking of ontologies in DL-Liteu,+
F ,R (RCC2) is
FOL rewritable.
We give a proof sketch. The idea is to find concepts that are unsatisfiable ac-
cording to the TBox (this amounts to constructing the negative closure as in the
proofs for pure DL-Lite [2, Def. 4.7, p. 292]); these are formulated as boolean
queries, and the (finite) disjunctions of these queries is answered over the ABox;
e.g., if A1 v ¬A2 is in the TBox, then the query would contain ∃x(A1 (x)∧A2 (x))
as disjunct. The introduction of concepts of the form ∃U1 , U2 .r enlarges the po-
tential conflicts of a TBox T with an ABox A. So in addition to the FOL queries
that result from the negative closure of the TBox, we have to find queries for
the potential conflicts in the four conditions of Proposition 4. The resulting con-
junctive queries have further to be fed into a perfect rewriting algorithm like
PerfectRef for pure DL-Lite [2] in order to capture the implications of the TBox.
Concerning the first two conditions we have to deal with axioms of the form
B v ∃l, l.DR. If this axiom occurs in the TBox T , then one has to produce
the CQ ∃x.B(x). Similarly, if {B v ∃R̃, R̃.DR, (funct R)} ⊆ T , then the CQ
∃x.B(x) has to be added. Also if {B v ∃R̃1 , R̃2 .DR, (funct R1 , funct R2 )} ⊆
T , then we may get a conflict of the first kind and hence we have to add a
CQ ∃x, y[B(x) ∧ R1 (x, y) ∧ R2 (x, y)]. Concerning the third and fourth condition
we note that this can be only the case if the =-marked paths have maximal
length one. Otherwise we already have a contradiction of the ABox with the
functionality assertions in the TBox. Hence, one considers only the case of pairs
of TBox axioms of the general form A v ∃R̃1 , R̃2 .DR and B v ∃R̃3 , R̃4 .O with
(funct R1 , R2 , R3 , R4 ). In this case we feed also into the PerfectRef algorithm the
CQ ∃x, y, z, w[A(x) ∧ B(y) ∧ R1 (x, z) ∧ R3 (y, z) ∧ R2 (x, w) ∧ R4 (y, w)].
5 Conclusion
As recapitulated in this paper, combining DL-Lite with expressive fragments
of the region calculus like RCC8 into logics that preserve the property of FOL
rewritability is possible if the coupling is weak: Constraints of the RCC8 network
contained in the ABox are not transported over to the implicitly constructed
constraint network resulting from the constructors of the form ∃U1 , U2 .r. In this
paper we mainly dealt with strong combinations for weaker calculi like RCC2
or RCC3. As we have shown by a reduction proof, a strong combination with
RCC3 destroys the FOL rewritability of satisfiability checking. The reason is
that checking the satisfiability of RCC3 networks needs to test for reachability
along EQ paths, which can be reproduced by the TBox. For the low resolution
calculus RCC2, FOL rewritability of satisfiability checking is provable—though
checking the satisfiability of RCC2 networks with additional identity assertions
is at least as hard as checking RCC3 networks. We plan to investigate whether
DL-Liteu,+ u
F ,R (RCC2) and DL-LiteF ,R (RCC8) can be used for approximation—
following the complete but not necessarily correct approximation method of
u,+
[5]. Moreover we want to check whether DL-LiteF ,R (RCC2) allows for FOL
rewritability of query answering w.r.t. unions of conjunctive queries.
References
1. Calı̀, A., Gottlob, G., Lukasiewicz, T.: A general datalog-based framework for
tractable query answering over ontologies. Technical Report CL-RR-10-21, Oxford
University Computing Laboratory (November 2010)
2. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Poggi, A., Rodrı́guez-
Muro, M., Rosati, R.: Ontologies and databases: The DL-Lite approach. In: Tes-
saris, S., Franconi, E. (eds.) Semantic Technologies for Informations Systems – 5th
Int. Reasoning Web Summer School (RW-2009), LNCS, vol. 5689, pp. 255–356.
Springer (2009)
3. Grigni, M., Papadias, D., Papadimitriou, C.H.: Topological inference. In: IJCAI
(1). pp. 901–907 (1995)
4. Haarslev, V., Lutz, C., Möller, R.: A description logic with concrete domains and
a role-forming predicate operator. J. Log. Comput. 9(3), 351–384 (1999)
5. Kaplunova, A., Moeller, R., Wandelt, S., Wessel, M.: Towards scalable instance
retrieval over ontologies. In: Yaxin, B., Mary-Anne, W. (eds.) Knowledge Science,
Engineering and Management, Fourth International Conference, KSEM 2010, Pro-
ceedings. Lecture Notes in Computer Science, vol. 6291. Springer (2010)
6. Lutz, C., Miličić, M.: A tableau algorithm for description logics with concrete
domains and general TBoxes. J. Autom. Reasoning 38(1-3), 227–259 (2007)
7. Özçep, O.L., Möller, R.: Computationally feasible query answering over spatio-
thematic ontologies. In: Proceedings of GEOProcessing 2012, The Fourth Inter-
national Conference on Advanced Geographic Information Systems, Applications,
and Services (2012), available online at http://www.thinkmind.org/index.php?
view=article&articleid=geoprocessing_2012_7_10_30059
8. Özçep, Ö.L., Möller, R.: Scalable geo-thematic query answering. Technical report,
Institute for Softwaresystems (STS), Hamburg University of Technology (2012),
available online at http://www.sts.tu-harburg.de/tech-reports/papers.html
9. Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection.
In: Proceedings of the 3rd International Conferecence on Knowledge Representa-
tion and Reasoning. pp. 165–176 (1992)
10. Reingold, O.: Undirected connectivity in log-space. J. ACM 55(4), 17:1–17:24 (Sep
2008), http://doi.acm.org/10.1145/1391289.1391291
11. Renz, J.: Qualitative Spatial Reasoning with Topological Information, Lecture
Notes in Computer Science, vol. 2293. Springer (2002)
12. Renz, J., Nebel, B.: Qualitative spatial reasoning using constraint calculi. In: Aiello,
M., Pratt-Hartmann, I., Benthem, J. (eds.) Handbook of Spatial Logics, pp. 161–
215. Springer Netherlands (2007)
13. Rodriguez-Muro, M., Calvanese, D.: Semantic index: Scalable query answering
without forward chaining or exponential rewritings. In: Posters of the 10th Int.
Semantic Web Conf. (ISWC 2011) (2011)
14. Wessel, M.: On spatial reasoning with description logics - position paper. In:
Ian Horrocks, S.T. (ed.) Proceedings of the International Workshop on Description
Logics (DL-2002). CEUR Workshop Proceedings, vol. 53 (2002), http://CEUR-
WS.org/Vol-53/
15. Wessel, M.: Qualitative spatial reasoning with the ALCI RCC - family — first results
and unanswered questions. Technical Report FBI–HH–M–324/03, University of
Hamburg, Department for Informatics (2003)