Summary Description of Region Based Geometry Automated Reasoning 2020/21
February 12, 2021
1 Background
This coursework is based on the paper Region Based Qualitative Geometry by Bennett et al. [3]. However, due to their use of unfamiliar notation and a number of typographical errors, we have produced this document to summarise the parts of the work that you will be mechanising in Is- abelle/HOL. You may refer to their paper, as well as their shorter summary [2] and categoricity proof [1], for further detail.1
“We present a highly expressive logical language for describing qualitative configurations of spatial regions. We call the theory Region Based Geometry (RBG). Our axiomati- sation is based on Tarski’s Geometry of Solids, in which the parthood relation and the concept of sphere are taken as primitive. We show that our theory is categorical: all models are isomorphic to a classical interpretation in terms of Cartesian space over R.
We investigate the 2nd-order character of RBG and prove incompleteness of some weaker 1st-order variants. We show that within this theory the concept of sphere and congruence relation are interdefinable. We indicate how our theory might be applied to practical problems in knowledge representation by defiing concepts that can be used for representing and reasoning about the motion of rigid bodies within a confining environment.”
As you can see from the abstract above, the authors were principally concerned with the properties of the axiom system, such as consistency, decidability, completeness, and categoricity, not reasoning with the axiom system2. These properties are outside the scope of this coursework, but we will be proving various properties about n-regions and n-spheres (where n is some fixed dimensionality, implicit in the axioms) which are essential to their proofs. We will not be able to explore their qualitative kinematics for RBG within the scope of this coursework. The “qualitative” aspect of RBG is to do with the primitive concepts used and the basic definitions, which are closer to an intuitive understanding of space and how its parts are related than the traditional coordinate- geometry-influenced approach of focusing on points as at least one of the primitive concepts. With that said, they note:
1If you do decide to consult their papers, note that their notation, axioms, and some definitions are inconsistent between the three papers.
2Nor are they concerned with the independence of the system; that is, no axiom can be proved by a set of any others. They note themselves that A1 is redundant with A7.
1
“However, whether a theory is ‘qualitative’ or ‘quantitative’ is a rather subtle issue and may not be apparent from its primitive vocabulary. As we have seen, although RBG is based on ostensibly qualitative concepts, it is sufficiently rich that coordinate systems and metrical relationships are in fact definable.”
Axiomatic geometry has been a persistent feature of mathematics going back to at least Hilbert and even further back to Euclid. One starts with some “primitive” constants and relations, for us regions and parthood and sphere, for others some options are betweenness or congruence and points, lines, planes, and/or surfaces, and characterise these constants and relations using a consistent set of axioms using some base logical theory like first-order logic with set theory or higher-order logic. There are even axiomatic foundations for Minkowski spacetime, which forms the basis for special relativity, in terms of paths, events, and betweenness.
Among other things, the approach allows one to clarify the foundations of a theory, explore subtly different foundations by tweaking the set of axioms (one can arrive at hyperbolic geometry via Euclidean geometry in this way by dropping the parallel postulate), and work with the theory on a purely syntactic level using automated theorem proving tools.
2 Mereology
B C
D
A
E
Figure 1: Consider what mereological relations the regions A, B, C, D, and E are in with respect to parthood and the following definitions.
Mereology describes regions in terms of parthood. We have two primitive concepts, a set of regions and a parthood relation, (R, ⊑). It consists of just two axioms (where the domain is R):
Axiom 1 (transitivity). ∀xyz. x ⊑ y ∧ y ⊑ z → x ⊑ z
Axiom 2 (unique summation). ∀α. α ̸= {} → ∃!x. α x
Which we can break down into three axioms as in the paper, to isolate the specific uses of uniqueness:
2
Axiom1(transitivity). ∀xyz.x⊑y∧y⊑z→x⊑z Axiom 2 (exists summation). ∀α. α ̸= {} → ∃x. α x
Axiom 2’ (unique summation). ∀αxy. α x ∧ α y → x = y
Bennett et al. provide a substantial number of definitions, though we will only be using the
definitions needed for writing the axioms above and the proofs that we will be tackling: Definition1(properparthood). xyiffx⊑y∧x̸=y
Definition 2 (overlapping regions). x ⌢ y iff ∃z. z ⊑ x ∧ z ⊑ y
Definition 3 (disjoint regions). x ≍ y iff ¬ x ⌢ y
Definition 4 (partially overlapping regions). x ∼⌢ y iff x ⌢ y ∧ ¬x ⊑ y ∧ ¬y ⊑ x Definition5(summingregions). αxiff(∀y∈α.y⊑x)∧(∀y.y⊑x→∃z∈α.y⌢z) 3 Region Based Geometry
We now move to Region Based Geometry (RBG). Here we introduce the notion of spheres by use of a predicate S(x) which returns true iff region x is a sphere. We will present all of the axioms, though only a few are necessary for the theorems we will be proving. First the necessary definitions:
Definition 6 (all spheres). ∀◦x. P(x) iff ∀x. S(x) → P(x) Definition 7 (exists sphere). ∃◦ x. P (x) iff ∃x. S (x) ∧ P (x)
Definition8(externaltangency). ET(a,b)iffS(a)∧S(b)∧a≍b∧(∀◦xy.a⊑x∧a⊑y∧b≍ x ∧ b ≍ y → x ⊑ y ∨ y ⊑ x)
3
Definition 9 (internal tangency). IT(a,b) iff S(a)∧S(b)∧a b∧(∀◦xy. a ⊑ x∧a ⊑ y∧x ⊑ b ∧ y ⊑ b → x ⊑ y ∨ y ⊑ x)
Definition 10 (external diametricity). ED(a, b, c) iff ET (a, c) ∧ ET (b, c) ∧ (∀◦xy. x ≍ c ∧ y ≍ c ∧ a ⊑ x ∧ b ⊑ y → x ≍ y)
Definition 11 (internal diametricity). ID(a, b, c) iff IT (a, b) ∧ IT (b, c) ∧ (∀◦xy. x ≍ cy ≍ c ∧ ET (a, x) ∧ ET (b, y) → x ≍ y)
Definition 12 (concentricity). ab iff S(a)∧S(b)∧(a = b∨a b∧(∀◦xy. ED(x,y,a)∧IT(x,b)∧ IT(y,b)→ID(x,y,b))∨ba∧(∀◦xy. ED(x,y,b)∧IT(x,a)∧IT(y,a)→ID(x,y,a)))
Definition 13 (betweenness). [xyz] iff S(x)∧S(z)∧(xy∨yz∨(∃x′y′z′vw. x′ x∧y′ y∧ z′ z∧ED(x′,y′,v)∧ED(v,w,y′)∧ED(y′,z′,w)))
Definition 14 (centred on boundary). COB(s, r) iff S(s) ∧ (∀s′. s′s′ s → s′ ⌢ r ∧ ¬s′ ⊑ r)
Definition 15 (equidistant). EQD(x, y, z) iff ∃◦z′. z′ z ∧ COB(y, z′) ∧ COB(x, z′)
Definition 16 (midpoint). MID(x,y,z) iff [xyz]∧(∃◦y′. y′ y∧COB(x,y′)∧COB(z,y′))
Definition 17 (equidistant pair). EQDP(w,x,y,z) iff ∃◦uv. MID(w,u,y) ∧ MID(x,u,v) ∧ EQD(v, z, y)
Definition 18 (nearer centres). NEARER(w,x,y,z) iff ∃◦.x′ [wxx′]∧¬xx′∧EQDP(w,x′,y,z) Definition 19 (centred on interior). COI(s, r) iff ∃s′. s′ s ∧ s′ ⊑ r
We omit Axiom 3, which is outside the scope of this coursework. We can now present the remaining 6 axioms specific to RBG:
Axiom 4 (concentricity transitive). ∀◦xyz. x y ∧ y z → x z
Axiom 5 (equidistant replace concentric). ∀◦xx′yzw. EQDP (x, y, z, w)∧x′x → EQDP (x′, y, z, w) Axiom 6 (points centred bounded). ∀◦xy. ¬xy → (∃◦s. ∀◦z. COI(z,s) = NEARER(x,z,x,y)) Axiom7(constructspheres). ∀◦x.∃◦y.¬xy∧(∀◦z.COI(z,x)=NEARER(x,z,x,y)) Axiom 8 (interior part of). ∀xy. x ⊑ y = (∀◦s. COI(s, x) → COI(s, y))
Axiom 9 (all has spherical part). ∀r. ∃◦s. s ⊑ r
4
4 Prose proofs
We present here some prose proofs of theorems from the coursework. You will be directed to refer to these proofs for some tasks.
Theorem partof overlaps (a region’s parts also overlap it).
Given some region which is a part of x, we can prove it is also a part of y by transitivity of parthood and the fact that we assume x is a part of y. Thus by the definition of ‘overlaps’ we know that some part of x overlaps y.
Theorem both partof eq (mutual parthood implies equality).
If we have that summing all of the parts of x is y, then by the uniqueness of sums and
the fact that we know summing the parts of any x is x we can conclude that x = y.
We proceed by proving summing the parts of x is y by contradiction, i.e. by assuming it is not true. Then by unfolding the definition we have that there is some part of x which is not a part of y, or there is some part of y that no part of x overlaps. We take them one by one.
Suppose there is some part of x which is not a part of y. We can immediately conclude that it actually is a part of y by using the fact that x is a part of y and transitivity, hence we have a contradiction.
Now suppose there is some part w of y that no part of x overlaps. We use the fact that y is a part of x to conclude that y does not overlap w. But we already have that w is a part of y, hence we have our second contradiction.
Theorem sum all with parts overlapping (sum overlapping parts).
We want to show that, given some y, summing all regions whose parts all overlap y is the same as just summing y. As we do not yet know what y sums to, we will just call what it sums to x.
We proceed according to another proof by contradiction. Suppose summing y alone is notx. Thenyisnotapartofx,orthereisapartofxthatdoesnotoverlapy. We will take these one at a time, as before.
Suppose y is not a part of x. We can trivially conclude that y is in the set of regions whose every part overlaps y, then by our assumption that this set sums to x, y must be a part of x. Contradiction!
Now suppose there is a part of x that does not overlap y. Call it w. By our assumption, anything which is a part of x must have some z in the summed set which overlaps it, and this z has every one of its parts overlapping y (unfolding the assumption may make this clearer). Given w overlaps z, there must be some region wz that is a part of both of them. But anything which is a part of z overlaps y, hence wz overlaps y. This implies
5
there is a wzy which is a part of both wz and y. By transitivity we have that wzy is a part of w, hence w and y share a common part, i.e. w overlaps y, a contradiction!
References
[1] Brandon Bennett. A categorical axiomatisation of region-based geometry. Fundamenta Infor- maticae, 46(1-2):145–158, 2001.
[2] Brandon Bennett, Anthony G Cohn, Paolo Torrini, and Shyamanta M Hazarika. A foundation for region-based qualitative geometry. In ECAI, pages 204–208, 2000.
[3] Brandon Bennett, Anthony G Cohn, Paolo Torrini, and Shyamanta M Hazarika. Region-based qualitative geometry. University of Leeds, School of Computer Studies, Research Report Series, Report, 2000.
6