=Paper=
{{Paper
|id=Vol-1577/paper_32
|storemode=property
|title=Reasoning About General TBoxes with Spatial and Temporal Constraints: Implementation and Optimizations
|pdfUrl=https://ceur-ws.org/Vol-1577/paper_32.pdf
|volume=Vol-1577
|authors=Matthias Hengel,Sefan Wölfl,Bernhard Nebel
|dblpUrl=https://dblp.org/rec/conf/dlog/HengelWN16
}}
==Reasoning About General TBoxes with Spatial and Temporal Constraints: Implementation and Optimizations==
https://ceur-ws.org/Vol-1577/paper_32.pdf
Reasoning about general TBoxes with spatial and
temporal constraints: Implementation and optimizations
Matthias Hengel, Stefan Wölfl, and Bernhard Nebel
Department of Computer Science, University of Freiburg,
Georges-Köhler-Allee 52, 79110 Freiburg, Germany
{hengelm,woelfl,nebel}@informatik.uni-freiburg.de
Abstract. In many applications a reasonable representation of conceptual knowl-
edge requires the possibility to express spatial or temporal relations between do-
main entities. A feasible approach to this is to consider spatial or temporal con-
straint systems on concrete domains. Indeed, Lutz and Miličic̀ (2007) showed that
for the description logic ALC(C) with ω-admissible constraint systems, concept
satsifiability with respect to general TBoxes can be decided by an extension of a
standard ALC tableau algorithm. In this paper we report on a study in which this
tableau method was implemented, optimized, and evaluated.
1 Introduction
When an application domain is to be conceptualized in terms of a terminological knowl-
edge base, it is often necessary to refer to spatial or temporal relations between domain
entities. Examples include domains dealing with legal concepts (such as traffic laws,
building legislation, etc.), architectural domains, and domains concerned with spatial
layouts. At first glance it seems suggesting to use spatial and temporal relations as
roles in description logic TBoxes, but a series of undecidability results (see, e.g., [21])
lead to a different approach in which such relations are handled as constraints on con-
crete spatial or temporal domains (see, e.g., [2, 10]). This concrete domain approach
may result in undecidable reasoning problems (in particular if one allows for general
concept inclusions, see, e.g., [10]), but Lutz and Miličic̀ [11] showed that so-called ω-
admissible constraint systems on concrete domains allow for deciding consistency of
general TBoxes in the description logic ALC(C). In particular, they presented a tableau
algorithm and stated that the algorithm is a first step towards an efficient implementation
of description logics with constraint systems on concrete domains.
In this paper we present the first implementation of this tableau procedure.1 In par-
ticular, we are interested in the question which of the standard optimization techniques
used in current description logic reasoners [7] can be used in a reasoner for ALC(C). We
show that techniques such as lazy unfolding and absorption can be effortlessly applied
1 Note that serveral DL-reasoners support concrete domain reasoning (see, e.g., [19, 17, 16],
but to our knowledge, there is currently no reasoner that supports reasoning with constraint
systems on concrete domains. Furthermore there has been some work on integrating spatial
reasoning into description logics using a hybrid approach [5, 18].
within a concrete domain DL-reasoner, while other techniques such as dependency-
directed backtracking and caching need careful adaptations.
A second source for optimizations are special techniques that arise from interweav-
ing tableau reasoning and constraint-based reasoning. For example, spatial and tem-
poral constraint-based formalisms such as RCC8 [13] and Allen’s interval algebra [1]
typically allow for disjunctive constraints. Since such constraints can be handled by
constraint solvers for these languages, it makes sense to delegate reasoning steps.
The setup of the paper is as follows: In section 2, we provide the necessary back-
ground on the description logic ALC(C) as well as the tableau procedure for ALC(C)
as presented in [11]. In section 3, we discuss which standard tableau optimization
techniques can be adapted to the ALC(C)-tableau procedure and also the above men-
tioned special techniques that improve the processing of disjunctive constraints. In sec-
tion 4, we report on the results of an empirical evaluation of our implementation of the
ALC(C)-tableau procedure, showing the influence of the different optimization tech-
niques. Since there are no knowledge bases yet that use this particular language, we
have to generate synthetic test cases. However, the structure of our test cases tries to
mimic the structure of existing KBs. Section 5 concludes the paper.
2 Background
In what follows we introduce the technical background in a rather condensed way. For
a more detailed presentation we refer to [11]. Furthermore we assume that the reader is
familiar with the description logic ALC [15].
Constraint systems. A constraint system on a concrete domain D is a finite set Γ of
binary relations on D. Usually the relations in the constraint system are assumed to be
jointly exhaustive and pairwise disjoint. Given a constraint system Γ , its disjunctive
closure Γ ∨ is the set of all relations that are unions of relations in Γ . We write relations
from Γ ∨ in the form r1 ∨ · · · ∨ rn with ri ∈ Γ (1 ≤ i ≤ n). A constraint, then, is an
expression of the form (v r v0 ) where r is a relation from the disjunctive closure of
Γ and v and v0 are variables from a countably infinite set of variables. A constraint
network N is a finite or infinite set of constraints (we use the symbol VN to denote to
the set of all variables mentioned in N). Given network N and some subset V 0 ⊆ VN ,
N|V 0 is the set of all constraints in N that mention variables from V 0 only. We will
assume that networks contain at most one constraint (v r v0 ) for each pair of variables
v, v0 . If a network contains exactly one constraint for each variable pair, it is called
complete. A network is called atomic if all its constraints use only relations from the
basic constraint system (i.e., it uses no relation from Γ ∨ \ Γ ). A network N is called
satisfiable if there exists a mapping a that assigns to each variable in VN an element of
the concrete domain such that for each constraint (v r v0 ) in N, it holds (a(v), a(v0 )) ∈ r.
The variable assignment a is then called a solution of the network. A network N is
called a refinement of network N 0 if for each constraint (v r v0 ) in N, if N 0 contains a
constraint of the form (v r0 v0 ) then r ⊆ r0 (i.e., each relation r j ∈ Γ mentioned in r is
also mentioned in r0 ).
Examples of constraint systems include Allen’s interval calculus [1], which consists
of 13 relations describing all possibilities how in a linear flow of time the start- and
endpoints of two intervals can be related to each other. Another example is the fragment
RCC8 of the Region Connection Calculus [13] with 8 relations describing topological
relations between extended spatial regions. For further examples as well as for basic
algorithms used to decide the satisfiability of such constraint networks, we refer to
[14].
A constraint system is said to have the compactness property if for each infinite
network N, N is satisfiable if and only if for each finite subset V 0 ⊆ VN the network
N|V 0 is satisfiable. It is said to have the patchwork property if for any pair of finite,
atomic, complete, and satisfiable networks N and N 0 that coincide on all constraints with
variables from VN ∩VN 0 , the network N ∪ N 0 is satisfiable. Finally, the constraint system
is called ω-admissible if it has both the compactness and the patchwork property and
furthermore, there exists a procedure that decides the satisfiability of finite networks.
Note that both Allen’s interval calculus and RCC8 feature ω-admissibility [11].
ALC(C). In what follows let C = hD,Γ i be a fixed ω-admissible constraint system.
The vocabulary of the description logic ALC(C) is given by countably infinite sets
of concept names (A, A0 , A1 , . . . ), role names (R, R0 , R1 , . . . ) with an infinite subset of
abstract features, and concrete features (g, g0 , g1 , . . . ). A path is a sequence R1 . . . Rk g
consisting of role names Ri and a single concrete feature g. A feature path is a path
R1 . . . Rk g, where all role names Ri are abstract features. The concepts of ALC(C) are
formed by the following rule:
C ::= A | ¬C | C uC0 | C tC0 | ∃R.C | ∀R.C | ∃U1 ,U2 .r | ∀U1 ,U2 .r
with r ∈ Γ ∨ . In the constraint constructors ∃U1 ,U2 .r and ∀U1 ,U2 .r we allow the fol-
lowing two situations: (a) both U1 and U2 are feature paths or (b) both have length ≤ 2,
i.e., they have the form Ui = Rgi or Ui = gi (i = 1, 2)). A general concept inclusion is an
expression of the form C v C0 where C and C0 are arbitrary ALC(C)-concepts. Finally,
a general TBox is a finite set of general concept inclusions.
We use a descriptive set-based semantics: An interpretation I is a tuple (∆I , ·I ),
where ∆I is called the domain and ·I the interpretation function. The interpretation
function maps each abstract feature f to a partial function from ∆I to ∆I , and each
concrete feature g to a partial function from ∆I to the concrete domain D. For pure
ALC-concepts we use the ordinary semantics as given in [15]. The interpretation func-
tion is then extended to arbitrary ALC(C)-concepts as follows:
(∃U1 ,U2 .r)I := {x ∈ ∆I : ∃d1 ∈ U1I (x), d2 ∈ U2I (x) with hD,Γ i |= (d1 r d2 )}
(∀U1 ,U2 .r)I := {x ∈ ∆I : ∀d1 ∈ U1I (x), d2 ∈ U2I (x), it holds hD,Γ i |= (d1 r d2 )},
In these conditions we use the following notations: hD,Γ i |= (d1 r d2 ) means (d1 , d2 ) ∈
ri for some 1 ≤ i ≤ n (where r = r1 ∨ · · · ∨ rn ); and for a path U = (R1 . . . Rk g), U I (x) is
defined as:
U I (x) := {d ∈ ∆I : ∃x1 , . . . , xk+1 ∈ ∆I , such that x = x1 , gI (xk+1 ) = d,
and (x j , x j+1 ) ∈ RIj for 1 ≤ j ≤ k, }.
Example 1. In the language ALC(C) with the Allen interval constraints, we can for
example define the concept of time-travelling father, i.e., a father that is not born before
the lifetime of some of his children. Using the role name has-child, the concrete
feature has-lifetime, and the usual notation for interval relations: s (‘starts’), d
(‘during’), f (‘finishes’), = (‘equals’), > (‘after’), mi (converse of ‘meets’), oi (converse
of ‘overlaps’), and si (converse of ‘starts’), we can define:
Timetravelling Father = Man u
∃(has-lifetime), (has-child has-lifetime).(s∨d∨f∨=∨>∨mi∨oi∨si)
Tableau algorithm. Lutz and Miličic̀ [11] present a tableau algorithm to decide the
satisfiability of a concept C w.r.t. a general TBox T (i.e., the problem if there exists an
interpretation that satisfies the concept inclusions in the TBox and assigns to C a non-
empty set). The idea of the algorithm is to construct a ‘pre-model’ step-by-step such
that in each step all concrete domain constraints are satisfied. The non-deterministic
algorithm builds up a tree with two different kinds of nodes: abstract nodes representing
individuals in the domain ∆I and concrete nodes representing variables for concrete
domain values. Constraints between the concrete nodes are represented by a constraint
network N , which initially is the empty network and which is updated as the algorithm
proceeds.
The algorithm starts by creating a single abstract node a labeled with a set contain-
ing the concept to be checked (the label set of node a is denoted by L(a)). The label
sets are then expanded by applying the tableau rules on the contained concepts. Where
needed, abstract successors (nodes corresponding to role successors) and concrete suc-
cessors (nodes for concrete feature fillers) are created. Successors are labeled as well as
the edges linking parents to successors (with role names or concrete features, resp.).
The algorithm expects both the concept to be checked and the TBox to be in path
normal form, i.e. to be in negation normal form such that every path has length at most
two. In [11] it is shown that concept satisfiability w.r.t. general TBoxes can be reduced
in polynomial time to satisfiability of concepts in path normal form w.r.t. TBoxes in
path normal form.
For pure DL concepts like concept conjunctions, concept disjunctions and role re-
strictions the standard tableau rules (Ru), (Rt), (R∃), (R∀) and (RTBox) are used. In
addition to these, the algorithm uses the rules listed in Table 1.
To guarantee termination, the algorithm uses a static blocking mechanism that con-
siders the concrete neighborhood of abstract nodes. The concrete neighborhood of an
abstract node a is defined as the set
N (a) := {(v r v0 ) ∈ N : ∃g, g0 ∈ feat(a) such that
v g-successor of a and v0 g0 -successor of a},
where feat(a) denotes the set of all concrete features g such that a has g-successors.
A node a is potentially blocked by node b if b is an ancestor of a, L(a) ⊆ L(b),
and feat(a) = feat(b). Node a is directly blocked by b if a is potentially blocked by b,
the concrete neighborhoods N (a) and N (b) are atomic and complete, and the mapping
Table 1. Subset of the tableau rules for ALC(C). a and b refer to abstract nodes in the constructed
completion system, N to the constructed constraint network. The presentation here is slightly
simplified. For details and a complete list of rules see [11].
R∃c If ∃U1 ,U2 .r ∈ L(a), r = r1 ∨ · · · ∨ rn , a is not blocked, and there exist no
variables v1 , v2 in N such that v j is a U j -successor of a for j = 1, 2 and
(v1 ri v2 ) ∈ N for some i with 1 ≤ i ≤ n, then add ‘fresh’ U1 - and U2 -successors
v1 and v2 , resp., and set N := N ∪ {(v1 ri v2 )} for some i with 1 ≤ i ≤ n.
R∀c If ∀U1 ,U2 .r ∈ L(a), r = r1 ∨ · · · ∨ rn , a is not blocked, and there are variables
v1 , v2 in N such that v j is a U j -successor of a for j = 1, 2 but (v1 ri v2 ) ∈
/ N for
each i with 1 ≤ i ≤ n, then set N := N ∪ {(v1 ri v2 )} for some i with 1 ≤ i ≤ n.
RNet If a is potentially blocked by b or vice versa, and N (a) is not complete and
atomic, then non-deterministically guess an atomic completion N 0 of N (a) and
set N := N ∪ N 0 .
from VN (a) to VN (b) induced by assigning to every unique g-successor of a the unique
g-successor of b is an isomorphism. A node a is blocked if it or one of its ancestors is
directly blocked. On blocked nodes no rule may be applied.
Crucial is the rule (RNet). This rule must be applied before any other rule in or-
der to resolve any potential blocking situation to either a non-blocking or a blocking
situation. The rule is used to guess a complete and atomic refinement of the concrete
neighborhood of an abstract node a.
The non-deterministic algorithm returns unsatisfiable if a ‘guessed’ completion step
yields a clash: A clash can arise on the part of DL (e.g. A and ¬A are in a label) or on
the part of the concrete domain (the constructed network is unsatisfiable). The algorithm
terminates and returns satisfiable if no rule can be applied anymore and no clash is in
the guessed completion.
To obtain a model from the ‘pre-model’ constructed by the algorithm, that part of
the ‘pre-model’ that links the blocked node and its blocking node is ‘glued’ together
infinitely often. In the case of ALC(C), compactness and the patchwork property are
needed to ensure that the so constructed infinite network still is satisfiable. The tableau
algorithm runs in 2-NE XP T IME if satisfiability of the concrete domains is in NP [11].
To the best of our knowledge no tighter complexity results are known.
3 Optimizations
Optimizations are essential to gain acceptable runtimes of the tableau algorithm. In [7,
8] several techniques for optimizing satisfiability checking using a tableau algorithm
are described. We adapt these techniques, where possible, to our case and additionally
propose some techniques which generalize the ideas behind the fragment of ALC(C)
described in [11].
3.1 Standard techniques
The idea of lazy unfolding is to keep the structure of the knowledge base as long as
possible [3]. It works by only introducing axioms which are relevant for the current
label. For example, an axiom A v C is only relevant to a label already containing A.
It is easy to see that lazy unfolding is applicable in the context of ALC(C) without
restriction: as described for example in [7], general TBoxes may be separated in an
unfoldable part, which is handled by lazy unfolding, and a non-unfoldable part, handled
by (RTBox).
Absorption [3] is used to reduce the number of general concept inclusions in a
knowledge base. The idea is to replace general concept inclusions, where possible, by
primitive definition axioms, which in a next step may be merged further on. Since this
standard technique can be implemented by just considering operations on the label sets
of abstract nodes, it is quite clear to see that absorption is applicable to our case without
any restriction.
Backjumping [8] is a dependency-directed backtracking scheme used to reduce the
number of branches expanded during search. It works by identifying the cause behind a
clash and using this information to safely ignore branches. Backjumping can be applied
to ALC without any restrictions, but for application to a concrete domain it is nec-
essary to identify the cause of concrete clashes in detail [20]. As our implementation
(as described in the next section) uses an external constraint solving library, we per-
form backjumps only when clashes on the DL part are discovered. When clashes on the
part of the constraint reasoner are discovered, we use the chronological backtracking
scheme.
Caching [8] is a technique that aims at avoiding recomputations. If a node a of a
tableau with starting label L(a) has been discovered to be satisfiable and later in the
execution of the algorithm another node a0 with L(a0 ) = L(a) is created, the idea is
to not further expand a0 but to reuse the result of the completion of a instead. This
works for ALC, as the satisfiability of a node a is independent of the satisfiability of its
parent node b once b is completely expanded. But this is not the case in ALC(C), as the
following example shows.
Example 2. Let R be an abstract feature (i.e. R is functional) and T be the following
TBox:
A v ∃R.(∃(loc1 ), (loc2 ).(>)) u ∃(loc1 ), (R loc1 ).(=) u ∃(loc2 ), (R loc2 ).(=),
B v ∃(loc1 ), (loc2 ).(<) u ∃(loc1 ), (R loc1 ).(=) u ∃(loc2 ), (R loc2 ).(=) u ∀R.A.
Concept A is satisfiable, as Figure 1 (left) shows. On the other hand, if this information
is used while checking B, the algorithm returns that B is satisfiable, which is wrong, as
can be seen in Figure 1 (right).
The problem is caused by the fact that the satisfiability of parts of a constraint net-
work in general does not imply the satisfiability of the whole network. For this reason
it is necessary to not only cache the label set, but also its concrete neighborhood.
Another problem arises from the fact that for a node a and a parent node b of a
the application of a rule on a may trigger the application of a ∀-rule on b. For example
consider a node a with
L(a) = {∃(loc1 ), (loc1 ).(=) u ∃(loc2 ), (loc2 ).(=)}.
B
R
A
A
R <
R
= =
∃(loc1 ), (loc2 ).(>) ∃(loc1 ), (loc2 ).(>)
= = = =
> >
Fig. 1. Checking of concepts A (left) and B (right) of Example 1. The symbols and denote
the concrete feature successors w.r.t. loc1 and loc2 , resp.
and a parent node b of a connected by abstract feature R with
L(b) = {∀(R loc1 ), (R loc2 ).(ntpp)}.
Then, only if a is completely expanded (the concrete successors are generated), the ∀-
rule can be applied on L(b), i.e. the parent influences the concrete neighborhood of the
child node. Our solution to this problem is to completely expand a node a and its parent
node b before caching or loading the result for a.
Thus we restrict caching in our case in the two following ways:
– Only nodes that have an atomic and complete concrete neighborhood may be used
for caching.
– Every node must be completely expanded before it is cached or used for loading of
cached results.
This kind of caching is not as effective as caching for ALC, because less nodes may
be cached or loaded, and more rules must be applied before a node is considered for
loading of a cached result.
3.2 Special techniques
In addition to these standard techniques, we use two optimizations tailored towards the
usage of a constraint systems with general TBoxes. Both are suggested in [11] to be
used in a particular fragment of ALC(C), but we discuss how one can use these in the
general case.
Patchwork property revisited. In the original version of the algorithm in [11], the
constructed constraint networks are atomic. As this requires to non-deterministically
guess a relation for every disjunctive constraint, we will make use of a reformulation of
the patchwork property (cp. [11]) to allow for disjunctive constraints in the constructed
constraint network:
Lemma 1. Let C = hD,Γ i be a constraint system. Then the following statements are
equivalent:
(i) C has the patchwork property.
(ii) For any finite networks N and N 0 such that N|VN ∩VN 0 = N 0 |VN ∩VN 0 and N|VN ∩VN 0
is atomic and complete, if both N and N 0 are satisfiable, then so is the network
N ∪ N0.
Notice the difference between statements (i) and (ii) of the lemma. Condition (ii)
does not require the networks N and N 0 to be atomic and complete. This allows to
refine networks to atomic networks only for concrete neighborhoods of potentially
blocked nodes,i.e., the non-deterministic rules R∃c and R∀c can be replaced by de-
terministic versions that do not refine disjunctive constraints to atomic ones. The ra-
tionale here is that a constraint solver may handle disjunctive networks substantially
faster than the non-optimized tableau algorithm. In particular the constraint solver can
use search heuristics as well as tractability information of fragments of the constraint
system. These techniques are not available on the part of the tableau reasoner, when
constraint techniques are delegated to an external library. (This, by the way, is also the
reason why the more general patchwork properties discussed in [9] can not be used in
our setting).
Furthermore, since the network constructed during the tableau procedure needs to
be checked for satisfiability after each step modifying the network, we can improve
these checks by considering only that part of the network where a change occurs. The
idea is to split the network into two parts that coincide on the concrete neighborhood of
an abstract node (given that the concrete neighborhood is atomic and complete).
Definition 1. Let (T, N ) be a state in the tableau procedure, i.e., T is some tree of
abstract nodes and N the constructed constraint network. Let a be an abstract node.
The succeeding network of a is defined by:
Ns (a) := {(v r v0 ) ∈ N : there are concrete features g, g0 s.t. v is g-successor of
some abstract node b, v0 is g0 -successor of some abstract node b0 where
b and b0 are successors of, or identical to, a }
The preceding network of a is defined by:
N p (a) := {(v r v0 ) ∈ N : there are concrete features g, g0 s.t. v is g-successor of
some abstract node b, v0 is g0 -successor of some abstract node b0 , and b
and b0 are not successors of a }
Lemma 2. In the situation of Definition 1, it holds:
(a) N = Ns (a) ∪ N p (a);
(b) Ns (a) ∩ N p (a) = N (a);
(c) Ns (a)|VNs (a) ∩VN p (a) = N p (a)|VNs (a) ∩VN p (a) .
Example 3. We consider the situation in Figure 2. The concrete neighborhood of node
b is atomic and complete (notice that each concrete node is related to itself via the iden-
tity relation). The preceding network is given by the relations r1 , r2 , r4 , r7 and r8 , the
a
b d
r2 r8
r7
r1
c r4
r5
r6
r3
Fig. 2. Situation of Example 3. The symbols and represent different concrete features. The
figure shows the preceding and succeeding networks of node b.
succeeding network by the relations r3 , r5 and r6 . By Lemmas 1 and 2 the satisfiabil-
ity of both the preceding and succeeding network ensures that the whole network is
satisfiable.
By these lemmas it suffices at abstract nodes with a concrete neighborhood that
is atomic and complete to divide the network into the preceding and the succeeding
network (of the node). Of course, this separation method is reasonable for TBoxes with
a single concrete feature, because then each concrete neighborhood is complete and
atomic [11]. But also in the case of multiple concrete features, this separation method
can be applied by first guessing an atomic completion of the concrete neighborhood of
some abstract node a.
4 Implementation and evaluation
We implemented a reasoner based on the tableau algorithm and the optimization tech-
niques presented in section 3. The reasoner is implemented in C++ and uses GQR [22]
via libgqr for checking the satisfiability of spatial or temporal constraint networks. We
decided to make the connection between GQR and our reasoner loose, i.e. we construct
the network in our reasoner and translate it to a compatible data structure for the use
in GQR. This design decision makes it possible to incorporate other constraint solvers
without much effort.
To evaluate the proposed optimizations, we needed test problems. Unfortunately,
there do not exist any benchmark problems or ontologies using the given approach
based on ALC with constraints systems, which is maybe due to the fact that there does
not exist a concrete language for writing such problems, either. For this reason we had
to come up with synthetic test cases on our own.
To check the effect of the optimization techniques, we wanted to generate ‘realis-
tic’ knowledge bases, and therefore we adapted the method proposed in [6]. The basic
idea of this method is to analyze example knowledge bases in order to infer rules for
the generation of further synthetic knowledge bases from those examples. In more de-
tail, the method uses a fixed ratio of partial concept inclusions, a fixed number of role
names, and a fixed scheme for concept definitions (in contrast to [6] we also use concept
disjunction). Moreover, concepts are generated in layers to avoid terminological cycles
(i.e., concept definitions used in layer l mention concepts from the layers 0, . . . , l − 1
only). Further parameters are extracted from natural knowledge bases. For our experi-
ments, we wrote some example knowledge bases from scratch and additionally adapted
knowledge bases from SpacePortal on Ontohub [4]. In particular we considered the
knowledge bases ArchitecturalConstruction2 and BuildingStructure3 that use RCC8-
relations as roles and translated these into the ALC(C)-framework. Definitions using
constructors disallowed in ALC were rewritten or removed.
From these hand-crafted examples we derived the following rules:
.
– An axiom A v B or A = B contains concrete information (e.g. a conjunct
∀(R loc), (R loc).(r1 ∨ · · · ∨ rk ) or ∃(R loc), (R loc).(r1 ∨ · · · ∨ rk )) with a proba-
bility of 0.36.
– The average size of a constraint in a concrete concept is 3.31 in the case of Allen
and 3.08 in the case of RCC8. So a relation r is contained with a probability of 3.31 13
in the case of Allen and 3.088 in the case of RCC8.
– Only one concrete feature is used.
– Every declared concept is satisfiable, as in most real world knowledge bases this
should be the case.
Notice that the knowledge bases generated in this way are in the fragment described
in [11] as we only use one concrete feature. For each number 200, 400, . . . , 2000 of
axioms we generated 10 ontologies for both Allen and RCC8. For the evaluation we
used a timeout of 300s per instance.
The following strategies for checking the satisfiability of all defined concepts (i.e.
concepts on the left side of the axioms) were considered:
– All Opts: All considered optimizations were activated. This is the baseline, i.e., the
other strategies differ from this strategy by deactivating single optimizations.
– No Caching: All optimizations are activated except for caching.
– No Disjunctions: Disjunctive constraints are resolved to atomic constraints by the
tableau algorithm like in the original description of the algorithm in [11]. This is
expected to be highly inefficient as there are no heuristics or other optimizations
implemented for a careful selection of the relation, even though caching can be
applied to every node as every concrete neighborhood is atomic and complete.
– No Separation: The patchwork property is not used to divide the network into
smaller parts when the prerequisites of the patchwork property are satisfied. As
we only allow one concrete feature, the deactivation of this optimization should
have a huge impact on the runtime.
All tests were run on an Ubuntu 14.04 system with an Intel i3 U380 1.33GHz Pro-
cessor and 4GB of RAM.
In Figure 3 the results of our tests are shown. As expected the runtimes of ‘No
Caching’, ‘No Disjunctions’ and ‘No Separation’ are distinctly worse than the runtimes
2 http://ontohub.org/spaceportal/OntoSpace/ArchitecturalConstruction
3 http://ontohub.org/spaceportal/OntoSpace/BuildingStructure
300000
All Opts
No Caching
No Disjunction
250000
No Separation
200000
Time in ms
150000
100000
50000
0
200 400 600 800 1000 1200 1400 1600 1800 2000
Number of axioms
Fig. 3. Comparison of optimizations: 0.75-quantiles of the runtimes for generated knowledge
bases using Allen interval constraints
of ‘All Opts’. Notice that even the restricted form of caching used in our implementa-
tion shows to be beneficial. The most significant performance gains however are ob-
tained by delegating disjunctive constraints to an external reasoner and by applying the
generalized version of the patchwork property to split the network into smaller parts.
Moreover, comparing the benefits of using all optimization techniques with respect to
the used constraint system, our results do not show any significant difference between
the constraint systems.
We also conducted some experiments on test instances with multiple concrete fea-
tures. Our results indicate that instances without terminological cycles can be handled
by our reasoner quite well, while the presence of terminological cycles may degrade its
performance considerably.
5 Conclusion
We implemented and evaluated a reasoner for the description logic ALC(C) with gen-
eral TBoxes and temporal and spatial constraint systems based on the algorithm pro-
posed in [11]. To our knowledge, our implementation is the first reasoner supporting
such constraint systems. We adapted optimizations from [8] to this case and applied op-
timizations discussed in [11] for a fragment of ALC(C) to the general case. Restrictions
were necessary to use some of the optimizations, namely backjumping and caching. Our
implementation is loosely connected to the used constraint solver, i.e. another constraint
solver may be used without much effort. For example, in [12] a quite similar algorithm
for checking concept satisfiability with general TBoxes and fuzzy concrete domains is
proposed. It should be quite straightforward to adapt our implementation to this setting.
Acknowledgements. We thank the anonymous reviewers for helpful suggestions and
comments. This work was supported by DFG (Transregional Collaborative Research
Center SFB/TR 8 Spatial Cognition, project R4-[LogoSpace]).
References
1. Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–
843 (1983)
2. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages.
In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on
Artificial Intelligence. Sydney, Australia, August 24-30, 1991. pp. 452–457. Morgan Kauf-
mann (1991)
3. Baader, F., Hollunder, B., Nebel, B., Profitlich, H.J., Franconi, E.: An empirical analysis of
optimization techniques for terminological representation systems, or making KRIS get a
move on. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International
Conference on Principles of Knowledge Representation and Reasoning (KR’92). Cambridge,
MA, October 25-29, 1992. pp. 270–281. Morgan Kaufmann (1992)
4. Bateman, J., Kutz, O., Mossakowski, T., Sojic, A., Codescu, M.: Space for Space - Space-
Portal: the 21st century home for spatial ontologies. In: Freksa, C., Nebel, B., Hegarty,
M., Barkowsky, T. (eds.) Spatial Cognition 2014: Poster Presentations. pp. 13–16. No. 036-
09/2014 in SFB/TR 8 Report (2014)
5. Grütter, R., Bauer-Messmer, B.: Towards spatial reasoning in the semantic web: A hybrid
knowledge representation system architecture. In: Fabrikant, S.I., Wachowicz, M. (eds.) The
European Information Society: Leading the Way with Geo-information, Proceedings of the
10th AGILE Conference, Aalborg, Denmark, 8-11 May 2007. pp. 349–364. Lecture Notes
in Geoinformation and Cartography, Springer (2007)
6. Heinsohn, J., Kudenko, D., Nebel, B., Profitlich, H.: An empirical analysis of terminological
representation systems. Artificial Intelligence 68(2), 367–397 (1994)
7. Horrocks, I.: Optimising Tableaux Decision Procedures for Description Logics. Ph.D. thesis,
University of Manchester (1997)
8. Horrocks, I.: Implementation and optimization techniques. In: Baader, F., Calvanese, D.,
McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.) Description Logic Handbook. pp.
306–346. Cambridge University Press (2003)
9. Huang, J.: Compactness and its implications for qualitative spatial and temporal reasoning.
In: Brewka, G., Eiter, T., McIlraith, S.A. (eds.) Principles of Knowledge Representation and
Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, Rome, Italy,
June 10-14, 2012. AAAI Press (2012)
10. Lutz, C.: Description logics with concrete domains – a survey. In: Balbiani, P., Suzuki, N.,
Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic 4, papers from the fourth
conference on ”Advances in Modal logic,” held in Toulouse (France) in October 2002. pp.
265–296. King’s College Publications (2002)
11. Lutz, C., Miličić, M.: A tableau algorithm for description logics with concrete domains and
general TBoxes. Journal of Automated Reasoning 38(1-3), 227–259 (2007)
12. Merz, D., Peñaloza, R., Turhan, A.: Reasoning in ALC with fuzzy concrete domains. In:
Lutz, C., Thielscher, M. (eds.) KI 2014: Advances in Artificial Intelligence - 37th Annual
German Conference on AI, Stuttgart, Germany, September 22-26, 2014. Lecture Notes in
Computer Science, vol. 8736, pp. 171–182. Springer (2014)
13. Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In:
Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International Conference on
Principles of Knowledge Representation and Reasoning (KR’92). Cambridge, MA, October
25-29, 1992. pp. 165–176. Morgan Kaufmann (1992)
14. Renz, J., Nebel, B.: Qualitative spatial reasoning using constraint calculi. In: Aiello, M.,
Pratt-Hartmann, I., van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 161–215.
Springer (2007)
15. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Arti-
ficial Intelligence 48(1), 1–26 (1991)
16. Shearer, R., Motik, B., Horrocks, I.: HermiT: A highly-efficient OWL reasoner. In: Dolbear,
C., Ruttenberg, A., Sattler, U. (eds.) Proceedings of the Fifth OWLED Workshop on OWL:
Experiences and Directions, collocated with the 7th International Semantic Web Conference
(ISWC-2008), Karlsruhe, Germany, October 26-27, 2008. CEUR Workshop Proceedings,
vol. 432. CEUR-WS.org (2008)
17. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL rea-
soner. Web Semantics: Science, Services and Agents on the World Wide Web 5(2), 51–53
(2007)
18. Stocker, M., Sirin, E.: PelletSpatial: A hybrid RCC-8 and RDF/OWL reasoning and query
engine. In: Hoekstra, R., Patel-Schneider, P.F. (eds.) Proceedings of the 5th International
Workshop on OWL: Experiences and Directions (OWLED 2009), Chantilly, VA, United
States, October 23-24, 2009. CEUR Workshop Proceedings, vol. 529. CEUR-WS.org (2009)
19. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Fur-
bach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference,
IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Lecture Notes in Computer Science,
vol. 4130, pp. 292–297. Springer (2006)
20. Turhan, A., Haarslev, V.: Adapting optimization techniques to description logics with con-
crete domains. In: Baader, F., Sattler, U. (eds.) Proceedings of the 2000 International Work-
shop on Description Logics (DL2000), Aachen, Germany, August 17-19, 2000. CEUR Work-
shop Proceedings, vol. 33, pp. 247–256. CEUR-WS.org (2000)
21. Wessel, M.: Obstacles on the way to qualitative spatial reasoning with description log-
ics: Some undecidability results. In: Goble, C.A., McGuinness, D.L., Möller, R., Patel-
Schneider, P.F. (eds.) Working Notes of the 2001 International Description Logics Workshop
(DL-2001), Stanford, CA, USA, August 1-3, 2001. CEUR Workshop Proceedings, vol. 49.
CEUR-WS.org (2001)
22. Westphal, M., Wölfl, S., Gantner, Z.: GQR: A fast solver for binary qualitative constraint
networks. In: Benchmarking of Qualitative Spatial and Temporal Reasoning Systems, Papers
from the 2009 AAAI Spring Symposium, Technical Report SS-09-02, Stanford, California,
USA, March 23-25, 2009. pp. 51–52. AAAI (2009)