Spatial Symmetry Driven Pruning Strategies for
Efficient Declarative Spatial Reasoning
Carl Schultz1,3 and Mehul Bhatt2,3
Institute for Geoinformatics, University of Münster, Germany
Department of Computer Science, University of Bremen, Germany
3
The DesignSpace Group
1

arXiv:1506.04945v1 [] 16 Jun 2015

2

Abstract. Declarative spatial reasoning denotes the ability to (declaratively) specify and solve real-world problems related to geometric and
qualitative spatial representation and reasoning within standard knowledge representation and reasoning (KR) based methods (e.g., logic programming and derivatives). One approach for encoding the semantics of
spatial relations within a declarative programming framework is by systems of polynomial constraints. However, solving such constraints is computationally intractable in general (i.e. the theory of real-closed fields).
We present a new algorithm, implemented within the declarative spatial
reasoning system CLP(QS), that drastically improves the performance
of deciding the consistency of spatial constraint graphs over conventional
polynomial encodings. We develop pruning strategies founded on spatial
symmetries that form equivalence classes (based on affine transformations) at the qualitative spatial level. Moreover, pruning strategies are
themselves formalised as knowledge about the properties of space and
spatial symmetries. We evaluate our algorithm using a range of benchmarks in the class of contact problems, and proofs in mereology and
geometry. The empirical results show that CLP(QS) with knowledgebased spatial pruning outperforms conventional polynomial encodings
by orders of magnitude, and can thus be applied to problems that are
otherwise unsolvable in practice.
Keywords: Declarative Spatial Reasoning, Geometric Reasoning, Logic
Programming, Knowledge Representation and Reasoning

1

Introduction

Knowledge representation and reasoning (KR) about space may be formally interpreted within diverse frameworks such as: (a) analytically founded geometric
reasoning & constructive (solid) geometry [21, 27, 29]; (b) relational algebraic semantics of ‘qualitative spatial calculi’ [24]; and (c) by axiomatically constructed
formal systems of mereotopology and mereogeometry [1]. Independent of formal semantics, commonsense spatio-linguistic abstractions offer a human-centred
and cognitively adequate mechanism for logic-based automated reasoning about
spatio-temporal information [5].
. Declarative Spatial Reasoning In the recent years, declarative spatial
reasoning has been developed as a high-level commonsense spatial reasoning

2

Carl Schultz and Mehul Bhatt

paradigm aimed at (declaratively) specifying and solving real-world problems
related to geometric and qualitative spatial representation and reasoning [4]. A
particular manifestation of this paradigm is the constraint logic programming
based CLP(QS) spatial reasoning system [4, 33, 34] (Section 2).
. Relational Algebraic Qualitative Spatial Reasoning The state of the
art in qualitative spatial reasoning using relational algebraic methods [24] has
resulted in prototypical algorithms and black-box systems that do not integrate
with KR languages, such as those dealing with semantics and conceptual knowledge necessary for handling background knowledge, action & change, relational
learning, rule-based systems etc. Furthermore, relation algebraic qualitative spatial reasoning (e.g. LR [25]), while efficient, is incomplete in general [22, 23, 24].4
Alternatively, constraint logic programming based systems such as CLP(QS) [4]
and others (see [9, 10, 18, 20, 28, 29]) adopt an analytic geometry approach where
spatial relations are encoded as systems of polynomial constraints;5 while these
methods are sound and complete (see Section 2.2), they have prohibitive comcn
putational complexity, O(c12 ) in the number of polynomial variables n, meaning
that even relatively simple problems are not solved within a practical amount
of time via “naive” or direct encodings as polynomial constraints, i.e. encodings
that lack common-sense knowledge about spatial objects and relations. On the
other hand, highly efficient and specialised geometric theorem provers (e.g. [12])
and geometric constraint solvers (e.g. [17, 27]) exist. However, these provers exhibit highly specialised and restricted spatial languages6 and lack (a) the direct
integration with more general AI methods and (b) the capacity for incorporating modular common-sense rules about space in an extensible domain- and
context-specific manner.
The aims and contributions of the research presented in this paper are two-fold:
1. to further develop a KR-centered declarative spatial reasoning paradigm
such that spatial reasoning capabilities are available and accessible within
AI programs and applications areas, and may be seamlessly integrated with
other AI methods dealing with representation, reasoning, and learning about
non-spatial aspects
4

5

6

Incompleteness refers to the inability of a spatial reasoning method to determine
whether a given network of qualitative spatial constraints is consistent or inconsistent
in general. Relation-algebraic spatial reasoning (i.e. using algebraic closure based
on weak composition) has been shown to be incomplete for a number of spatial
languages and cannot guarantee consistency in general, e.g. relative directions [23]
and containment relations between linearly ordered intervals [22], Theorem 5.9.
We emphasise that this analytic geometry approach that we also adopt is not qualitative spatial reasoning in the relation algebraic sense; the foundations are similar
(i.e. employing a finite language of spatial relations that are interpreted as infinite
sets of configurations, determining consistency in the complete absence of numeric
information, and so on) but the methods for determining consistency etc. come from
different branches of spatial reasoning.
Standard geometric constraint languages of approaches including [12, 17, 27] consist
of points, lines, circles, ellipses, and coincidence, tangency, perpendicularity, parallelism, and numerical dimension constraints; note the absence of e.g. mereotopology
and “common-sense” relative orientation relations [35].

Spatial Symmetry Driven Pruning

3

2. to demonstrate that in spite of high computational complexity in a general
and domain-independent case, the power of analytic geometric —in particular polynomial systems for encoding the semantics of spatial relations–
can be exploited by systematically utilising commonsense knowledge about
spatial object and relationships at the qualitative level.

We present a new algorithm that drastically improves analytic spatial reasoning
performance within KR-based declarative spatial reasoning approaches by identifying and pruning spatial symmetries that form equivalence classes (based on
affine transformations) at the qualitative spatial level. By exploiting symmetries
our approach utilises powerful underlying, but computationally expensive, polynomial solvers in a significantly more effective manner. Our algorithm is simple
to implement, and enables spatial reasoners to solve problems that are otherwise
unsolvable using analytic or relation algebraic methods. We emphasise that our
approach is independent of any particular polynomial constraint solver; it can be
similarly applied over a range of solvers such as CLP(R), SMTs, and specialised
geometric constraint solvers that have been integrated into a KR framework.
In addition to AI / commonsense reasoning applications areas such as design,
GIS, vision, robotics [3, 5, 6, 7], we also address application into automating
support for proving the validity of theorems in mereotopology, orientation, shape,
etc. (e.g. [8, 36]). Building on such foundational capabilities, another outreach is
in the area of computer-aided learning systems in mathematics (e.g. at a highschool level). For instance, consider Proposition 9, Book I of Euclid’s Elements,
where the task is to bisect an angle using only an unmarked ruler and collapsable
compass. Once a student has developed what they believe to be a constructive
proof, they can employ declarative spatial reasoners to formally verify that their
construction applies to all possible inputs (i.e. all possible angles) and manipulate
an interactive sketch that maintains the specified spatial relations (i.e. dynamic
geometry [17]). A further area of interest is verifying the entries of composition
tables that are used in relation algebraic qualitative spatial reasoning [30]: given
spatial objects a, b, c ∈ U , composition “look up” tables are indexed by pairs of
(base) relations R1ab , R2bc and return disjunctions of possible (base) relations

R3ac . For each entry, the task is to prove ∃a, b, c ∈ U R1ab ∧ R2bc ∧ R3ac for
only those base relations R3 in the entry’s disjunction.

2

Declarative Spatial Reasoning with CLP(QS)

Declarative spatial reasoning denotes the ability of declarative programming
frameworks in AI to handle spatial objects and the spatial relationships amongst
them as native entities, e.g., as is possible with concrete domains of Integers,
Reals and Inequality relationships. The objective is to enable points, oriented
points, directed line-segments, regions, and topological and orientation relationships amongst them as first-class entities within declarative frameworks in AI
[4].

4

Carl Schultz and Mehul Bhatt

2.1

Examples of Declarative Spatial Reasoning with CLP(QS)

With a focus on spatial question-answering, the CLP(QS) spatial reasoning system [4, 33, 34] provides a practical manifestation of certain aspects of the declarative spatial reasoning paradigm in the context of constraint logic programming
(CLP). 7 CLP(QS) utilises a high-level language of spatial relations and commonsense knowledge about how various spatial domains behave. Such relations
describe sets of object configurations, i.e. qualitative spatial relations such as
coincident, left of, or partially overlapping. Through this deep integration of
spatial reasoning with KR-based frameworks, the long-term research agenda
is to seamlessly provide spatial reasoning in other AI tasks such as planning,
non-monotonic reasoning, and ontological reasoning [4]. What follows is a brief
illustration of the spatial Q/A capability supported by CLP(QS).
EXAMPLE A. Massachusetts Comprehensive Assessment System (MCAS)
Grade 3 Mathematics (2009), Question 12. Put a square and two rightangled triangles together to make a rectangle. (1) Put the shapes T1 , T2 , S illustrated in Figure 1(d) together to make a rectangle. (2) Put the shapes T1 , T2 , S
in Figure 1(d) together to make a quadrilateral that is not a rectangle.
CLP(QS) represents right-angle triangles as illustrated in Figure 1(b). Figures
1(a) and 1(c) present the CLP(QS) solutions.
Grade 3 Mathematics (2013), Question 17. (1) How many copies of T1
illustrated in Figure 1(d) are needed to completely fill the region R illustrated in
Figure 2(a) without any of them overlapping?
As presented in Figure 2, CLP(QS) solves both the geometric definition and a
variation where the dimensions of the rectangle and triangles are not given.
EXAMPLE B. Qualitative Spatial Reasoning with Complete Unknowns
In this example CLP(QS) reasons about spatial objects based solely on given
qualitative spatial relations, i.e. without any geometric information.
Define three cubes A, B, C. Put B inside A, and make B disconnected from C.
What spatial relations can possibly hold between A and C?
CLP(QS) determines that A must be disconnected from C and provides the
inferred corresponding geometric constraints, as illustrated in Figure 3.
2.2

Analytical Geometry Foundations for Declarative Spatial
Reasoning

Analytic geometry methods parameterise classes of objects and encode spatial
relations as systems of polynomial equations and inequalities [12]. For example,
we can define a sphere as having a 3D centroid point (x, y, z) and a radius r,
where x, y, z, r are reals. Two spheres s1 , s2 externally connect or touch if
(xs1 − xs2 )2 + (ys1 − ys2 )2 + (zs1 − zs2 )2 = (rs1 + rs2 )2
7

Spatial Reasoning (CLP(QS)). www.spatial-reasoning.com

(1)

Spatial Symmetry Driven Pruning

= right_triangle(_,_,W,W),
= right_triangle(_,_,W,W),

?- T1
|

talking about space

17

talking about space

17

5

TW

T2

|
S = rectangle(_,W,W),
?- T1 = right_triangle(_,_,W,W),
|
Solution = rectangle(_,_,_),
|
T2 = right_triangle(_,_,W,W),
|
topology(rcc8(eq), Solution, tile_union([T1,T2,S])),
|
S = rectangle(_,W,W),
|
ground_object(Solution).
|
Solution = rectangle(_,_,_),
|
topology(rcc8(eq), Solution, tile_union([T1,T2,S])),
T1 = right_triangle(orientation(0), point(0, 0), 5, 5),
|
ground_object(Solution).
W = 5,
T2 = right_triangle(orientation(180), point(5, 5), 5, 5),
T1 = right_triangle(orientation(0), point(0, 0), 5, 5),
S = rectangle(point(5, 0), 5, 5),
W = 5,
Solution = rectangle(point(0, 0), 10, 5) .
T2 = right_triangle(orientation(180), point(5, 5), 5, 5),

TH

TW

TX,TY

orientation = 0o

(a) CLP(QS) solution to arranging T , T , S to
rectangle.
Solution = rectangle(point(0, 0), 10, 5) .
form
rectangles.
?- T1 = right_triangle(_,_,W,W),

TX,TY

orientation = 90o

(b) Representing right-angle triangle
T in CLP(QS).

the shapes in Figure 10),
together
to make a quadrilateral
S Put
= rectangle(point(5,
5, 5),
1 that2 is not a

Put the shapes in _Figure 1 together
to make a quadrilateral that is not a
|
T2 = right triangle(_,_,W,W),
rectangle.
_
|
S = rectangle( ,W,W),
?- T1 = right_triangle(_,_,W,W),
|
topology(rcc8(eq), Solution, tile_union([T1,T2,S])),
|
T2 = right_triangle(_,_,W,W),
|
quadrilateral(Solution),
|
S = rectangle(_,W,W),
|
not(Solution = rectangle(_,_,_)),
|
topology(rcc8(eq), Solution, tile_union([T1,T2,S])),
|
ground_object(Solution).
|
quadrilateral(Solution),
|
not(Solution = rectangle(_,_,_)),
T1 = right_triangle(orientation(90), point(5, 0), 5, 5),
|
ground_object(Solution).
W = 5,
T2 = right_triangle(orientation(270), point(10, 5), 5, 5),
T1 = right_triangle(orientation(90), point(5, 0), 5, 5),
S = rectangle(point(5, 0), 5, 5),
W = 5,
Solution = parallelogram(orientation(0), point(0,0), 10, 5);
T2 = right_triangle(orientation(270), point(10, 5), 5, 5),
...
S = rectangle(point(5,
0), 5, 5),
T1 = right_triangle(orientation(90), point(5, 0), 5, 5),
Solution = parallelogram(orientation(0), point(0,0), 10, 5);
W = 5,
...
T2 = right_triangle(orientation(0), point(10, 0), 5, 5),
T1 = right_triangle(orientation(90), point(5, 0), 5, 5),
S = rectangle(point(5, 0), 5, 5),
W = 5,
Solution = trapezoid(orientation(0), point(0, 0), 15, 5, 5);
T2 = right_triangle(orientation(0), point(10, 0), 5, 5),
...
S = rectangle(point(5, 0), 5, 5),
false.
Solution = trapezoid(orientation(0), point(0, 0), 15, 5, 5);

2013 Massachusetts Comprehensive Assessment System (MCAS)
Grade 3 Mathematics, Question 17.
How many triangles illustrated in Figure 1 are needed to completely
2013 Massachusetts Comprehensive Assessment System (MCAS)
1
2
fill the region illustrated in Figure 3 without any overlapping?
Grade 3 Mathematics, Question 17.
How many triangles illustrated in Figure 1 are needed to completely
fill the region illustrated in Figure 3 without any overlapping?

TH

T1

T2

S

shapes to arrange

rectangle

parallelogram

...

trapezoid

false.

(c) CLP(QS) solution to arranging T , T , S to
form non-rectangular quadrilaterals.

18

(d) Shapes T1 , T2 , S
spatial reasoning in cognitive systems
to be arranged and
CLP(QS) solutions.

?- between(1,8,TriangleCount),
|
right_triangle_list(TriangleCount,[T1|TRest]),

_,_,1,1),
T1 = right_triangle(Test
Fig. 1. Using CLP(QS) to solve MCAS Grade| 3 Mathematics
questions (2009).
|

size(equal, T1, TRest),

|

topology(rcc8(eq), rectangle(point(0,0),3,1),
tile_union([T1|TRest])).

|

region R
18

tiling solution

spatial reasoning in cognitive systems

TriangleCount = 6

When no geometric information is given, CLP(QS) determines that
the number of right-angled triangles must be odd:
?- between(1,8,TriangleCount),
|
right_triangle_list(TriangleCount,Triangles),

?- between(1,8,TriangleCount),
|
right_triangle_list(TriangleCount,[T1|TRest]),

|
|

topology(rcc8(eq), rectangle(_,_,_),
tile_union(Triangles)).

|

T1 = right_triangle(_,_,1,1),

|

size(equal, T1, TRest),

TriangleCount = 2;...

|

topology(rcc8(eq), rectangle(point(0,0),3,1),
tile_union([T1|TRest])).

TriangleCount = 4;...

|

TriangleCount = 6;...
TriangleCount = 8;

TriangleCount = 6

false.

Regenstno
High
School Examination,
The University
of the
no geometric
information
determines that (b)2012
(a)When
CLP(QS)
solution
tois given,
tilingCLP(QS)
a rectangular
When
geometric
information
is given,
State of New York
the number of right-angled triangles must be odd:
region
with
triangle
T
.
CLP(QS)
determines
that
the
number
of
right1
?- between(1,8,TriangleCount),
Part 1, Question 1.
angle
must
even.angles shown in Figure 4.
|
right_triangle_list(TriangleCount,Triangles),
Line ntriangles
intersects lines
l and be
m, forming
|
|

topology(rcc8(eq), rectangle(_,_,_),
tile_union(Triangles)).

Which value of x would prove l ||m?

?- L=line(_, horizon_angle(_)),

M=line(_, horizon_angle(
Fig. 2. Using CLP(QS) to solve MCAS Grade| 3 Mathematics
Test_)),questions (2013).
N=line(_, horizon_angle(_)),

TriangleCount = 2,

|

... ; ...

|

TriangleCount = 4,

|

... ; ...

|

TriangleCount = 6,

|

... ; ...

|

TriangleCount = 8,

|

... ;

|

orientation(parallel, L,M),
orientation(angle_degrees(Theta1), M,N),
orientation(angle_degrees(Theta2), L,N),

false.

|

true.

2012 Regenst High School Examination, The University of the
State of New York
Part 1, Question 1.
Line n intersects lines l and m, forming angles shown in Figure 4.
Which value of x would prove l ||m?

{Theta1 =:= 18 * X - 12},
{Theta2 =:= 6 * X + 42},

...
Theta1 = Theta2, Theta2 = 69.0,
X = 4.5

talking about space

19

Figure 4: Regents High School Examination question to find x to prove that l and

6

m are
parallel.
Carl Schultz
and
Mehul Bhatt

Figures/clpqs/nyu-exercise.png

B
?- A=cube(_, _), B=cube(_, _), C=cube(_, _),
|

topology(rcc8(ntpp), A, B),

|

topology(rcc8(dc), B, C),

|

topology(Relation, A,C),

|

constraints([(A,’A’),(B,’B’),(C,’C’)],Cons),
pretty_print_constraints(Cons).

|

---------------------------------CLP(QS) Constraints:
(1)

B.length+B.x-C.x< -0.0

(2)

A.z-B.z>0.0

(3)

A.length-B.length+A.z-B.z<0.0

(4)

A.y-B.y>0.0

(5)

A.length-B.length+A.y-B.y<0.0

(6)

A.x-B.x>0.0

(7)

A.length-B.length+A.x-B.x<0.0

(8)

A.length>0.0

(9)

C.length>0.0

20

ntpp

A

C

Relation = rcc8(dc),
...

A

C

dc page 2 of 2
examples

(1) Bx + Bl < Cx

B is left of C

(2) Az > Bz

the front face of A is behind
the front face of B

(3) Az + Al < Bz + Bl

the back face of A is in front
of the back face of B

(4) Ay > By

the base of A is above the
base of B

(5) Ay + Al < By + Bl

the top of A is below the
top of B

(6) A x > Bx

the left side of A is right of
the left side of B

(7) A x + Al < Bx + Bl

the right side of A is left of
the right side of B

---------------------------------...

B

dc

spatial reasoning in cognitive systems

(8) Al > 0

A side length is positive

(9) Cl > 0

C side length is positive

(a) CLP(QS) solution and its corresponding (b) Behaviour
Geometric
inequalities provided by
Specification using Spatial Knowledge
inferred
CLP(QS) that correspond to the qualitative
In the behaviour specification we use CLP(QS) to find out on which
geometric constraints.
constraints.
side of the robot the goal field is and turn the robot accordingly.

Define a new predicate get_direction/4 in the beginning of the file, that

Fig. 3. Spatial reasoning about cubes A,B,C takes
withthecomplete
geometric
unknowns.
points of the robots
location and
the goal location and the facing
direction and gives us the orientation of the goal relative to the robot. The
If the system of polynomial constraints is satisfiable
then the spatial constraint
possible relations are left, right, front and back.
_direction(point(Xa,Ya),
graph is consistent. Specifically, the system of get
polynomial
(in)equalities
over direction(D)
varipoint(Xb,Yb),
, Rel):direction(point(Xa,Ya),
Line),
ables X is satisfiable if there exists a real number assignment
for eachdirection(D),
x ∈ X such
point(Xb, Yb)).
that the (in)equalities are true. Partial geometric orientation(Rel,Line,
information (i.e.
a combinaTo execute the sensing actions, extend the sensing interrupt by the new
tion of numerical and qualitative spatial information)
is
utilised
by
assigning
the
sensing action.
given real numerical values to the corresponding
object parameters.
Thus, we can
interrupt(sensed
= false,
[
integrate spatial reasoning and logic programming
using Constraint Logic Programming (CLP) [19]; this system is called CLPsenseFront,
over
qualitative spatial domains.
senseGoalLocation,
CLP(QS), provides a suitable framework for expressing
and proving first-order
senseRobotLocation
]),
spatial theorems.
To let the robot turn into the direction of the goal after each step, define two

Cylindrical Algebraic Decomposition (CAD) new
[13]
is a prominent sound and cominterrupts after the sensing interrupt.
plete algorithm for deciding satisfiability of a general
system of polynomial conThe first
interrupt is executed when the next field is free and the robot has
cn
2 in the last step.
moved
straints over reals and has time complexity not
O(c
)
in
the number of free vari1
ables [2]. Thus, a key focus within analytic spatial reasoning has been methods
for managing this inherent intractibility.8 More efficient refinements of the original CAD algorithm include partial CAD [14]. Symbolic methods for solving
systems of multivariate equations include the Gröbner basis method [11] and
Wu’s characteristic set method [40]. In the QUAD-CLP(R) system, the authors
improve solving performance by using linear approximations of quadratic constraints and by identifying geometric equivalence classes [28]. Ratschan employs
pruning methods, also at the polynomial level, in the rsolve system [31, 32].
8

Important factors in determining the applicability of various analytic approaches are
the degree of the polynomials (particularly the distinction between linear and nonlinear) and whether both equality and inequalities are permitted in the constraints.

Spatial Symmetry Driven Pruning

7

Constructive and iterative (i.e. Newton and Quasi-Newton iteration) methods
solve spatial reasoning problems by “building” a solution, i.e. by finding a configuration that satisfies the given constraints [27]. If a solution is found, then the
solution itself is the proof that the system is consistent – but what if a solution
is not found within a given time frame? In general these methods are incomplete
for spatial reasoning problems encoded as nonlinear equations and inequalities
of arbitrary degree.9

3

Spatial Symmetries

Information about objects and their spatial relations is formally expressed as
a constraint graph G = (N, E), where the nodes N of the graph are spatial
objects and the edges between nodes specify the relations between the objects.
Objects belong to a domain, e.g. points, lines, squares, and circles in 2D Euclidean space, and cuboids, vertically-extruded polygons, spheres, and cylinders
in 3D Euclidean space. We denote the object domain of node i as Ui (spatial
domains are typically infinite). A node may refer to a partially ground, or completely geometrically ground object, such that Ui can be a proper subset of the
full domain of that object type. Each element i0 ∈ Ui is called an instance of
that object domain. A configuration of objects is a set of instances {i01 , . . . , i0n }
of nodes i1 , . . . , in respectively.
A binary relation Rij between nodes i, j distinguishes a set of relative configurations of i, j; relation R is said to hold for those configurations, Rij ⊆ Ui × Uj . In
general, an n-ary relation for n ≥ 1 distinguishes a set of configurations between
n objects: Ri1 ,...,in ⊆ Ui1 × · · · × Uin .

An edge between nodes i, j is assigned a logical formula over relation symbols
R1 , . . . , Rm and logical operators ∨, ∧, ¬. Given an interpretation i0 , j 0 , the formula for edge e is interpreted in the standard way, denoted e(i0 , j 0 ):
–
–
–
–

R1 ≡ (i0 , j 0 ) ∈ R1ij
(R1 ∨ R2 ) ≡ (i0 , j 0 ) ∈ R1ij ∪ R2ij
(R1 ∧ R2 ) ≡ (i0 , j 0 ) ∈ R1ij ∩ R2ij
(¬R1 ) ≡ (i0 , j 0 ) ∈ (Ui × Uj ) \ R1ij

An edge between i, j is satisfied by a configuration i0 , j 0 if e(i0 , j 0 ) is true (this
is generalised to n-ary relations). A spatial constraint graph G = (N, E) is
consistent or satisfiable if there exists a configuration s of N that satisfies all
edges in E, denoted G(s); this is referred to as the consistency task. Graph G0 is
a consequence of, or implied by, G if every spatial configuration that satisfies G
also satisfies G0 . This is the sufficiency task (or entailment) that we commonly
apply to constructive proofs, where the task is to prove that objects and relations
in G are sufficient for ensuring that particular properties hold in G0 .
Given graph G, two key questions are (1) how to give meaning, or interpret,
the spatial relations in G, and (2) how to efficiently determine consistency and
produce instantiations of G. That is, we need to adopt a method for spatial
reasoning.
9

That is, constructive methods may fail in building a consistent solution, and iterative
root finding methods may fail to converge.

8

Carl Schultz and Mehul Bhatt

(a) initial configuration

(b) rotation

(c) translation

Fig. 4. Topological relations between four spheres maintained after various affine transformations.

3.1

An Example of the Basic Concept

A key insight is that spatial configurations form equivalence classes over qualitative relationships based on certain affine transformations. For example, consider
the spatial task of determining whether five same-sized spheres can be mutually touching. Suppose we are given a specific numerically defined configuration
of four mutually touching spheres as illustrated in Figure 4(a), and we prove
that it is impossible to add an additional mutually touching sphere to this configuration. That is, let s1 , . . . , s4 be unit spheres (radiusq1), q
centred on points
√
1
p1 = (0, 0, 0), p2 = (2, 0, 0), p3 = (1, 3, 0), p4 = (1, 3 , 83 ), respectively.
According to Equation 1, s1 , . . . , s4 are mutually touching. We prove that a fifth
same-sized, mutually touching sphere cannot be added to this configuration by
determining that the corresponding system of polynomial constraints is unsatisfiable (the system consists of four constraints with three free variables xs5 , ys5 , zs5 ,
by reapplying Equation 1 between s5 and each other sphere, e.g. s1 touches s5
is x2s5 + ys25 + zs25 = 4).
Now consider that we apply an affine transformation to the original configuration
such as rotation, translation, scaling, or reflection, as illustrated in Figures 4(b)
and 4(c). After having applied the transformation, it is still impossible to add
a fifth mutually touching sphere, because the relevant qualitative (topological)
relations are preserved under these transformations. Thus, when we proved that
it was impossible to add a fifth same-sized mutually touching sphere to the
original given configuration, in fact we proved it for a class of configurations,
specifically, the class of configurations that can be reached by applying an affine
transformation to the original configuration. Now, when determining consistency
of graphs of qualitative spatial relations, we are not given any specific spatial
configurations to work with (i.e. complete absence of numerical information),
and instead need to prove consistency over all possible configurations.
The key is that, each time we ground and constrain variables, we are eliminating a spatial symmetry from our partially defined configuration. If we maintain
knowledge about symmetries that certain object types have (e.g. spheres have
complete rotational symmetry) then we can judiciously “trade” symmetries for
unbound variables in our polynomial encoding at a purely symbolic level. Importantly, rather than having to compute symmetries or undertake any complex
symmetry detection procedure, we are instead building knowledge about space
and spatial properties of objects into the spatial solver at a declarative level.
Thus, we are able to efficiently reason over an infinite set of possible configurations by incrementally pruning spatial symmetries based on commonsense

Spatial Symmetry Driven Pruning

9

knowledge about space, and this pruning is exploited by eliminating and constraining variables in the underlying polynomial encoding.
3.2

Theoretical Foundations for Symmetries

Due to the parameterisation of objects, spatial configurations are embedded in
n-dimensional Euclidean space Rn (1 ≤ n ≤ 3) with a fixed origin point. Let
V, W be Euclidean spaces in Rn , each with an origin. Given vectors x, y and
constant k, a linear transformation f is a mapping V → W such that
f (x + y) = f (x) + f (y)

(additive)

f (kx) = kf (x)

(homogeneous)

An affine transformation f 0 is a linear transformation composed with a translation. It is convenient to represent a linear transformation on vector x as a left
multiplication of a d×d real matrix Q, and translation as an addition of vector t,
f 0 (x) = Qx + t. We denote a transformation T applied to a spatial configuration
of objects s as T s.
We distinguish particular classes of transformations with respect to the qualitative spatial relationships that are preserved, for example, in R2 the following
matrices represent rotation by θ, uniform scaling by k > 0, and horizontal reflection, respectively:

 
 

cos(θ) −sin(θ)
k0
−1 0
,
,
.
sin(θ) cos(θ)
0k
01
Given transformation T we annotate it with its type c ∈ C, e.g. C = {translate,
rotate, scale, reflect} as T c . Each spatial relation R belongs to a class of relations
in Rel, such as topology, mereology, coincidence, relative orientation, distance.
Let Sym be a function Sym : Rel → 2C that represents the classes of transformations that preserve a given class of spatial relations. The Sym function is
our mechanism for building knowledge about spatial symmetries into the spatial
reasoning system. Let RelG be the set of classes of the spatial
relations that are
T
used in the spatial constraint graph G, and let SymG = R∈RelG Sym(R).
The following formal Condition on SymG states that transformations (applied to
the embedding space) define equivalence classes of configurations with respect
to the consistency of spatial constraint graphs. When satisfied, this condition
provides a theoretically sound foundation for symmetry pruning.
Condition 1 Given spatial constraint graph G, configuration s, and affine transformation T c with c ∈ SymG then G(s) is true if and only if G(T c s).
3.3

Polynomial Encodings for Spatial Relations

In this section we define a range of spatial domains and spatial relations with
the corresponding polynomial encodings. While our method is applicable to a
wide range of 2D and 3D spatial objects and qualitative relations, for brevity
and clarity we primarily focus on a 2D spatial domain. Our method is readily
applicable to other 2D and 3D spatial domains and qualitative relations, for
example, as defined in [4, 9, 10, 28, 29, 33, 34].

10

Carl Schultz and Mehul Bhatt
Relation

Polynomial Encoding

left of
(point p, segment sab )
collinear
(point p, segment sab )
right or collinear
(point p, segment sab )
parallel
(segments sab , scd )
coincident
(point p, segment sab )
coincident
(point p, circle c)
inside
(point p, rectangle a)
intersects
(point p, rectangle a)
boundary
(point p, rectangle a)
outside
(point p, rectangle a)
concentric
(rectangles a, b)
part of
(rectangles a, b)
proper part
(rectangles a, b)
boundary part of
(rectangles a, b)
discrete from
(rectangles a, b)
partially overlaps
(rectangles a, b)

(xb − xa )(yp − ya ) > (yb − ya )(xp − xa )
(xb − xa )(yp − ya ) = (yb − ya )(xp − xa )
(xb − xa )(yp − ya ) ≤ (yb − ya )(xp − xa )
(yb − ya )(xd − xc ) = (yd − yc )(xb − xa )
collinear(p, sab ) ∧ xp ∈ [xa , xb ] ∧ yp ∈ [ya , yb ]
(xc − xp )2 + (yc − yp )2 = rc2
(0 < (p − p1a ) · va < wa )∧
0
(0 < (p − p1a ) · va
< ha )
(0 ≤ (p − p1a ) · va ≤ wa )∧
0
≤ ha )
(0 ≤ (p − p1a ) · va
intersects(p, a) ∧ ¬ inside(p, a)
¬ intersects(p, a)
1
2 (p3a

V

− p1a ) + p1a =

i=1...4

1
2 (p3b

− p1b ) + p1b

intersects(pia , b)

¬ equals(a, b) ∧ part_of(a, b)
V
i=1...4 boundary(pia , b)
W

i=1...4

∃pi ∈ R2
∃pj ∈ R2
∃pk ∈ R2

right_or_collinear(a, (pib , p(i+1)b ))

∨ right_or_collinear(b, (pia , p(i+1)a ))

inside(pi , a) ∧ inside(pi , b) ∧
inside(pj , a) ∧ outside(pj , b) ∧
outside(pk , a) ∧ inside(pk , b)

Table 1. Polynomial encodings of qualitative spatial relations.

– a point is a pair of reals x, y
– a line segment is a pair of end points p1 , p2 (p1 6= p2 )
– a rectangle is a point p representing the bottom left corner, a unit direction
vector v defining the orientation of the base of the rectangle, and a real width
and height w, h (0 < w, 0 < h); we can refer to the vertices of the rectangle:
let v 0 = (−yv , xv ) be v rotated 90o counter-clockwise, then p1 = p = p5 , p2 =
wv + p1 , p3 = wv + hv 0 + p1 , p4 = hv 0 + p1
– a circle is a centre point p and a real radius r (0 < r)
We consider the following spatial relations:
Relative Orientation. Left, right, collinear orientation relations between points
and segments, and parallel, perpendicular relations between segments [23].
Coincidence. Intersection between a point and a line, and a point and the boundary of a circle. Also whether the point is in the interior, outside or on the boundary of a region.
Mereology. Part-whole relations between regions [37].
Table 1 presents the corresponding polynomial encodings. Given three real variables v, i, j, let:
v ∈ [i, j] ≡ i ≤ v ≤ j ∨ j ≤ v ≤ i.

l2

l1

l3 pa

l2

l1

pd
p p
pb l3c a

pd

l3 pa
l3 pa

pb p
c
pd

pc

pb

l2

l1
Spatial Symmetry Driven Pruning

l2

l1

l2pd

l1

pb
l3 pa l3 pa
(a)

pd
pc

pb

configuration
points and lines

l1

pc
of

l1 pd
l3 pa l3l1 ppad
pc
p
p
b
cpb
lp2c
l2 pc
pb
llp32d pbpd l3
l2
pa
p
a
l1
l1
(b)

vertical reflection

p

(c)

x-scaling

pd

l1

pc
pb

l2

pa

l2

l1

rotation

p

l2
l2
pl3b
pwhether
a point is inside
a prectangle is based on vector projection.
b
l3Determining
p
a
pa p pisa projected onto vector v aby taking
Point
the dot product,
l3
l3
(xp , yp ) · (xv , yv ) = xp xv + yp yv

Given point a and rectangle b, we translate the point such that the bottom left
corner of b is at the origin, project pa on the base and side vectors of b, and
check whether the projection lies within the width and height of the rectangle,
0 < (pa − p1b ) · vb < wb
0 < (pa − p1b ) · vb0 < hb

Convex regions a, b are disconnected iff there is a hyperplane of separation, i.e.
there exists a line l such that a and b lie on different sides of l. This is the basis
for determining the discrete from relation between rectangles.
Formalising Knowledge about Symmetries

In this section we formally determine the qualitative spatial relations that are
preserved by various affine transformations. A fundamental property of affine
transformations is that they preserve (a) point coincidence (e.g. line intersections), (b) parallelism between straight lines, and (c) proportions of distances
between points on parallel lines [26]. For example, consider the configuration of
points pa , pb , pc , pd and lines l1 , l2 , l3 in Figure 5: (a) we cannot introduce new
points of coincidence between lines by applying transformations such as translation, scaling, reflection, and rotation. Conversely, if two lines intersect, then they
will still intersect after these transformations; (b) lines l1 , l2 are parallel before
and after the transformations; lines l1 , l3 are always non-parallel; (c) the ratio of
distances between collinear points pa , pb , pc is maintained; formally, let sij be the
segment between points pi , pj and let |sij | be the length of the segment. Then
ab |
the ratio |s
|sbc | in Figure 5 is the same before and after the transformations.

Based on these properties we can determine the transformations that preserve
various qualitative spatial relations.10
10

pd

The properties of affine transformations and the geometric objects that they preserve
are well understood; further information is readily available in introductory texts
such as [26]. Our key contribution is formalising and exploiting this spatial knowledge
as modular and extensible common-sense rules in intelligent knowledge-based spatial
assistance systems.

pc
pb

l2

d l1 point
pc d coincidence,
pc
d lAffine
l1 preserve
Fig.p5.
parallelism, and ratios of
pc1 pd pctransformations
ldistances
2
l2 along parallel lines.
pb
pb

3.4

l1

11

l3
(d)

pb p
c
pd

pa
l3

12

Carl Schultz and Mehul Bhatt

Theorem 1 The following qualitative spatial relations are preserved under translation, scale, rotation, and reflection (applied to the embedding space): topology,
mereology, coincidence, collinearity, line parallelism.
Proof. By definition, affine transformations preserve parallelism with respect to
qualitative line orientation, and point coincidence. Due to preservation of point
coincidence and proportions of collinear distances by affine transformations, it
follows that mereological part of and topological contact relations between regions are preserved, i.e. if a mereological or topological relation changes between
regions a, b, then by definition there exists a point p coincident with a such
that the coincidence relation between p and b has changed; but this cannot occur as point coincidence is maintained with affine transformations by definition,
therefore mereological and topological relations are also maintained.
The interaction between spatial relations and transformations is richer than we
have space to elaborate on here, i.e. not all qualitative spatial relations are
preserved under all affine transformations; orientation is not preserved under
reflection (e.g. Figure 5(b) gives a counter example), distance is not preserved
under non-uniform scaling. To summarise, we formalise the following knowledge
as modular commonsense rules in CLP(QS): point-coincidence, line parallelism,
topological and mereological relations are preserved with all affine transformations. Relative orientation changes with reflection, and qualitative distances and
perpendicularity change with non-uniform scaling. Spheres, circles, and rectangles are not preserved with non-uniform scaling, with the exception of axisaligned bounding boxes.
“Trading” Transformations Symmetries are used to eliminate object variables. As a metaphor, unbound variables are replaced by constant values in
“exchange” for transformations. We start with a set of transformations that can
be applied to a configuration: translation, scaling, arbitrary rotation, and horizontal and vertical reflection. We can then “trade” each transformation for an
elimination of variables. Each transformation can only be “spent” once. Theorem 2 presents an instance of such a pruning case.
Table 2 presents a variety of different pruning cases for position variables and
the associated combination of transformations, as illustrated in Figure 6.11 Some
cases require more than one distinct set of parameter restrictions to cover the
set of all position variables due to point coincidence being preserved by affine
transformations. For example, consider case (f): all pairs of points p1 , p2 can
be transformed into any other pair of points pi , pj by translation, rotation, and
scaling, iff p1 = p2 ↔ pi = pj . Thus, to cover all pairs of possible points, we need
to consider two distinct parameter restrictions: pi = pj and pi 6= pj ; we refer to
these as subcases.
Many further pruning cases are identifiable. For example, a version of case (i)
can be defined without reflection by requiring more sub-cases where c4 > c2 and
c4 < c2 . Case (i) can be extended so that all six coordinates of three points
are grounded if we also “exchange” the skew transformation (e.g. applicable to
object domains like triangles or points).
11

All cases have been verified using Reduce as presented in Theorem 2.

Spatial Symmetry Driven Pruning

13

Theorem 2 Any pair of object position variables (x1 , y1 ), (x2 , y2 ) can be transformed into any given position constants (c1 , c2 ), (c3 , c2 ) such that (c1 = c3 ↔
(x1 = x2 ∧ y1 = y2)) by applying: an xy-translation, a rotation about the origin
in the range (0, 2π), and an x-scale.
Proof. The corresponding expression has been verified using the Reduce system
(Redlog quantifier elimination) [15]; all variables are quantified over reals.
∀c1 ∀c2 ∀c3 ∀x1 ∀y1 ∀x2 ∀y2
(c1 = c3 ↔ (x1 = x2 ∧ y1 = y2)) ↔ ∃tx ∃ty ∃dx ∃dy ∃sx
(0 < sx )∧ (d2x +d2y = 1) ∧ 

 
sx 0
dx − dy
tx
let S =
∧ let R =
∧ let T =
∧
0 1
dy dx
ty
 
 
 
 

x2
c3
x1
c1
+T ≡>
= SR
+T ∧
= SR
y2
c2
y1
c2

We can use this pruning case on any spatial constraint graph G where the graph’s
spatial relations are preserved by translation, rotation, and scaling. Given graph
G = (N, E), the following Algorithm applies the pruning case, with selected
constants c1 = 0, c2 = 0, and c3 = 1 or c3 = 0:
1.
2.
3.
4.
5.

select object position variables p1 , p2 from nodes in N
copy G to create G1 , G2
in G1 set p1 = (0, 0), p2 = (1, 0) (case c1 6= c3 )
in G2 set p1 = (0, 0), p2 = (0, 0) (case c1 = c3 )
if the task is:
W2
(a) consistency of G then solve i=1 ∃s Gi (s)
(b) sufficiency, G → G0 , then solve
V2
0
i=1 ¬∃s(Gi (s) ∧ ¬G (s))

In Step 1 any pair of objects can be selected for which their position variables
will be grounded; we also employ policies that target computationally costly
subgraphs (for example, pairs of non-equal circles that share a boundary point
are often good candidates for this pruning case). Having eliminated free variables
from the system of polynomial constraints, the constraints are significantly more
cn
simple to solve. Due to the double exponential complexity O(c12 ) reducing n
has a significant impact on performance; the system may even collapse from
nonlinear constraints to linear (solvable in O(cn )) or constants.
3.5

Combining Symmetry Pruning with Graph Decomposition

In certain cases, spatial constraint graphs can be decomposed into subgraphs
that can be solved independently. For example, subgraphs G1 , G2 can be independently solved if all objects in subgraph G1 are either:
–
–
–
–

disconnected from all objects in subgraph G2 ;
a proper part of some object in G2 ;
left of some segment in G2 ;
only related by relative size to some object in G2 , and so on.

y

y

x1=c1
y2
y1=c

x1=c1
y1=c2

y
x1=c1

x

x

x1=c1

y

x1=c1
x1=c1 y1=c2

y

x1=c1 y
y1=c2

y

y

y

x1=c1
y1=c2

y

y2=c2 y

x
x1=c1
y1=c2

x

(a)
(b)
x
x x1=c1
x
x2x=c
3
x
=c
x
=c
1
1
2
3
x1=c1 y
x1=c
x2=c3
1
y
y
y1=c2 y2=c
y2y=c
2 2
y
1=c
2=c
2 3 x2=c3
x
=c
2
2
y1=c2
y1=c2
y2=c2
y
y
y
y
y
x2=c3 x2=c3 x
x2=c3
x
x
x =c x =c

y

y

x
x
x1=c1 x1=cx21=c3 x2=c3
x2=c2
x1=c1
y1=c2 y1=c2
y1=c2 y1=cy2=c2 y2=c2
x
x x1=c1 x
x x1=c1 xx2=c3 x
x1=c1
=c31 (e)
x2=c3
x1=c1
x1=c1
xx21=c
(f)
y1=c2(d) y =c
y1y=c=c
y2=c2
2
y
y
=c
y
y
1=c2
2
2
1=c2
1
2
21=c
22
y
y
y
y
y
y3=c3
y3=cy3
y3=c4
y3=c4y
y3=c3
y3=cy4
y3=c4y
y3=c4
1

1 1

x

(c)

1

x

CLP(QS). For example, consider Proposition 22 of Book I of Euclid’s Elements
(Figure 7):

=c1
=c2

y2=c2

y3=c4

x
x
x
x
x
x
x1=cx1
x1=cx1
x2x=c
x1=c
x
3 1
y 1 y x1=c1
1y=c
3
y x2x=c
x1=c1 x2=c
2
x2=c3
y
1=c1
y
x1=c1 x2=c
y
=c
2
y
=c
3
3
3
3
y
=c
x1=c1 x2=c12 2 x2=c
3 2
y
y
=c
y1=c
y
=c
x2y=c
1=c2
2y
2
y
=c
y3=c4 y3=c
3
4
3
3
4
=c
y
=c
1
2
2y =c
2
x2=c3
1=c2
y2=c2
1
2
y
y
y
y3=c3 y (h) y
y
y
(g)
y3=c(i)
y3=c4
4
y
y
y3=c3
y3=c3
yx3=c4
y3=cx4
y3=c4x y3x=c4
x
x1=c1 x1=c1
x1=c1 x1=cx12=c3 x2=c3
x2=c2
x2=c
1 2 position
1=cpruning
1 x1=c
Fig. 6. Casesxxfor
parameters.
x22=c3 x2=c3
x y1=c2 y1=c
x y1=c2 y1=cy2 =c2 y2=c2
x
x
x1=c1
xx2=c3
x
x x1=c1 pruning
In such cases wex1can
in
each
independent
x
=c1 reapply
x2=c2 x1spatial
xsymmetry
=c
=c1
1
1 y1=c2
=c31 y1=c
x22=c3 y2=c2
xx21=c
x2=c3 x1=c1
=c
x2=c2
x1=c1 x2x=c
1this
2 1 commonsense
sub-graph;
knowledge
is3 modularly
formalised
=c32 x2=c
yspatial
xy21=c
1=c2
=c22 within
y2=c2
y1=c
yy21=c
2

2=c2

y

y2=c2 y

x
x
x
x
x
x
x
x
x
14
Bhatt
y Carly Schultz and
y 1 xy2=c2 x1=c1
y
y
x1=cMehul
1 x2=c
x12=c
x
=c
1
1
x1=c1
x1=cx11x=c
1 1 x2=c2
1=c
x1=c1 x1=c1
y1=c2 y1=c2
y
y
y
y
y
y
y
y
y
y
y
y
y2=c
y2=c2
x1=c1
x 1=c1 x x1=c1
x
x 2y2=c
x
x2
x1=c1 x1=c1
x1=c1
y1=c2 y1=c2
y1=c2
x1=c1 x1=c
x2=c
1 2 x2=c2
x
x
x
x
xy
x
x
x
x
x
x
x
y
y
x2=c3 y x2=c3 y
x
=c
x
=c
x
=c
1 2 2 x21=c1
x1=c1 1 1
x1=c1 x2x=c
1=c
2 1 1x2=c
x2=c3

y
x

x

2=c3

y
x1=c1

y3=c4
x
x2=c3

y

y3=c4

Constructing a triangle from three segments. Given three line segments lab , lcd ,
x
x1=cl1ef , draw
x2=c3 a line through four collinear points p1 , . . . , p4 such that |(p1 , p2 )| = |lab |,
, p =c
)|2 = |lcd |, |(p3 , p4 )| = |lef |. Draw circle ca centred on p2 , coincident with
y1=c|(p
2 2 y23
p1 . Draw circle cb centred on p3 coincident with p4 . Draw p5 coincident with
ca and cb . The triangle p2 , p3 , p5 has side lengths such that |(p2 , p3 )| = |lcd |,
|(p3 , p5 )| = |lef |, |(p5 , p2 )| = |lab |.
In this example, the three segments lab , lcd , lef and the remaining objects are
only related by the distances between their end points. That is, the relative
position and orientation of lab , lcd , lef is not relevant to the consistency of the
spatial graph; we only need to explore all combinations of segment lengths. Thus
the solver decomposes the graph into four sub-graphs: (1) lab (2) lcd (3) lef , and
(4) p1 , . . . , p5 , ca , cb . In subgraphs (1),(2),(3) it “trades” translation and rotation
to ground pa = pc = pe = (0, 0), and yb = yd = yf = 0 and keeps x-scale to cover
all possible combinations of segment lengths, i.e. xb , xd , xf are free variables. In
subgraph (4) CLP(QS) applies the pruning case of Theorem 2 by grounding
p1 , p4 .

Spatial Symmetry Driven Pruning
Case Parameter restrictions

15

Traded transformations

a
b
c
d
e

x 1 = c1
x-translate
x 1 = c 1 , y1 = c2
xy-translate
x1 = c1 , x2 = c2 , (i) c1 6= c2 (ii) c1 = c2
x-translate, rotate ⇡, x-scale
x 1 = c 1 , y2 = c2
xy-translate
x 1 = c 1 , y1 = c2 , x 2 = c3 ,
xy-translate, rotate ⇡, x-scale
(i) c1 6= c3 (ii) c1 = c3
f
x 1 = c 1 , y1 = c2 , x 2 = c3 , y2 = c 2 ,
xy-translate, rotate (0, 2⇡), x-scale
Spatial Symmetry Driven Pruning
15
(i) c1 6= c3 (ii) c1 = c3
g
x 1 = c 1 , x 2 = c2 , y3 = c3
xy-translate, rotate ⇡, x-scale
(i) c1 6= c2 (ii) c1 = c2
Case
Parameter
restrictions
Traded transformations
h⇤ x
xy-translate,
rotate ⇡, xy-scale,
1 = c 1 , y1 = c2 , x 2 = c3 , y3 = c 4
(i)
a
x1 =c1c16= c3 ^ c2 6= c4 (ii) c1 = c3 ^ c2 6= c4 y-reflect
x-translate
(iii)
^ c2 = c4 (iv) c1 = c3 ^ c2 = c4 xy-translate
b
x1 =c1c16=, yc13 =
i c⇤
x 1 = c1 , y
= cc21, =
y3 c=
rotateπ,(0,
2⇡), xy-scale,
x12 =
= cc22,, x
(i)
c1 c6=
x-translate, rotate
x-scale
2 =
3 ,cy22(ii)
2 c4 xy-translate,
(i)
c
=
6
c
^ c2 6= c4 (ii) c1 6= c3 ^ c2 = c4 y-reflect
d
x1 = 1c1 , y23 =
xy-translate
(iii)
c
=
c
^
c
=
c
e
x1 = 1c1 , y13 = 2 , x2 4= c3 ,
xy-translate, rotate π, x-scale
(i) c1 for
6= c3pruning
(ii) c1 = parameters
c3
Table 2. Cases
for one position point (a,b), two position points
f
x1 = c1 , y1 = c2 , x2 = c3 , y2 = c2 ,
xy-translate, rotate (0, 2π), x-scale
(c-f ), three (i)
position
(g-i).
c1 6= c3points
(ii) c1 =
c3 Cases marked with ⇤ require arbitrary scaling (i.e. both
uniformg andx1non-uniform).
= c1 , x2 = c2 , y3 = c3
xy-translate, rotate π, x-scale
(i) c1 6= c2 (ii) c1 = c2
h ∗ x1 = c1 , y1 = c2 , x2 = c3 , y3 = c4
xy-translate, rotate π, xy-scale,
(i) c1 6= c3 ∧ c2 6= c4 (ii) c1 = c3 ∧ c2 6= c4 y-reflect p5
ab
(iii) c1 6= c3 ∧ c2 = c4 (iv) c1 = c3 ∧ c2 = c4
i∗
x1 = c1 , y1 = c2 , x2 = c3 , y2 = c2 , y3 = c4 xy-translate, rotate (0, 2π), xy-scale,
(i) c1 6= c3 ∧ c2 6= c4 (ii) c1cd
6= c3 ∧ c2 = c4 y-reflect
p1
p2 p3
p4
(iii) c1 = c3 ∧ c2 = c4

l
l

Table 2. Cases for pruning parameters
lef for one position point (a,b), two position points
(c-f ), three position points (g-i). Cases marked with ∗ require arbitrary scaling (i.e. both
uniform and non-uniform).
Fig. 7. Constructing a triangle by decomposing the spatial constraint graph.
?- Sab = segment(Pa,Pb), Scd = segment(Pc,Pd), Sef = segment(Pe,Pf),
| S12 = segment(P1,P2), S23 = segment(P2,P3), S34 = segment(P3,P4),
| S14 = segment(P1,P4),
| coincident(P2,S14), coincident(P3,S14),
|
| length_dim(equal, S12, Sab),
| length_dim(equal, S23, Scd),
| length_dim(equal, S34, Sef),
|
| Ca=circle(P2,_),
coincident(P1,Ca),
| Cb=circle(P3,_),
coincident(P4,Cb),
| coincident(P5,Ca), coincident(P5,Cb),
| S35 = segment(P3,P5), S52 = segment(P5,P2),
|
| %% triangle
| length_dim(equal, S23, Scd),
| length_dim(equal, S35, Sef),
| length_dim(equal, S52, Sab).
true.
...
| (length_dim(not_equal, S23, Scd);
|
length_dim(not_equal, S35, Sef);
|
length_dim(not_equal, S52, Sab)).
false.

4

Application-Driven lUse
Cases
ab

p5

lcd

p1 ofp2mereology,
p3
p4 ruler and compass,
We present problem instances in the classes
and contact. Table 3 presents lthe
ef experiment time results of CLP(QS) using
symmetry pruning compared with existing systems: z3 SMT solver, Redlog real
quantifier
(ina the
Reduce
computer algebra
system)
[12], and
the reFig. 7.elimination
Constructing
triangle
by decomposing
the spatial
constraint
graph.
lation algebraic qualitative spatial reasoners GQR [13] and SparQ [35]. CLP(QS)
uses z3 to solve polynomial constraints (after our pruning), thus z3 is the most

4

Application-Driven Use Cases

We present problem instances in the classes of mereology, ruler and compass,
and contact. Table 3 presents the experiment time results of CLP(QS) using
symmetry pruning compared with existing systems: z3 SMT solver, Redlog real

16

Carl Schultz and Mehul Bhatt

quantifier elimination (in the Reduce computer algebra system) [15], and the relation algebraic qualitative spatial reasoners GQR [16] and SparQ [39]. CLP(QS)
uses z3 to solve polynomial constraints (after our pruning), thus z3 is the most
direct comparison. Experiments were run on a MacBookPro, OS X 10.8.5, 2.6
GHz Intel Core i7. The empirical results show that no other spatial reasoning system exists (to the best of our knowledge) that can solve the range of
problems presented in this section, and in cases where solvers are applicable,
CLP(QS) with spatial pruning solves those problems significantly faster than
other systems.
Problem
Aligned Concentric
Boundary Concentric
Mereologically Concentric
Angle Bisector
Sphere Contact

CLP(QS)
z3 Redlog GQR SparQ
6.831
47.651 time out n/a
n/a
2.036 time out time out n/a
n/a
0.105
0.373 time out n/a
n/a
0.931 time out time out n/a
n/a
0.004 time out time out fail
fail

Table 3. Time (in seconds) to solve benchmark problems using CLP(QS) with pruning compared to z3 SMT solver, Redlog (Reduce) quantifier elimination, and GQR and
SparQ relation algebraic solvers. Time out was issued after a running time of 10 minutes. Failure ( fail) indicates that the incorrect result was given. Not applicable ( n/a)
indicates that the problem could not be expressed using the given system.

B A Z
4.1

Spatial Theorem Proving: Geometry of Solids

P
A
Tarski [36] shows that a geometric point Spatial
can be Symmetry
defined byDriven
a language
of mereoPruning
17
B concenlogical relations over spheres. TheBidea
isZto distinguish when spheres are
A
A
tric, and to define a geometric point as the point of convergence. Borgo [8] shows h
I
B
that this can be accomplished with aPlanguage of mereology over hypercubes. We
will use CLP(QS) Pto prove that the definitions are sound for rotatable squares.
As a preliminary we need to determine whetherAthe intersectionAof two squares
A
is non-square A(Figure 8) [34]. Given two squares
a, b, the
B
B intersection is non- B
B
B
square if a partially overlaps b (Table 1) and either
(a) a and b are not aligned,
P
xva 6= xv(a)
orA(b)
width
height
equal,
andthe
B are
(b)and
A and
B areof the
(c) intersection
A is bound- are
(d)
A and
B arewI 6=
hI not
I hI ,
b
non-concentric
concentric
ary concentric rotated concensuch that
B. · p , v tric.
A
wI = min(v · p2a , v · p2b )Awith
− max(v
· p1b )
1a
B

A

0
0 and rotated (c),(d)
0
0
Fig. 9. Characterising
aligned
concentric
hI = min(v
· p(a),(b)
· p1b ) squares using
4a , v · p
4b ) − max(v · p1a , v
B 2013])
wI
mereology (reproduced from [Borgo,

Aligned Concentric. Two squares A, B are aligned and concentric if: A is part of
B and there does not exist a square P such that (a) P is covertex with B, and
(b) the intersection of P and A is not a square (Figure 9).
|
|
|
|
|
|
|

aligned_concentric(A,B) :mereology(part_of, A,B),
not((
P=square(_,_,_),
covertex(P,B),
intersection(non_square,A,P).
)).

We use CLP(QS) to prove that the definition is suﬃcient, by contradiction; two
squares are covertex if they are aligned and share a vertex, and the relation
concentric is the geometric definition of concentricity in Table 1 that is used to
evaluate the mereological definition of concentricity:
?- A=square(_,_,_),
| B=square(_,_,_),
| aligned(A,B),
| not_concentric(A,B),
| aligned_concentric(A,B).
false.

Boundary Concentric. Square A is boundary concentric with square B if: A is
proper part of B and there does not exist a square Z such that (a) Z is proper
part of B (b) A is part of Z, and (c) Z is not part of A (Figure 9).

B
I
A
wI

B
I
A
B A Z
Spatial Symmetry Driven Pruning
P

B

Spatial Symmetry Driven Pruning

B

B AhIZ

A
B
P
A
B

A
(a) A, B B are

A

A
A

B

not

P(a) A andaligned.
B are (b) A and B are
A
B

wI
(b)
P hI 6= wI

A

17

B

I

P

I

17

B
hI
A

B A Z
A

B

B

(c) A is bound- (d)
hI A and B are A I
non-concentric
concentric
ary concentric rotated concenB
A squares
ZAwith B.
Fig. 8. IntersectionBI of
A, B is non-square.
tric.
A
B

A

Fig. 9. Characterising aligned (a),(b) Pand rotated (c),(d) concentric squares using
B
B 2013])
P
wI
mereology (reproduced
from [Borgo,

A and concentricA if: A is part of
Aligned Concentric. Two squares A, B are aligned
A
h
I
I
A
B and there does not exist a square P suchB that (a) P isBcovertex
with B, and B
B
B
(b) the intersection of P and A is not a square
P (Figure 9).

A (d)
boundhI A and B are

(a) A and B are :(b) A and B are (c) A is
| aligned_concentric(A,B)
non-concentricA,B),concentric
ary concentric
|
mereology(part_of,
|
not((
Awith B.
|
P=square(_,_,_),
A
|
covertex(P,B),
B
|
intersection(non_square,A,P).
Fig.
9.
Characterising aligned (a),(b) and rotated (c),(d)
|
)).
B
mereology (reproduced from [Borgo, 2013])

rotated concentric.
A

I

wI

concentric squares using

wI

We use CLP(QS) to prove that the definition is sufficient,
suﬃcient, by contradiction; two
squares are covertex if they are aligned and share a vertex, and the relation
concentric is the geometric definition of concentricity in Table 1 that is used to
evaluate the mereological definition of concentricity:
?- A=square(_,_,_),
| B=square(_,_,_),
| aligned(A,B),
| not_concentric(A,B),
| aligned_concentric(A,B).
false.

Boundary Concentric. Square A is boundary concentric with square B if: A is
proper part of B and there does not exist a square Z such that (a) Z is proper
part of B (b) A is part of Z, and (c) Z is not part of A (Figure 9).
|
|
|
|
|
|
|
|

I

boundary_concentric(A,B) :mereology(proper_part,A,B),
not((
Z = square(_,_,_)
mereology(proper_part, Z,B),
mereology(part_of, A,Z),
mereology(not_part_of, Z,A),
)).

?- A=square(_,_,_),
| B=square(_,_,_),
| not_aligned(A,B),
| not_concentric(A,B),
| boundary_concentric(A,B).
false.

Mereologically Concentric. Squares A, B are mereologically concentric if: A, B
are aligned concentric or there exists Q such that (a) Q is boundary concentric
with B and Q is aligned concentric with A or (b) Q is boundary concentric with
A and Q is aligned concentric with B.

wI
B
hI

I
A
wI

18

Carl Schultz and Mehul Bhatt

Mereologically Concentric. Squares A, B are mereologically concentric if: A, B

18
Carl Schultz
Mehul
Bhatt
are aligned concentric or there exists
Q suchand
that
(a) Q
is boundary concentric
with B and Q is aligned concentric
A orand
(b)Mehul
Q is boundary
concentric with
18
Carlwith
Schultz
Bhatt

A and Q
is aligned
concentric with
B.
Having
proved
the mereological
definitions
of aligned and boundary concentricity,
we
can replace
these
with more eﬃcient
geometric
definitions
from concentricity,
Table 1 when
Having
proved the
mereological
definitions
of aligned
and boundary
proving
mereological
concentricity.
we can replace
these with
more eﬃcient
efficient geometric definitions from Table 1 when
proving
mereological concentricity.
| g_aligned_concentric(A,B)
:|
aligned(A,B), concentric(A,B).
|| g_aligned_concentric(A,B) :aligned(A,B), concentric(A,B).
|| g_boundary_concentric(A,B)
:|| mereology(boundary_part, A,B).
| g_boundary_concentric(A,B) :|
mereology(boundary_part, A,B).
| m_concentric(A,B) :|
g_aligned_concentric(A,B)
:|| m_concentric(A,B)
;
|| Qg_aligned_concentric(A,B)
= square(_,_,_),
;
|| g_boundary_concentric(Q,B),
Q = square(_,_,_),
|| g_aligned_concentric(Q,A)
|| ;g_boundary_concentric(Q,B),
|| Qg_aligned_concentric(Q,A)
= square(_,_,_),
;
|| g_boundary_concentric(Q,A),
|
Q
= square(_,_,_),
|
g_aligned_concentric(Q,B).
|
g_boundary_concentric(Q,A),
|
g_aligned_concentric(Q,B).
?- A=square(_,_,_),
| B=square(_,_,_),
A=square(_,_,_),
|?- not_concentric(A,B),
B=square(_,_,_),
|| m_concentric(A,B).
| not_concentric(A,B),
false.
| m_concentric(A,B).
false.

4.2 Didactics: Ruler–Compass and Contact Problems
4.2 Didactics: Ruler–Compass and Contact Problems
4.2 Didactics: Ruler–Compass and Contact Problems
Angle
Angle Bisector.
Bisector. Let
Let llaa,, llbb be line segments that share an endpoint at p. Draw
circle
at
at pa andthat
lb atshare
pb . Draw
circle ccBisector.
at p.
p. Circle
Circle
intersects
circles c aatatp.p aDraw
and
Angle
Let cclaintersects
, lb be linelaa segments
an endpoint
circle
at
ppbb Circle
such
pp is coincident
both
c
,
c
.
Circles
circle ccbbat
at p.
such that
that
c
and
c
intersect
a
b
c intersects
la at pwith
and
l
at
p
.
Draw
circles
c
at
p
a
b
a
b
b
a
a and
at
from p with
to pcboth
bisects
at pp and
and
The
line
segment
angle
between
l
and
lbb
circle
cb atppccp..bThe
suchline
thatsegment
p is coincident
ca , cthe
.
Circles
c
and
c
intersect
a
b
a
b
(Figure
(Figure
10).
at
p and10).
pc . The line segment from p to pc bisects the angle between la and lb
(Figure
10).
We
to
We use
use CLP(QS)
CLP(QS)
to prove
prove that the definition is suﬃcient.
sufficient. The relation bisects is
used
for
evaluation
by
checking
if
the
midpoint
of
(pa ,pb ) isThe
used
for
evaluation
by
checking
collinear
with
lc (i.e.
We use CLP(QS) to prove that the definition is suﬃcient.
relation
bisects
is
idealised
rulers
cannot
directly
measure
the
midpoint
idealised
rulers
cannot
directly
of
a
line).
An
interactive
used for evaluation by checking if the midpoint of (pa ,pb ) is collinear with lc (i.e.
diagram
automatically
generated
encodes
diagram is
is then
thencannot
automatically
specified
program
idealised
rulers
directly measure
thethat
midpoint
of the
a line).
An interactive
(using
system);
Figure 11.that encodes the specified program
(using the
theisFreeCAD
FreeCAD
system); seegenerated
diagram
then automatically
(using
FreeCAD system);
see Figure 11.
?- La = the
segment(P,_),Lb
= segment(P,_),
| orientation(not_parallel, La, Lb),
segment(P,_),Lb = segment(P,_),
|?- CLa= =circle(P,_),
orientation(not_parallel, La, Lb),
|| coincident(Pa,La),coincident(Pa,C),
C = circle(P,_),
|| coincident(Pb,Lb),coincident(Pb,C),
coincident(Pa,La),coincident(Pa,C),
|| Ca=circle(Pa,_),
Cb=circle(Pb,_),
coincident(Pb,Lb),coincident(Pb,C),
|| coincident(Pa,Ca),coincident(Pa,Cb),
|
Ca=circle(Pa,_),
Cb=circle(Pb,_),
| coincident(Pc,Ca),coincident(Pc,Cb),
coincident(Pa,Ca),coincident(Pa,Cb),
|| not_equal(P,Pc),
coincident(Pc,Ca),coincident(Pc,Cb),
|| Lc=segment(P,Pc),
not_equal(P,Pc),
|| bisects(segment(Pa,Pb),Lc).
| Lc=segment(P,Pc),
true.
| bisects(segment(Pa,Pb),Lc).
...
|true.not_bisects(segment(Pa,Pb),Lc).
...
false.
|
not_bisects(segment(Pa,Pb),Lc).
false.

Sphere contact. Determine the maximum number of same-sized mutually touching
spheres
(Figure
4 - note
no numeric
information
about
the spheres
is
Sphere
contact.
Determine
thethat
maximum
number
of same-sized
mutually
touchgiven
in this(Figure
benchmark
problem).
ing spheres
4 - note
that no numeric information about the spheres is
given in this benchmark problem).

Lb
Cb
C
La

Ca

P
Spatial Symmetry Driven Pruning

Lb

19

Lb
Cb

C
La
P

Lc

C
Ca

P

Pc

La

(a)

(b)

Fig. 10. Ruler and compass method for angle bisection. Line Lc bisects the angle
between lines La , Lb .

Lc
Pc

(a)

(b)

(c)

Fig. 11. Interactive diagram encoding the student’s constructive proof of Euclid’s angle bisector theorem; as the student manipulates figures in the diagram, the other
geometries are automatically updated to maintain the specified qualitative constraints.

Sphere contact. Determine the maximum number of same-sized mutually touching spheres (Figure 4 - note that no numeric information about the spheres is
given in this benchmark problem).

5

Conclusions

Affine transformations provide an effective and interesting class of symmetries
that can be used for pruning across a range of qualitative spatial relations.
To summarise, we formalise the following knowledge as modular commonsense
rules in CLP(QS): point-coincidence, line parallelism, topological and mereological relations are preserved with all affine transformations. Relative orientation
changes with reflection, and qualitative distances and perpendicularity change
with non-uniform scaling. Spheres, circles, and rectangles are not preserved with
non-uniform scaling, with the exception of axis-aligned bounding boxes. Our algorithm is simple to implement, and is easily extended to handle more pruning
cases.
Theoretical and empirical results show that our method of pruning yields an
improvement in performance by orders of magnitude over standard polynomial
encodings without loss of soundness, thus increasing the horizon of spatial problems solvable with any polynomial constraint solver. Furthermore, the declaratively formalised knowledge about pruning strategies is available to be utilised in

20

Carl Schultz and Mehul Bhatt

a modular manner within other knowledge representation and reasoning frameworks that rely on specialised SMT solvers etc, e.g., in the manner demonstrated
in ASPMT(QS) [38], which is a specialised non-monotonic spatial reasoning system built on top of answer set programming modulo theories.

References
[1] M. Aiello, I. E. Pratt-Hartmann, and J. F. v. Benthem. Handbook of Spatial
Logics. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2007. ISBN
978-1-4020-5586-7.
[2] D. S. Arnon, G. E. Collins, and S. McCallum. Cylindrical Algebraic Decomposition I: The basic algorithm. SIAM Journal on Computing, 13(4):
865–877, 1984.
[3] M. Bhatt and J. O. Wallgrün. Geospatial narratives and their spatiotemporal dynamics: Commonsense reasoning for high-level analyses in geographic information systems. ISPRS Int. J. Geo-Information, 3(1):166–
205, 2014. doi: 10.3390/ijgi3010166. URL http://dx.doi.org/10.3390/
ijgi3010166.
[4] M. Bhatt, J. H. Lee, and C. Schultz. CLP(QS): A Declarative Spatial Reasoning Framework. In Proceedings of the 10th international conference on
Spatial information theory, COSIT’11, pages 210–230, Berlin, Heidelberg,
2011. Springer-Verlag. ISBN 978-3-642-23195-7.
[5] M. Bhatt, C. Schultz, and C. Freksa. The ‘Space’ in Spatial Assistance
Systems: Conception, Formalisation and Computation. In T. Tenbrink,
J. Wiener, and C. Claramunt, editors, Representing space in cognition: Interrelations of behavior, language, and formal models. Series: Explorations
in Language and Space. 978-0-19-967991-1, Oxford University Press, 2013.
[6] M. Bhatt, J. Suchan, and C. Schultz. Cognitive Interpretation of Everyday
Activities – Toward Perceptual Narrative Based Visuo-Spatial Scene Interpretation. In M. Finlayson, B. Fisseni, B. Loewe, and J. C. Meister, editors,
Computational Models of Narrative (CMN) 2013., a satellite workshop of
CogSci 2013: The 35th meeting of the Cognitive Science Society., Dagstuhl,
Germany, 2013. OpenAccess Series in Informatics (OASIcs).
[7] M. Bhatt, C. P. L. Schultz, and M. Thosar. Computing narratives of cognitive user experience for building design analysis: KR for industry scale
computer-aided architecture design. In C. Baral, G. D. Giacomo, and
T. Eiter, editors, Principles of Knowledge Representation and Reasoning:
Proceedings of the Fourteenth International Conference, KR 2014, Vienna,
Austria, July 20-24, 2014. AAAI Press, 2014. ISBN 978-1-57735-657-8.
[8] S. Borgo. Spheres, cubes and simplexes in mereogeometry. Logic and Logical
Philosophy, 22(3):255–293, 2013.
[9] D. Bouhineau. Solving geometrical constraint systems using CLP based on
linear constraint solver. In Artificial Intelligence and Symbolic Mathematical
Computation, pages 274–288. Springer, 1996.
[10] D. Bouhineau, L. Trilling, and J. Cohen. An application of CLP: Checking
the correctness of theorems in geometry. Constraints, 4(4):383–405, 1999.
[11] B. Buchberger. Bruno Buchberger’s PhD thesis 1965: an algorithm for
finding the basis elements of the residue class ring of a zero dimensional
polynomial ideal (English translation). Journal of symbolic computation,
41(3):475–511, 2006.

Spatial Symmetry Driven Pruning

21

[12] S.-C. Chou. Mechanical geometry theorem proving, volume 41. Springer
Science & Business Media, 1988.
[13] G. E. Collins. Quantifier elimination for real closed fields by cylindrical
algebraic decompostion. In Automata Theory and Formal Languages 2nd
GI Conference Kaiserslautern, May 20–23, 1975, pages 134–183. Springer,
1975.
[14] G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for
quantifier elimination. Journal of Symbolic Computation, 12(3):299 – 328,
1991. ISSN 0747-7171.
[15] A. Dolzmann, A. Seidl, and T. Sturm. REDLOG User Manual, Apr. 2004.
Edition 3.0.
[16] Z. Gantner, M. Westphal, and S. Wölfl. GQR-A fast reasoner for binary
qualitative constraint calculi. In Proc. of AAAI, volume 8, 2008.
[17] N. Hadas, R. Hershkowitz, and B. B. Schwarz. The role of contradiction
and uncertainty in promoting the need to prove in dynamic geometry environments. Educational Studies in Mathematics, 44(1-2):127–150, 2000.
[18] P. Haunold, S. Grumbach, G. Kuper, and Z. Lacroix. Linear constraints:
Geometric objects represented by inequalitiesl. In S. C. Hirtle and A. U.
Frank, editors, Spatial Information Theory A Theoretical Basis for GIS,
volume 1329 of Lecture Notes in Computer Science, pages 429–440. Springer
Berlin Heidelberg, 1997. ISBN 978-3-540-63623-6.
[19] J. Jaffar and M. J. Maher. Constraint logic programming: A survey. The
journal of logic programming, 19:503–581, 1994.
[20] P. C. Kanellakis, G. M. Kuper, and P. Z. Revesz. Constraint query languages. In D. J. Rosenkrantz and Y. Sagiv, editors, Proceedings of the Ninth
ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems, April 2-4, 1990, Nashville, Tennessee, USA, pages 299–313. ACM
Press, 1990. ISBN 0-89791-352-3.
[21] D. Kapur and J. L. Mundy, editors. Geometric Reasoning. MIT Press,
Cambridge, MA, USA, 1988. ISBN 0-262-61058-2.
[22] P. B. Ladkin and R. D. Maddux. On binary constraint problems. Journal
of the ACM (JACM), 41(3):435–469, 1994.
[23] J. H. Lee. The complexity of reasoning with relative directions. In 21st
European Conference on Artificial Intelligence (ECAI 2014), 2014.
[24] G. Ligozat. Qualitative Spatial and Temporal Reasoning. Wiley-ISTE, 2011.
[25] G. F. Ligozat. Qualitative triangulation for spatial reasoning. In Spatial
Information Theory A Theoretical Basis for GIS, pages 54–68. Springer,
1993.
[26] G. E. Martin. Transformation geometry: An introduction to symmetry.
Springer, 1982.
[27] J. C. Owen. Algebraic solution for geometry from dimensional constraints.
In Proceedings of the first ACM symposium on Solid modeling foundations
and CAD/CAM applications, pages 397–407. ACM, 1991.
[28] G. Pesant and M. Boyer. QUAD-CLP (R): Adding the power of quadratic
constraints. In Principles and Practice of Constraint Programming, pages
95–108. Springer, 1994.
[29] G. Pesant and M. Boyer. Reasoning about solids using constraint logic
programming. Journal of Automated Reasoning, 22(3):241–262, 1999.
[30] D. A. Randell, A. G. Cohn, and Z. Cui. Computing transitivity tables: A
challenge for automated theorem provers. In 11th International Conference
on Automated Deduction (CADE-11), pages 786–790, 1992.

22

Carl Schultz and Mehul Bhatt

[31] S. Ratschan. Approximate quantified constraint solving by cylindrical box
decomposition. Reliable Computing, 8(1):21–42, 2002.
[32] S. Ratschan. Efficient solving of quantified inequality constraints over the
real numbers. ACM Transactions on Computational Logic (TOCL), 7(4):
723–748, 2006.
[33] C. Schultz and M. Bhatt. Towards a Declarative Spatial Reasoning System.
In 20th European Conference on Artificial Intelligence (ECAI 2012), 2012.
[34] C. Schultz and M. Bhatt. Declarative spatial reasoning with boolean combinations of axis-aligned rectangular polytopes. In ECAI 2014 - 21st European
Conference on Artificial Intelligence, pages 795–800, 2014.
[35] C. Schultz, M. Bhatt, and A. Borrmann. Bridging qualitative spatial constraints and parametric design - a use case with visibility constraints. In
EG-ICE: 21st International Workshop - Intelligent Computing in Engineering 2014, 2014.
[36] A. Tarski. A general theorem concerning primitive notions of Euclidean
geometry. Indagationes Mathematicae, 18(468):74, 1956.
[37] A. C. Varzi. Parts, wholes, and part-whole relations: The prospects of
mereotopology. Data & Knowledge Engineering, 20(3):259–286, 1996.
[38] P. Walega, M. Bhatt, and C. Schultz. ASPMT(QS): Non-Monotonic Spatial
Reasoning with Answer Set Programming Modulo Theories. In LPNMR:
Logic Programming and Nonmonotonic Reasoning - 13th International Conference, 2015. URL http://lpnmr2015.mat.unical.it.
[39] J. O. Wallgrün, L. Frommberger, D. Wolter, F. Dylla, and C. Freksa. Qualitative Spatial Representation and Reasoning in the SparQ-Toolbox. In
T. Barkowsky, M. Knauff, G. Ligozat, and D. Montello, editors, Spatial
Cognition V: Reasoning, Action, Interaction, volume 4387 of Lecture Notes
in Computer Science, pages 39–58. Springer, 2007.
[40] W. Wenjun. Basic principles of mechanical theorem proving in elementary
geometries. Journal of Systems Sciences & Mathematical Sciences, 4(3):
207–235, 1984.

