First order logic (FOL) rewritability is a desirable feature for query answering over geo-thematic ontologies because in most geoprocessing scenarios one has to cope with large data volume. Hence, there is a need for combined geo-thematic logics that provide a sufciently 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 suitable 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 allowing 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.
Query answering over a database becomes far more di cult 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 di erent 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 ( rst 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 [
DL-Lite per se [
Continuing previous work [
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
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 di erent fragments of the region connection calculus [
De nition 1 (Axiom system schema AxRCCi). For all i 2 f2; 3; 5; 8g the axiom set AxRCCi contains the following axioms: ff88xx;; yy:: VWrr12;Br2R2CBCRiCrC(ix;r;1y6=)rg2[r1(x; y) ! :r2(x; y)g [ (pai(rjwoiinset edxishjaouinsttinveistys)) f8x; y; z:r1(x; y) ^ r2(y; z) ! r31(x; z) _ _ r3k(x; z) j r1; r2 = fr31; : : : ; r3kgg (weak composition axioms) For i 2 f3; 5; 8g additionally the axiom 8xEQ(x; x) (re exivity of EQ) is contained. For i = 2 one has instead the axiom 8xO(x; x) (re exivity 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 composition table for RCCi. With the composition of two base relations, in most cases, only inde nite knowledge of spatial con gurations follows. The spatial con guration r1(x; z) _ _ rn(x; z) for base relations rj in BRCCi is also written as fr1; : : : ; rng(x; z), and the set fr1; : : : ; rng 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 fr1; : : : ; rng(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 = fDR; EQ; ONEg and BRCC2 = fDR; Og, and their weak compositions are de ned as shown in Fig. 1. The discreteness relation DR is the same as fDC; ECg, the overlappingbut-not-equal relation ONE is equal to fPO; NTPP; TPP; NTPPi; TPPig and the overlapping relation O is given by fONE; EQg.
; DR O DR BRCC2 BRCC2 O BRCC2 BRCC2
; DR DR BRCC3 ONE fDR; ONEg EQ DR
Note that in the de nitions of the base relations (of RCC3 and RCC2) we
followed the author of [
De nition 2 (DL-LiteuF;R). Let RN be the set of role symbols and P 2 RN , CN be a set of concept symbols and A 2 CN , Const be a set of individual constants and a; b 2 Const .
R ! P j P B ! A j 9R Cl ! B j Cl u B Cr ! B j :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-LiteuF;R which follows from the
corresponding FOL rewritability results for the Datalog extension Datalog [
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 [
The combination paradigm follows that of Lutz and Milicic [
We use an axiom set T! with corresponding properties of an !-admissible domain for coupling with DL-Lite because axioms are more appropriate for rewriting investigations. The axiom sets AxRCCi will instantiate T!.
We recapitulate the syntax and the semantics of the constructors of [
Now we can de ne the following combined geo-thematic logic (where a ; b stand for constants intended to be interpreted by regions): De nition 3 (DL-LiteuF;R(RCC8)). Let r 2 Rel RCC8 and T! = AxRCC8.
R ! P j P U ! R j R~ B ! A j 9R j 9l Cl ! B j Cl u B Cr ! B j :B j 9U1; 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) 2 T , then R and R do not occur on the righthand side of a role inclusion axiom or in a concept of the form 9U1; U2:r.
As satis ability 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 satis ability follows.
Proposition 1. Checking the satis ability of DL LiteuF;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 LiteuF;R(RCC8) ontologies that have a spatially complete ABox is FOL rewritable.
DL-LiteuF;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 [
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 [
R ! P j P U ! l j R~ B ! A j 9R Cl ! B j Cl u B Cr ! B j :B j 9U1; 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) 2 T , then R and R do not occur on the righthand side of a role inclusion axiom.
For RCC3 the strong combination with DL-LiteuF;R leads to non-FOL rewritability. The reason lies in the fact that testing the satis ability of RCC3 is not in the complexity class AC0 as shown by the following lemma.
Lemma 1. Checking satis ability of RCC3 networks is Logspace hard.
Proof. As is known, the reachability problem in symmetric (undirected) graphs is
logspace complete [
B
B -4"56"B #"$"%&"
-4"56"B %." %0"
B /"/"/" +,-"
-4"56"B %1(2&3" '"$"%(" connected in G. Assume that s and t are connected; then there is an EQ-path in N between them, hence sfEQgt follows. But this contradicts sfDRga and tfONEga. 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 di erent components. We de ne a consistent con guration as follows: For all nodes v; v0 in the component in which s is contained, let vfDRga and vfEQgv0. For all nodes v; v0 in the component of t let vfONEga and vfEQgv0. For all nodes v; v0 in the other components let vfDRga and vfEQgv0. For all nodes v; v0 which have not a label yet, let vfDRgv0. (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 satis ability checking for ontologies over the logic DL-LiteuF;;+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. Satis ability checking of ontologies in DL-LiteuF;;+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 satis ability check of this TBox and a spatially complete ABox. Let for every r 2 Rel RCC3 be given role symbols Rr1; Rr2. The generic TBox Tg has for every r 2 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 = fAr v 9R~r1; R~r2:r; (funct l; Rr1; Rr2) j r 2 RelRCC3g (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 = fAr(xab); Rr1(xab; xa); Rr2(xab; xb) j r(a; b) 2 N g (2) The construction entails: Tg [ AN [ AxRCC3 is satis able i N [ AxRCC3 is satis able. If the data complexity of the satis ability check for DL-Liteu;+ (RCC3)F;R ontologies were in AC0, then the consistency of constraint networks could be tested in AC0, too. (Note that Tg is a xed 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 combinations of RCC5 and RCC8 into DL-LiteuF;;+R(RCC5) and DL-LiteuF;;+R(RCC8), respectively|which are de ned in the same manner as in De nition 4|do not allow for FOL rewritability of satis ability 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 unspeci ed relation fDR; Og. Hence, FOL rewritability of satis ability testing follows easily considering the query Q = 9x; y[O(x; y) ^ DR(x; y)] _ 9x[DR(x; x)]. Proposition 3. Testing the satis ability 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 identi cations of regions. The identi ed 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 identi ed 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 unsatis able i 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. Su ciency of the condition for unsatis ability 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 unsatis ability can occur only, if N contains DR(v; v) for some node v ( rst 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 unsatis ability 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 satis able. Take an arbitrary =-marked labelled edge between nodes v; w. The label of this edge is either O= or B=. We de ne 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 i 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 ful ll conditions 3 and 4. Clearly N is satis able i N 0 is satis able. Assume to the contrary that N 0 is unsatis able. Hence, one of the four conditions holds for N 0: 1) Assume N 0 contains DR(v0; v0) or DR=(v0; v0) for some node v0. If v0 is not z, then also DR(v0; v0) 2 N resp. DR=(v0; v0) 2 N | contradicting the fact that N does not ful ll condition 1. Otherwise v0 = 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=(v0; w0). If neither v0 nor w0 is z, this contradicts the fact that N does not ful ll the 2. condition. Otherwise v0 = w0 = z, leading to a contradiction with the fact that N does not ful ll condition 1. 3) Assume N 0 contains a cycle in which there is DR(v0; w0) and there is a path from v0 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 ful lling the 3. condition|contradiction. Similarly, if N 0 ful lls condition 4, the verifying path can be extended to a path in N ful lling 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-LiteuF;;+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 DLLiteuF;;+R(RCC2) can have only a maximal length of one.
Proposition 5. Satis ability checking of ontologies in DL-LiteuF;;+R(RCC2) is FOL rewritable.
We give a proof sketch. The idea is to nd concepts that are unsatis able
according 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 ( nite) disjunctions of these queries is answered over the ABox;
e.g., if A1 v :A2 is in the TBox, then the query would contain 9x(A1(x)^A2(x))
as disjunct. The introduction of concepts of the form 9U1; U2:r enlarges the
potential con icts 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 nd queries for
the potential con icts in the four conditions of Proposition 4. The resulting
conjunctive queries have further to be fed into a perfect rewriting algorithm like
PerfectRef for pure DL-Lite [
Concerning the rst two conditions we have to deal with axioms of the form B v 9l; l:DR. If this axiom occurs in the TBox T , then one has to produce the CQ 9x:B(x). Similarly, if fB v 9R~; R~:DR; (funct R)g T , then the CQ 9x:B(x) has to be added. Also if fB v 9R~1; R~2:DR; (funct R1; funct R2)g T , then we may get a con ict of the rst kind and hence we have to add a CQ 9x; 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 9R~1; R~2:DR and B v 9R~3; R~4:O with (funct R1; R2; R3; R4). In this case we feed also into the PerfectRef algorithm the CQ 9x; y; z; w[A(x) ^ B(y) ^ R1(x; z) ^ R3(y; z) ^ R2(x; w) ^ R4(y; w)]. 5
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 9U1; 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 satis ability checking. The reason is
that checking the satis ability 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 satis ability checking is provable|though
checking the satis ability of RCC2 networks with additional identity assertions
is at least as hard as checking RCC3 networks. We plan to investigate whether
DL-LiteuF;;+R(RCC2) and DL-LiteuF;R(RCC8) can be used for approximation|
following the complete but not necessarily correct approximation method of
[