In many applications a reasonable representation of conceptual knowledge requires the possibility to express spatial or temporal relations between domain entities. A feasible approach to this is to consider spatial or temporal constraint systems on concrete domains. Indeed, Lutz and Milicˇic` (2007) showed that for the description logic ALC(C) with w-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.
When an application domain is to be conceptualized in terms of a terminological
knowledge 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., [
In this paper we present the first implementation of this tableau procedure.1 In
particular, we are interested in the question which of the standard optimization techniques
used in current description logic reasoners [
A second source for optimizations are special techniques that arise from
interweaving tableau reasoning and constraint-based reasoning. For example, spatial and
temporal constraint-based formalisms such as RCC8 [
The setup of the paper is as follows: In section 2, we provide the necessary
background on the description logic ALC(C) as well as the tableau procedure for ALC(C)
as presented in [
In what follows we introduce the technical background in a rather condensed way. For
a more detailed presentation we refer to [
Constraint systems. A constraint system on a concrete domain D is a finite set G 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 G , its disjunctive closure G _ is the set of all relations that are unions of relations in G . We write relations from G _ in the form r1 _ _ rn with ri 2 G (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 G 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 , NjV 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 G _ n G ). 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)) 2 r. The variable assignment a is then called a solution of the network. A network N is called a refinement of network N0 if for each constraint (v r v0) in N, if N0 contains a constraint of the form (v r0 v0) then r r0 (i.e., each relation r j 2 G mentioned in r is also mentioned in r0).
Examples of constraint systems include Allen’s interval calculus [
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
NjV 0 is satisfiable. It is said to have the patchwork property if for any pair of finite,
atomic, complete, and satisfiable networks N and N0 that coincide on all constraints with
variables from VN \VN0 , the network N [ N0 is satisfiable. Finally, the constraint system
is called w-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 w-admissibility [
C ::= A j :C j C u C0 j C t C0 j 9R:C j 8R:C j 9U1;U2:r j 8U1;U2:r with r 2 G _. In the constraint constructors 9U1;U2:r and 8U1;U2:r we allow the following 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 (DI ; I ),
where DI is called the domain and I the interpretation function. The interpretation
function maps each abstract feature f to a partial function from DI to DI , and each
concrete feature g to a partial function from DI to the concrete domain D. For pure
ALC-concepts we use the ordinary semantics as given in [
U I (x) := fd 2 DI : 9x1; : : : ; xk+1 2 DI ; such that x = x1; gI (xk+1) = d; and (x j; x j+1) 2 R Ij for 1 j k; g: 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
9(has-lifetime); (has-child has-lifetime):(s_d_f_=_>_mi_oi_si)
Tableau algorithm. Lutz and Milicˇic` [
The algorithm starts by creating a single abstract node a labeled with a set containing 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 successors (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 [
For pure DL concepts like concept conjunctions, concept disjunctions and role restrictions the standard tableau rules (Ru), (Rt), (R9), (R8) 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 considers the concrete neighborhood of abstract nodes. The concrete neighborhood of an abstract node a is defined as the set
N (a) := f(v r v0) 2 N : 9g; g0 2 feat(a) such that
v g-successor of a and v0 g0-successor of ag; 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
If 9U1;U2:r 2 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) 2 N for some i with 1 i n, then add ‘fresh’ U1- and U2-successors v1 and v2, resp., and set N := N [ f(v1 ri v2)g for some i with 1 i n.
If 8U1;U2:r 2 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) 2= N for each i with 1 i n, then set N := N [ f(v1 ri v2)g 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 order 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-NEXPTIME if satisfiability of the concrete domains is in NP [
Optimizations are essential to gain acceptable runtimes of the tableau algorithm. In [
The idea of lazy unfolding is to keep the structure of the knowledge base as long as
possible [
Absorption [
Backjumping [
Caching [
Example 2. Let R be an abstract feature (i.e. R is functional) and T be the following TBox:
A v 9R:(9(loc1); (loc2):(>)) u 9(loc1); (R loc1):(=) u 9(loc2); (R loc2):(=); B v 9(loc1); (loc2):(<) u 9(loc1); (R loc1):(=) u 9(loc2); (R loc2):(=) u 8R: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 network 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 8-rule on b. For example consider a node a with
L(a) = f9(loc1); (loc1):(=) u 9(loc2); (loc2):(=)g: >
R
A =
= 9(loc1); (loc2):(>) 9(loc1); (loc2):(>)
R and a parent node b of a connected by abstract feature R with
L(b) = f8(R loc1); (R loc2):(ntpp)g: Then, only if a is completely expanded (the concrete successors are generated), the 8rule 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
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 [
Patchwork property revisited. In the original version of the algorithm in [
Notice the difference between statements (i) and (ii) of the lemma. Condition (ii)
does not require the networks N and N0 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 R9c and R8c can be replaced by
deterministic versions that do not refine disjunctive constraints to atomic ones. The
rationale 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 [
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) := f(v r v0) 2 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 g
Np(a) := f(v r v0) 2 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 g
(a) N = Ns(a) [ Np(a); (b) Ns(a) \ Np(a) = N (a); (c) Ns(a)jVNs(a)\VNp(a) = Np(a)jVNs(a)\VNp(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 identity relation). The preceding network is given by the relations r1, r2, r4, r7 and r8, the c r5 r3 b r6 r1 r2 r4 r7 d r8 succeeding network by the relations r3, r5 and r6. By Lemmas 1 and 2 the satisfiability 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 [
We implemented a reasoner based on the tableau algorithm and the optimization
techniques presented in section 3. The reasoner is implemented in C++ and uses GQR [
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
‘realistic’ knowledge bases, and therefore we adapted the method proposed in [
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 8(R loc); (R loc):(r1 _ _ rk) or 9(R loc); (R loc):(r1 _ _ rk)) with a probability 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 31:331 in the case of Allen and 3:08 in the case of RCC8.
8 – 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 [
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 [
All tests were run on an Ubuntu 14.04 system with an Intel i3 U380 1.33GHz Processor 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 0 0 0 0 0 3 0 0 0 0 5 2 0 0 0 0 0 2 sm 0 iineTm 00051 0 0 0 0 0 1 0 0 0 0 5
All Opts
No Caching No Disjunction
No Separation 0 200 400 600 800 1000 1200 Number of axioms 1400 1600 1800 2000 of ‘All Opts’. Notice that even the restricted form of caching used in our implementation shows to be beneficial. The most significant performance gains however are obtained 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 features. 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
We implemented and evaluated a reasoner for the description logic ALC(C) with
general TBoxes and temporal and spatial constraint systems based on the algorithm
proposed in [