Location ontologies based on mereotopological pluralism

Abstract

Location ontologies axiomatize the relationship between physical bodies and the space that they occupy, and there is a rich literature on the philosophical underpinnings of these ontologies. Existing location ontologies have given primacy to the structure of what might be called abstract space. Consequently, the spatial properties and relations between physical bodies are extracted from the spatial properties and relations of the spatial regions that they occupy. In this paper, we take a different approach by beginning with the philosophical position of mereological pluralism, in which there are different mereologies for different kinds of entities. In particular, we make the fundamental ontological commitment that the mereology for spatial regions is different than the mereology for physical bodies. Different intuitions about location and different classes of physical bodies can be formally specified by imposing different conditions on this mapping, thus leading to different possible location ontologies. We propose an axiomatization of a location ontology and characterize the models of the axiomatization, up to isomorphism, by providing a representation theorem with respect to graph and poset homomorphisms.

Keywords

Mereotopology location parthood ontology verification

1. Introduction

The question, what is place? presents many difficulties. An examination of all the relevant facts seems to lead to divergent conclusions. Moreover, we have inherited nothing from previous thinkers, whether in the way of a statement of difficulties or of a solution. (Physics 208a27–208b7) (McKeon, 2009)

The relationship between physical bodies and the space that they occupy has long been a fundamental topic both in philosophy and more recently in applied ontology. This discussion has been closely related to debates in mereology, in which the relationship between the mereologies of both physical bodies and abstract space has been prominent. Approaches ranging from mereological monism to mereological pluralism have profoundly shaped any proposed ontology for location.

Existing location ontologies (and their applications in qualitative spatial reasoning and geospatial information systems) have given primacy to the structure of what might be called abstract space. Consequently, the spatial properties and relations between physical bodies are extracted from the spatial properties and relations of the spatial regions that they occupy. For example, the Region Connection Calculus is considered to be an axiomatization of space, not physical objects; indeed, discussion of the intended models of RCC (Cohn et al., 1997) have emphasized the role of Euclidean space. This leads to the oversimplification in which the spatial structure of physical bodies is naively mirrored in the structure of abstract space. This in turn raises a number of philosophical problems for mereology, such as the problem of extended simples (whether or not there exist physical objects that can be decomposed into spatially extended mereological atoms) and gunky space (abstract space that has no mereological atoms). Applying spatial mereotopologies for physical objects is also problematic from the practical point of view: Spatial regions are often considered to be atomless and extensional. However, there are valid physical configurations that do not satisfy atomlessness and extensionality axioms (Aameri and Gruninger, 2017). Consider for example the assembly of a bookshelf with two side panels and a back panel. Assemblies are typically modeled as finite domains; that is, it is assumed that the assembly product (in this case the bookshelf) has finite components and each component is atomic. Moreover, the two side panels are connected to the same set of elements (i.e., the back panel), but they are not identical. In fact, any model with finite number of elements may not be extensional. The atomlessness and extensionality axioms, therefore, should not be included in physical domain mereotopologies, but nor should their negations since a physical configuration may or may not be atomless and extensional.

Virtually all current location ontologies (Casati and Varzi, 1999; Donnelly et al., 2006; Borgo et al., 1997) assume that a unique fundamental parthood relation holds for all elements in all ontological categories. That is, there is just one parthood relation that holds both among regions and among entities that are located at regions. Such an assumption allows a whole that is composed of entities from distinct ontological categories, such as an entity that is the sum of a physical body and a spatial region.

One way to resolve these problems is to provide an explicit treatment of the underlying principles that can guide our understanding of the relationship between physical bodies and abstract spatial regions. The identification of these principles for a location ontology is inspired by the following quote from Casati and Varzi (1999):

One way or the other, spatial reasoning must come to terms with the fundamental metaphysical mystery on which it depends – embedding in space.

We accordingly propose a new approach to the axiomatization of location ontologies. First, we adopt the philosophical stance of mereological pluralism, that one needs different mereologies for different kinds of entities. In particular, we make the fundamental ontological commitment that the mereology for spatial regions is different than the mereology for physical bodies. This allows us to use a mereotopology (such as $MT$ ) for physical bodies that is weaker than the mereotopology (such as RCC) on abstract regions, or to allow different axioms for the behaviour of summation. We can study the mereotopological relations on physical bodies independently of the mereotopology of spatial regions.

Second, location axiomatizes a mapping from the mereotopology of physical bodies to the mereotopology of regions in abstract space. Different intuitions about location and different classes of physical bodies can be formally specified by imposing different conditions on this mapping, thus leading to different possible location ontologies. We do not commit to any specific assumption about space, objects, or the relationships between them except that there should be a distinction between spatial regions and objects that occupy them. This allows us to reuse existing mereotopologies when designing new location ontologies.

We propose an axiomatization of a location ontology and characterize the models of the axiomatization, up to isomorphism, by providing a representation theorem with respect to graph and poset homomorphisms. Our proposed theory is the weakest axiomatization required for representing location and occupation and so uses a region mereotopology with the same strength as the physical object mereotopology. However, due to the way we conceptualize and axiomatize location, both of the object and region mereotopologies can be extended to stronger mereotopologies with no effects on other modules of the proposed location ontology. The only restriction that the ontology imposes is that the region mereotopology must be at least as strong as the physical object mereotopology.

We begin in Section 2 by presenting a set of motivating scenarios and competency questions for our proposed ontology. We then review, in Section 3, the fundamental ontological commitments and ontological choices for location, thereby specifying a set of semantic requirements for location ontologies. In Section 4, we formalize these requirements as a class of mathematical structures (which we name occupation structures), present an axiomatization (named $T_{occupy_root}$ ), and then show that the models of $T_{occupy_root}$ are equivalent to occupation structures. We finish the paper by demonstrating the relationship between the extensions of $T_{occupy_root}$ and existing location ontologies.

2. Motivating scenarios

To guide the identification for the ontological choices and commitments for location ontologies, we propose a set of motivating scenarios that encapsulate potential applications of these ontologies.

It should be noted that we are interested only in the problem of location for physical bodies; in this paper we do not consider the problem of spatial location for events.

Scenario 1: Bookshelf. Alice buys a bookshelf from a furniture store. After unpacking the components from the box, she lays them out on the floor. Following the instructions, Alice assembles the bookshelf by attaching the sides to the backboard, and then connecting each shelf to the subassembly.

Scenario 2: Motion. Bob moves his computer across the table in his office. The parts of the computer and the table remain the same, and the space inside the office is fixed.

Scenario 3: Spatial change. A forest fire begins on the side of a mountain, grows to cover the entire valley adjacent to the mountain, and is then extinguished by firefighters.

Scenario 4: Landforms. An island cannot be disconnected (otherwise it would be two islands); similarly, the sum of two islands is not itself an island. Geological terranes never overlap, although they can be disconnected, and the sum of two terranes is not a terrane.

Scenario 5: Delivery and logistics systems. Carol, who lives in Toronto, orders a book from Acme Publishing. A copy of the book is found in a warehouse near Montreal. A shipping company picks up the book from the warehouse, loads it into the truck, and delivers it to Carol’s address.

Scenario 6: Commonsense reasoning. David drops some ice cubes into a glass and then pours water from a pitcher into the glass until it is full. Where are the ice cubes?

Scenario 7: Behaviour of physical objects. Emily is packing her car after shopping. She stuffs the pillow into the space between the chair and the lampstand, and then places the lampshade on top so that it doesn’t break.

Scenario 8: Behaviour of physical objects. A wooden board cannot be bent so that its ends touch each other, but we can bend a piece of thin metal sheet.

To evaluate the proposed ontology, we use the following competency questions which are based on Scenarios 1 to 8.

Mereological Pluralism – do there exist distinct mereotopological relations for different classes of objects? If so, are they axiomatized by different mereotopological theories?

Motion and Spatial Change – When a physical object moves, what spatial relations change? What relationships do not change? How can one say whether an object is moving or expanding/contracting?

Locations and Addresses – What is the relationship between a physical object (e.g., an ice cube) and objects that surround it (e.g., a portion of water in the cup)? What is the relationship between a physical object (e.g., a book) and the address that it’s located on (e.g., a warehouse)? How can we say two objects have the same address? When can we say that the object moved to another address?

Rigidity of Objects – In terms of spatial properties, what is the difference between a rigid object and a non-rigid object?

Scenarios 1 and 4 motivate [CQ1]: In Scenario 1, within the box the components are not connected, although the spatial regions occupied by the components are in contact with each other. While the components are laid on the floor, they are all disconnected. During construction, self-connected subassemblies correspond to different sums of components. In each of these cases, the mereotopological relationships of the components are different than those of the spatial regions they occupy. If we consider the landforms in Scenario 4, we can see that islands, continents, terranes, and other classes of geographical entities satisfy different mereological axioms, and hence have different parthood relations. Furthermore, there are different mereologies for different classes of physical bodies, even though all share the same mereology on spatial regions.

Scenarios 2 and 3 motivate [CQ2]: In Scenario 2, there is no change in any parthood relation (either in the physical bodies or spatial regions), whereas in Scenario 3, the parts of the physical body that is the fire are also changing as the fire grows and is extinguished, yet there is no change in either the parts of the spatial regions nor their mereotopological relationships. In both scenarios the locations of physical bodies are changing.

In Scenario 5, there is a relationship between physical bodies that is derivative of the locations of the bodies. Scenario 6 is similar insofar as it is concerned with the relationship between physical bodies and their locations. Both the icecubes and the water occupy regions that are part of the spatial region enclosed by the cup’s location. Scenarios 5 and 6 motivate [CQ3].

Finally, scenarios 7 and 8 motivate [CQ4] as with these scenarios we find the distinction between rigid and flexible physical bodies.

3. Ontological choices for location ontologies

What then after all is place? The answer to this question may be elucidated as follows.

Let us take for granted about it the various characteristics which are supposed correctly to belong to it essentially. We assume then –

(1) Place is what contains that of which it is the place.

(2) Place is no part of the thing.

(3) The immediate place of a thing is neither less nor greater than the thing.

(4) Place can be left behind by the thing and is separable.

In addition:

(5) All place admits of the distinction of up and down, and each of the bodies is naturally carried to its appropriate place and rests there, and this makes the place either up or down.

(Physics 210b32–211a5)

Aristotle notwithstanding, a number of philosophical positions underpin much of the foundations for location ontologies.

3.1. Substantivalism: Bodies and regions

The first choice that one must make is the distinction between physical bodies and abstract space. With supersubstantivalism (Lehmkuhl, 2018; Schaffer, 2009; Sklar, 1974), there is no such distinction – located entities are identical with their locations, so that each object is identical to the region of space it occupies. From the applied ontology perspective, this is typically formalized by saying that physical bodies form a subclass of regions (since every physical body is a region). Proponents of supersubstantivalism argue that its parsimony simplifies the ontology by positing fewer distinct class of objects (in fact going so far as to say that there is a unique fundamental substance in the world – space).

Substantivalism (Parsons, 2007) is less extreme, insofar as it posits the existence of such entities as physical bodies that are distinct from spatial regions, and that both are concrete fundamental entities in the world with the same ontological status. The motivation is that the basic properties, relationships, and identity criteria are so different between physical bodies and spatial regions that the two classes must be disjoint. Arguably, this approach is closer to the commonsense notions of bodies and space than supersubstantivalism. Even the linguistic use of the word “location” has a bias towards this distinction – we say that a physical body is located in or at some spatial region, rather than saying that a region is a physical body.

3.2. Compositional monism and pluralism

If one adopts substantivalism, the natural question to ask is about the relationship between spatial regions and physical bodies. Compositional (or mereological) monism advocates that there is a unique fundamental parthood relation that holds for all elements in all ontological categories. In particular, there is just one parthood relation that holds both among regions and among entities that are located at regions (Gilmore, 2017; Sider, 2007; Saucedo, 2011; Lehmkuhl, 2018; Leonard, 2016; Lewis, 1991). This position is adopted by virtually all current location ontologies (Casati and Varzi, 1999; Donnelly et al., 2006; Borgo et al., 1997).

With mereological monism, regions of space also have a location (typically, they are located at themselves). In fact, many approaches define spatial regions to be those entities that are located at themselves. Strictly speaking, this also means that there are at least two entities that can be located in a spatial region – the physical body and the region itself (although non-colocation axioms can be specified by suitably constraining the restricted entities to be nonregions).

Variants of compositional monism allow for additional parthood relations that are specializations of the one parthood relation only if they are definable with respect to an a priori taxonomy. For example, one can define the parthood subrelation in which its arguments are restricted to both be physical bodies or both be abstract spatial regions (Borgo et al., 1997). Nevertheless, this still allows a whole that is composed of entities from distinct ontological categories, such as an entity that is the sum of a physical body and a spatial region. Compositional monism allows the existence of an object that consists of a physical body (e.g. chair) and the region of space that it occupies. Both Parsons (2007) and Leonard (2016) raise the example of the possible location for the object that is the sum of someone’s left hand and the number π.

In contrast, compositional pluralism (McDaniel, 2004, 2007; Markosian, 2014) commits to one fundamental parthood relation that holds between regions, and another distinct parthood relation that holds between material objects. The primary argument in favour of this approach is that it avoids the problems of anomalous sums. Following compositional pluralism, physical bodies are entirely separate from their locations – there is no possible way for them to share any parts, since there are distinct mereological relations.

This approach can also be extended to a notion of mereotopological pluralism, in which there are distinct mereotopologies for physical objects and spatial regions (that is, in addition to distinct parthood relations, there are distinct connection relations for regions and physical bodies).

3.3. Mereological harmony

Since substantivalism posits the distinction between physical bodies and spatial regions, and compositional pluralism further requires the mereotopologies on these entities be distinct, we are naturally faced with the problem of the relationship between location and mereotopology. The notion of mereological harmony was introduced by Schaffer (2009) to describe the relationship between the mereological structure of a located entity and the mereological structure of its location. In particular, this notion is a response to the question: if an object occupies a region of space, must it have the same mereological structure as that region of space?

We argue that any resolution of this question requires compositional pluralism. Attempting to formalize mereological harmony principles within mereological monism leads to confusion.

A variety of different principles for mereological harmony have been proposed within the philosophical literature (Leonard, 2016; Uzquiano, 2011; Parsons, 2007; Gilmore, 2017; Saucedo, 2011). In this paper, we adopt the following:

Principle 1 (Basic Harmony Principle).

The parts of a physical body occupy parts of the region occupied by the physical body itself.

Note that this principle only postulates the existence of a mapping from the mereotopology of physical bodies to the mereotopology of spatial regions. In this sense, the Basic Harmony Principle is the weakest formalization of mereological harmony insofar as it does not posit any additional constraints on the mapping. A subsequent paper will characterize other mereological harmony principles and their relationships to each other.

3.4. Ontological commitments for the occupy ontology

A location ontology can be designed by adopting different stances towards the ontological choices introduced in the preceding section. The location ontology that we propose in this paper adopts the following ontological commitments:

Spatial regions and physical bodies are distinct entities, and each have their own distinct mereotopology.

Occupation is a relation between a physical body and an spatial region – there is no mereotopological relationship between spatial regions and physical bodies.

Each physical body occupies exactly one spatial region – multilocation is not possible.

The mereotopological relations between physical bodies must be preserved in the mereotopological relations between the spatial regions that they occupy.

We therefore adopt the stance of substantivalism and mereological pluralism, together with the Basic Harmony Principle. On the one hand, a supersubstantivalist might say that we have a crowded ontology indeed, with two fundamental disjoint classes of entities and two distinct mereotopologies. On the other hand, we have selected these commitments because they are the minimal conditions on mereological harmony principles. For example, the requirements we state allow the possibility of multiple objects occupying one single region, but they do not allow a connected physical body to be located in disconnected regions. The justification of these commitments is a natural question that arises at this point – in what sense are these the right ontological commitments for a location ontology? Are there in fact multiple alternative sets of ontological commitments that are equally valid?

We can show that the set of above ontological commitments are sufficient to address the competency questions and represent the motivating scenarios.

Adaptation of substantivalism and mereological pluralism addresses [CQ1] as well as the representation of Scenarios 1 and 4. In Scenarios 4, for example, Geographical entities form a subclass of physical bodies distinct from spatial regions (following substantivalism) and mereological pluralism supports the multiple mereologies that are used to capture the parthood relation for each class of entities.

Having occupation as a relation between physical bodies and spatial regions enables addressing [CQ2] and [CQ3]: Motion and spatial changes can be represented in terms of change in an occupy relation. When an object expands, the region that it occupies before the expansion is a proper part of the region it occupies after the expansion, while when an object merely moves the regions that it occupies (before and after the movement) only overlap. To say that a physical body is located in an address/location (e.g., the book is located in the warehouse or that it is located in the truck after loading) means that the region occupied by the physical body is part of the region occupied by the address/location. In Scenario 6, for example, both the icecubes and the water occupy regions that are part of the spatial region enclosed by the cup’s location (following the Basic Harmony Principle). However, the regions occupied by the icecubes are disjoint from the regions occupied by the water; rather than having interpenetrating objects, the icecubes occupy holes in the region occupied by the water. This indicates that in some cases, stronger mereological harmony principles may be needed. (As the icecubes melt down the region that they occupy shrinks and the region that water occupies expands. So to fully represent this process a temporal representation is also required) Note that different types of spatial change (i.e., [CQ2]), as well as addresses/locations (i.e., [CQ3]) can be represented since spatial regions and physical bodies are distinct entities with distinct mereotopologies, and occupation maps each physical body to a unique spatial region representing its location.

The distinction between rigidity and flexibility (i.e., [CQ4]) lies not in the mereotopology of physical bodies but in the way they are embedded in space. For example, parts of a flexible physical body that are not connected may occupy spatial regions that are connected by bending the object, which requires distinctive mereotopologies for physical objects and spatial regions as well as an occupation relation.

4. The occupy ontology

In designing an ontology, our objective is twofold – first, to prove that the models of the ontology are actually the intended models, and second, to demonstrate that the intended models do indeed formalize the ontological commitments. Our strategy is to first specify a class of mathematical structures and show that the ontology axiomatizes this class of structures (that is, there is a one-to-one correspondence between the class of models of the ontology and the class of mathematical structures). We then specify a representation theorem for this class of mathematical structures to demonstrate that it formalizes the ontological commitments. The primary benefit of this strategy is that it makes explicit the modular organization of the subtheories of the ontology, thereby highlighting how other ontologies are reused.

4.1. Methodology

The design and evaluation of the Occupy Ontology follows the verification approach described by Gruninger et al. (2010) and Aameri and Gruninger (2015). Rather than beginning with an axiomatization and then determining whether the models of the axioms are correct, we start by stating the requirements and ontological commitments that must be satisfied by the ontology. The requirements are then specified in the form of a class of mathematical structures; such structures are referred to as the required structures for the ontology. The ontology is verified with respect to the relationship between the required structures for the ontology and the axiomatization of the ontology.

If the ontology is too weak, it has models which are not isomorphic to any required structures. That is, there are requirements that are not captured by the ontology. If the ontology is too strong, there exist required models which are omitted, since the ontology imposes conditions which are not necessary by the requirements. An ontology $T_{ont}$ axiomatizes a class of required structures $M^{req}$ if there is a one-to-one correspondence between $Mod (T_{ont})$ and $M^{req}$ .

Nevertheless, it can be quite difficult to characterize the models of an ontology up to isomorphism and demonstrate that there is such a bijection between $Mod (T_{ont})$ and $M^{req}$ . The approach proposed by Gruninger et al. (2010) is to find a mathematical theory T for which it has already been proven that there is bijection between $Mod (T)$ and $M^{req}$ . The ontology itself is then designed as an axiomatization that is synonymous with the mathematical theory. When two theories are synonymous, there is a one-to-one correspondence between their models such that the corresponding models can be turned into each other using the translation definitions between the theories. Consequently, by axiomatizing $T_{ont}$ in such a way that it is synonymous with T, we in fact show that there is a one-to-one correspondence between models of $T_{ont}$ and $M^{req}$ . This leads to a methodology by which we design ontologies through reuse of existing mathematical theories that axiomatize the class of required models.

4.2. Introducing $M^{occupy_root}$

The first step is to specify the class of structures which capture intuitions and ontological commitments we described in Section 3:

compositional pluralism: there is a mereotopology on physical bodies and another distinct mereotopology on spatial regions;

mereological harmony: there is a homomorphism from the mereotopology of physical objects to the mereotopology of regions which is both

a homomorphism from the mereology of physical objects to the mereology of spatial regions, and

a homomorphism from the connection structure of physical objects to the connection structure of spatial regions.

Note that the existence of a mapping from one mereotopology to the other means that each physical body has a unique location. Multilocation for physical bodies would mean that a mapping could not exist.

We will denote the class of required structures by $M^{occupy_root}$ . We will first need to define several classes of mathematical structures1

¹
Definitions for the notation used in the specification of the mathematical structures can be found in Appendix A.

that will be amalgamated together to construct the required structures.

4.2.1. Mereographs

The ontological commitment to mereotopological pluralism means that we need to specify the mereotopology of physical bodies as well as the mereotopology of regions. We follow the work of Grüninger and Aameri (2017) for the approach to mereotopology in which both parthood and connection are primitive relations.

The mereology of the parthood relation is represented by the class of partial orderings $M^{partial_ordering}$ :

Definition 1.
A partial ordering is a pair of sets $P = ⟨ V, ⩽ ⟩$ such that
$⩽ \subseteq V \times V$ ;

$⩽ \circ ⩽ \subseteq ⩽$ ;

$Id \subseteq ⩽$ ;

$⩽ \cap ⩽^{-} \subseteq Id$ .
$M^{partial_ordering}$ denotes the class of partial orderings.

Since the connection relation is symmetric and reflexive, it is represented by the class of graphs with loops $M^{graph_loops}$ :
Definition 2.
A graph with loops is a pair of sets $G = ⟨ V, E ⟩$ such that
$E \subseteq V \times V$ ;

$E = E^{-}$ ;

$I \subseteq E$ .
$M^{graph_loops}$ denotes the class of graphs with loops.

Mereotopologies are represented by the amalgamation of partial orderings and graphs with loops:
Definition 3.
$P \oplus G = ⟨ V, E, ⩽ ⟩$ is a mereograph iff
$P = ⟨ V, ⩽ ⟩$ such that $P \in M^{partial_ordering}$ ;

$G = ⟨ V, E ⟩$ such that $G \in M^{graph_loops}$ ;

$U^{P} (N^{G} (x)) \subseteq N^{G} (x)$ , for each $x \in V$ .
$M^{mereograph}$ denotes the class of mereographs.

Figure 1 depicts an example of a mereograph.

Fig. 1.
Example of a mereograph.

The following Theorem from Grüninger and Aameri (2017) showed that there is a one-to-one correspondence between $M^{mereograph}$ and models of $T_{mereograph}$ ,2
²
colore.oor.net/mereograph/mereograph.clif

which in turn is synonymous with the Ground Mereotopology (MT) of Casati and Varzi (1999):
Theorem 1.
There exists a bijection $φ : Mod (T_{mereograph}) \to M^{mereograph}$ such that $φ (⟨ V, part, C ⟩) = P \oplus G$ iff
$⟨ x, y ⟩ \in C$ iff $(x, y) \in E$ ;

$⟨ x, y ⟩ \in part$ iff $x ⩽ y$ .

The use of MT rather than a mereotopology such as the Region Connection Calculus (RCC; Randell et al. 1992) is rooted in the ontological commitment to mereotopological pluralism. Formalizing the structure of a physical body (such as the bookshelf in Scenario 1), as well as the physical relationships among the different components and subassemblies of the body, requires a mereotopology for physical bodies. The mereological subtheory expresses parthood relations (e.g. the shelves, brackets, sideboards are atomic parts of the bookshelf), while the topological subtheory expresses connection relations between the parts (e.g. each shelf is connected to the two sideboards). The RCC8 relations (Cohn et al., 1997) have widely been used for describing spatial relationships within physical settings. The results of Grüninger and Aameri (2017) show that the mereotopology MT corresponds to an extension of the first-order theory of the RCC8 composition table. This means that the underlying mereotopology for RCC8 used in such settings does not include any of the basic mereotopological principles (i.e., supplementation, atomicity, extensibility, and closure under sum and product), since these principles are not axioms in MT.

On the other hand, RCC is widely used for the representation of space. RCC is a first-order theory3
³
colore.net/mereotopology/rcc.clif

whose signature contains the single primitive binary relation $C (x, y)$ denoting “x is connected to y”. Parthood is defined in terms of connection alone, being equivalent to the topological notion of enclosure. One distinctive property of models of RCC is that the regions are atomless – every region has proper part. On the other hand, physical bodies are not necessarily atomless. For assembling a bookshelf, we do not care about proper parts of shelves and divider. In many applications we have a finite domain, meaning that the elements of the domain are not atomless.

Intuitively then, elements of the two classes satisfy the axioms of two different mereotopologies – $MT$ for the physical bodies and $RCC$ for abstract space. Furthermore, the mereotopology on physical bodies is “weaker” than the mereotopology on spatial regions, in the sense that $MT$ is a subtheory of $RCC$ . Besides the axioms of different mereological theories, one important difference between physical bodies and spatial regions is the relationship between parthood and connection. Within $RCC$ , enclosure entails parthood, which is not the case for $MT$ .

If we look closely at Scenarios 2 and 3, we can see that any treatment of motion and spatial change also leads to the ontological commitment to multiple mereotopologies. A model-theoretic characterization of RCC (Stell, 2000) demonstrates that every model of RCC is equivalent to an atomless Boolean lattice together with a graph, where the Boolean lattice represents parthood relations and the graph represents connection relations. On the other hand, any pair of nontrivial atomless Boolean algebras are elementary equivalent, and so the differences between the pairs are not first-order axiomatizable. Therefore, it is not possible to describe spatial change (by a first-order language) with the RCC theory alone. This is compatible with the view that RCC is intended to be a representation of spatial regions, and abstract space is fixed – it is the spatial extensions of physical objects that change. Therefore, to represent mereotopological change, there should be an explicit distinction between spatial regions and objects that occupy them. In that sense, rather than changing spatial regions, activity occurrences change the regions that are occupied by a set of objects.
4.2.2. Poset homomorphisms

The next requirement for the required structures in $M^{occupy_root}$ is mereological harmony, which is formalized as a mapping of the mereology of physical objects to the mereology of regions. Such a mapping is the formalization of the Basic Harmony Principle – the parts of a physical body occupy parts of the region occupied by the physical body itself. Homomorphisms formalize the Basic Harmony Principle insofar as occupation is thought of as a mapping such that any parthood relationship between two physical bodies will be preserved by the mapping, that is, the corresponding spatial regions will also be related by the spatial parthood relation.

It is important to note that although mereological monism can represent occupation as a mapping, it cannot represent occupation as a homomorphism on the mereology. First, since there is only one mereology $Q$ , any mapping $μ : Q \to Q$ that preserved parthood would be a poset endomorphism that fixes the spatial regions (i.e. regions would occupy themselves). Furthermore, there exist several oddities with such poset endomorphisms, including the existence of an entity that contains a region as part yet is mapped to a different region, and the fact that many different entities must be mapped to the same region (namely those entities that contain both regions and non-regions as parts).

The advantage of representing occupation as a poset homomorphism (related to mapping the mereology of physical bodies to the mereology of spatial regions) is that the class of homomorphisms between posets is well-understood (Schröder, 2003). On the other hand, a characterization of poset endomorphisms that fix a subordering does not exist in the literature. In particular, given two posets $P$ and $Q$ , the set of homomorphisms $μ : Q \to P$ itself forms as poset, since two mappings $μ_{1}$ , $μ_{2}$ can be ordered by the condition $\begin{matrix} μ_{1} (q) ⩽ μ_{2} (q) \end{matrix}$ for all $q \in Q$ .

Some approaches (e.g. Borgo et al., 1997) attempt to specify occupation as a mapping from one definable subordering (i.e. the mereology restricted to physical bodies) to another definable subordering (i.e. the mereology restricted to spatial regions), and then argue that this mapping is a homomorphism. However, since the mapping is total, restricting it to definable substructures does not correspond to a homomorphism between the substructures. Admittedly, one could consider the notion of partial homomorphisms (i.e. partial mappings with domain and image that are subsets of the domain); however, there is no known characterization of the set of partial homomorphisms of a poset.

The first challenge in the design of the ontology is to find a class of mathematical structures that can be used to represent a mapping between the mereotopology of physical bodies and the mereotopology of spatial regions.

Definition 4.
A mapping-bipartite incidence structure is a tuple $I = ⟨ P, L, I ⟩$ such that
$P \cap L = \emptyset$ ;

$I \subseteq (P \times L) \cup (L \times P) \cup Id$ ;

$I^{-} = I$ ;

$N^{I} (P) \cap L \neq \emptyset$ ;

for each pair of distinct elements $l_{1}, l_{2} \in L$ , $\begin{matrix} N^{I} (l_{1}) \cap N^{I} (l_{2}) = \emptyset \end{matrix}$
$M^{mapping_bipartite}$ is the class of mapping-bipartite incidence structures.

The idea behind mapping-bipartite incidence structures is that physical bodies and spatial regions are represented by the two disjoint sets P and L respectively,4
⁴
Within incidence structures, the elements of P are referred to as points and the elements of L are referred to as lines.

and a physical body is incident to a region in the incidence structure iff the body occupies the region. However, to guarantee that incidence represents a mapping, we must enforce the condition that each element of P is incident with a unique element of L. Condition (4) in Definition 4 enforces the existence of such an element, and Condition (5) enforces uniqueness. Figure 2 shows an example of a mapping-bipartite incidence structure; representing a mapping in which the points $p_{1}$ and $p_{2}$ are mapped to the line $l_{1}$ (since $p_{1}, p_{2}$ are both incident with $l_{1}$ ), and the point $p_{3}$ is mapped to the line $l_{2}$ .

Fig. 2.
Example of a mapping-bipartite incidence structure.

It is insufficient to only require that there be a mapping from physical bodies to spatial regions – we need to impose an additional condition on the relationship between their mereologies. Recall that in the context of location ontologies, the Basic Harmony Principle (the parts of a physical body occupy parts of the region occupied by the physical body itself) is captured by the notion of homomorphisms between partially ordered sets, which are mappings that preserve the structure of the partial orderings.
Definition 5.
Suppose $Q, P \in M^{partial_ordering}$ such that $Q = ⟨ V_{1}, ⩽ ⟩$ , $P = ⟨ V_{2}, ⪯ ⟩$ .

A mapping $μ : Q \to P$ is a poset homomorphism iff $\begin{matrix} x ⩽ y \Rightarrow μ (x) ⪯ μ (y) \end{matrix}$

To formally capture the Basic Harmony Principle, we therefore consider a class of structures that represents homomorphisms between partial orderings.
Definition 6.
$Q \oplus I \oplus P$ is a preserved multigeometry iff
$Q = ⟨ P, ⪯ ⟩$ such that $Q \in M^{partial_ordering}$ ;

$P = ⟨ L, ⩽ ⟩$ such that $P \in M^{partial_ordering}$ ;

$I = ⟨ P, L, I ⟩$ such that $I \in M^{mapping_bipartite}$ .

$N^{I} (U^{Q} (x)) \subseteq U^{P} (N^{I} (x))$
$M^{mapping_preserve}$ is the class of preserved multigeometries.

How are the conditions in the definition of preserved multigeometry related to the definition of poset homomorphism? By Conditions (1) and (2), there exist two partial orderings $Q$ and $P$ . Condition (3) guarantees that the incidence relation represents a mapping $μ : Q \to P$ . Condition (4) guarantees that this mapping is a homomorphism.

An example of a preserved multigeometry can be seen in Fig. 3. The elements $a, b, d, e$ of $Q$ are mapped to the poset $P$ containing the elements $l_{i}$ . We can see, for instance, that $a ⩽ d$ and that $μ (a) ⪯ μ (d)$ (i.e. $l_{3} ⪯ l_{7}$ ).

Fig. 3.
Example of a preserved multigeometry. The dashed lines represent the incidence relation in the preserved multigeometry and a mapping $μ : Q \to P$ .

The representation theorem shows that preserved multigeometries do indeed represent poset homomorphisms:
Theorem 2.
Let $Hom (Q, P)$ denote the set of all poset homomorphisms between the partial orderings $Q$ , $P$ .

If $\begin{matrix} P = {μ : μ \in Hom (Q, P) ∋ Q, P \in M^{partial_ordering}} \end{matrix}$ then there is a bijection $φ : P \to M^{mapping_preserve}$ such that $\begin{matrix} φ (μ) = Q \oplus I \oplus P \end{matrix}$ iff $μ : Q \to P$ and $\begin{matrix} μ (x) = N^{I} (x) \cap L \end{matrix}$

In other words, each preserved multigeometry $Q \oplus I \oplus P$ corresponds to a homomorphism that maps the partial ordering $Q$ to the partial ordering $P$ ; the incidence structure $I$ represents this homomorphism in the sense that the line l that is incident with the point p is the image of p under the homomorphism.

Note that since each element of $P$ is a specific homomorphism between two specific partial orderings, $P$ itself is the set of all poset homomorphisms between all pairs of partial orderings in $M^{partial_ordering}$ . It is not enough to consider all possible poset homomorphisms between two partial orderings; the class of preserved multigeometries represents the poset homomorphisms between any two partial orderings.

The mathematical theory $T_{mapping_preserve}$ 5
⁵
colore.oor.net/multigeometry/mapping_preserve

axiomatizes the class of preserved multigeometries:
Theorem 3.
There exists a bijection $\begin{matrix} φ : Mod (T_{mapping_preserve}) \to M^{mapping_preserve} \end{matrix}$ such that $φ (⟨ M, point, line, in, part, leq ⟩) = Q \oplus I \oplus P$ iff
$M = P \cup L$ ;

$⟨ p ⟩ \in point$ iff $p \in P$ ;

$⟨ l ⟩ \in line$ iff $l \in L$ ;

$⟨ x, y ⟩ \in in$ iff $y \in N^{I} (x)$ ;

$⟨ x, y ⟩ \in part$ iff $y \in U^{Q} (x)$ ;

$⟨ x, y ⟩ \in leq$ iff $y \in U^{P} (x)$ .

One may ask why we first present a definition of preserved multigeometries and then prove a separate theorem that shows how these structures correspond to poset homomorphisms. Why not define preserved multigeometries directly by their relationship to poset homomorphisms? A mathematical structure is specified using only the extensions of the relations in the signature and elements of the domain; there is no external reference to any mathematical properties beyond the relations in the signature. The relationship between the extension of a relation and some other property (e.g. the existence of homomorphisms) is proven in a representation theorem. For example, Boolean lattices are defined with respect to the existence of meets, joins, and complements; the relationship to the field of sets is proven in the Stone Representation Theorem. Similarly, distributive lattices are defined with respect to constraints on meet and join, while Birkhoff’s Representation Theorem shows that the elements of any finite distributive lattice can be represented as finite sets, in such a way that the lattice operations correspond to unions and intersections of sets.
4.2.3. Graph homomorphisms

For mereotopological harmony, we also need to formalize the mapping of the connection structure of physical objects to the connection structure of regions (in addition to the mereologies). Just as we invoked the notion of poset homomorphisms to formalize the preservation of mereologies under the mapping, the notion of graph homomorphism formalizes the preservation of connection structures.

Definition 7.
Suppose $C, G \in M^{graph_loops}$ such that $C = ⟨ V_{1}, E_{1} ⟩$ , $G = ⟨ V_{2}, E_{2} ⟩$ .

A mapping $μ : C \to G$ is a graph homomorphism iff $\begin{matrix} ⟨ x, y ⟩ \in E_{1} \Rightarrow ⟨ μ (x), μ (y) ⟩ \in E_{2} \end{matrix}$

In a similar way that we used multigeometries to represent poset homomorphisms, we consider a class of structures that represent graph homomorphisms as a way of formalizing the application of the Basic Harmony Principle to mereotopology.
Definition 8.
$G \oplus I$ is a looped graph homomorphism structure iff
$G = ⟨ P \cup L, E ⟩$ such that $G \in M^{graph_loops}$ ;

$I = ⟨ P, L, I ⟩$ such that $I \in M^{mapping_bipartite}$ ;

$N^{G} [P] \subseteq P$ ;

$N^{G} [L] \subseteq L$ ;

$N^{I} (x) \cap N^{G} (x) = \emptyset$ .

$N^{I} (N^{G} [x]) \subseteq N^{G} [N^{I} (x)]$ , for any $x \in P$ .
$M^{loop_graph_hom}$ is the class of looped graph homomorphism structures.

How are the conditions in the definition of looped graph homomorphism structure related to the definition of graph homomorphism? By Conditions (1), (3) and (4), there are two disjoint subgraphs of a graph $G$ – a subgraph $G_{P}$ whose vertices are points in $I$ and a subgraph $G_{L}$ whose vertices are lines in $I$ . Condition (2) guarantees that the incidence relation represents a mapping $μ : G_{P} \to G_{L}$ . Condition (5) guarantees that this mapping is a graph homomorphism. By Condition (6), the graph $G$ and the incidence structure $I$ are disjoint.

An example of a looped graph homomorphism structure can be seen in Fig. 4. The points $a, b, d, e$ in one subgraph are mapped to the lines $l_{i}$ in the other subgraph. We can see, for instance, that a is adjacent d and that $μ (a) = l_{3}$ is adjacent to $μ (d) = l_{7}$ .

Fig. 4.
Example of a looped graph homomorphism structure. The dashed lines represent the incidence relation in the looped graph homomorphism structure.

Looped graph homomorphism structures represent graph homomorphisms through the following representation theorem:
Theorem 4.
Let ${Hom}^{loop} (C, G)$ denote the set of all graph homomorphisms between the graphs with loops $C$ , $G$ .

If $\begin{matrix} G = {μ : μ \in {Hom}^{loop} (C, G), ∋ C, G \in M^{graph_loops}} \end{matrix}$ then there is a bijection $φ : G \to M^{loop_graph_hom}$ such that $\begin{matrix} φ (μ) = (C \cup G) \oplus I \end{matrix}$ iff $μ : C \to G$ and $\begin{matrix} μ (x) = N^{I} (x) \cap L \end{matrix}$

As we saw with preserved multigeometries, each looped graph homomorphism structure $C \oplus I \oplus G$ corresponds to a homomorphism that maps the graph $C$ to the graph $G$ ; the incidence structure $I$ represents this homomorphism in the sense that the line l that is incident with the point p is the image of p under the homomorphism.

Thus, each structure $M^{loop_graph_hom}$ corresponds to a unique graph homomorphism between graphs with loops, and each graph homomorphism corresponds to a unique structure in $M^{loop_graph_hom}$ .

The mathematical theory $T_{graph_hom}$ 6
⁶
colore.oor.net/multigeometry/graph_hom

axiomatizes the class of graph homomorphism between graphs with loops:
Theorem 5.
There exists a bijection $\begin{matrix} φ : Mod (T_{graph_hom}) \to M^{graph_hom} \end{matrix}$ such that for any $φ (⟨ M, point, line, in, adj ⟩) = G \oplus I$
$M = P \cup L$ ;

$⟨ p ⟩ \in point$ iff $p \in P$ ;

$⟨ l ⟩ \in line$ iff $l \in L$ ;

$⟨ x, y ⟩ \in in$ iff $y \in N^{I} (x)$ ;

$⟨ x, y ⟩ \in adj$ iff $(x, y) \in E$ .

4.2.4. $M^{occupy_root}$

Individually, preserved multigeometries formalize poset homomorphisms and looped graph homomorphism structures represent graph homomorphisms, yet we are primarily interested in formalizing mereograph homomorphisms, since mereographs are the amalgamation of posets and looped graphs.

Definition 9.
$Q \oplus C \oplus I \oplus P \oplus G$ is an occupation structure iff
$Q \oplus C, P \oplus G \in M^{mereograph}$ ;

$Q \oplus I \oplus P \in M^{mapping_preserve}$ ;

$(C \cup G) \oplus I \in M^{loop_graph_hom}$ .
$M^{occupy_root}$ is the class of occupation structures.

The idea is that occupation structures are a representation of mereograph homomorphisms, which are captured by the amalgamation of preserved multigeometries and looped graph homomorphism structures.
Theorem 6.
Suppose $\begin{matrix} O = {μ : μ \in Hom (Q \oplus C, P \oplus G) ∋ Q \oplus C, P \oplus G \in M^{mereograph}} \end{matrix}$

There is a bijection $φ : O \to M^{occupy_root}$ such that $\begin{matrix} φ (μ) = Q \oplus C \oplus I \oplus P \oplus G \end{matrix}$ iff $μ : Q \oplus C \to P \oplus G$ and $\begin{matrix} μ (x) = N^{I} (x) \cap L \end{matrix}$

Thus, the class of structures $M^{occupy_root}$ represents mereotopological homomorphisms as those mappings which are homomorphisms of both the posets and the looped graphs that are the substructures of the mereographs for physical bodies and spatial regions.

It is worthwhile to review how the structures in $M^{occupy_root}$ are related to the ontological commitments we made in Section 3.4. The mereotopology for physical bodies is the substructure $Q \oplus C$ , which is distinct from the mereotopology for spatial regions, which is the substructure $P \oplus G$ . The Basic Harmony Principle, formalized as a homomorphism on these structures, is represented by the two substructures $Q \oplus I \oplus P$ (for the mereologies) and $C \oplus I \oplus G$ (for the connection structures). Since homomorphisms are mappings, each physical body occupies a unique spatial region.
4.3. Axiomatization

In this section, we provide and analyze the axiomatization of the ontology $T_{occupy_root}$ . Each class of mathematical structures that was introduced in the preceding section is axiomatized by a mathematical theory in COLORE (Common Logic Ontology Repository). For each mathematical theory, we will generate a subtheory of $T_{occupy_root}$ . In this way, the subtheories of $T_{occupy_root}$ mirror the different classes of mathematical structures that are amalgamated to construct an occupation structure. Corresponding to the four substructures of an occupation structure, the axioms of $T_{occupy_root}$ can be found by combining four subtheories, each of which is synonymous with a mathematical theory that axiomatizes one of the classes of mathematical structures.

We have already seen from Theorem 1 that $T_{mereograph}$ axiomatizes $M^{mereograph}$ . $T_{region_mt}$ is the theory in the signature $\begin{matrix} {region, part, C} \end{matrix}$ that is synonymous with $T_{mereograph}$ . In this way, the mereotopology of regions axiomatizes the relationship between the mereology on regions and the connection structure on regions.

Definition 10.
$T_{region_mt}$ is the following set of axioms $\begin{array}{l} (1) & (\forall x, y) part (x, y) \supset region (x) \land region (y) \\ (2) & (\forall x) region (x) \supset part (x, x) \\ (3) & (\forall x, y) part (x, y) \land part (y, x) \supset (x = y) \\ (4) & (\forall x, y, z) part (x, y) \land part (y, z) \supset part (x, z) \\ (5) & (\forall x, y) C (x, y) \supset region (x) \land region (y) \\ (6) & (\forall x) region (x) \supset C (x, x) \\ (7) & (\forall x, y) C (x, y) \supset C (y, x) \\ (8) & (\forall x, y, z) C (x, y) \land part (y, z) \supset C (x, z) \end{array}$

The modularity of $T_{region_mt}$ follows from the modularity of $T_{mereograph}$ . In particular, $T_{region_mereology}$ is the module of $T_{region_mt}$ consisting of Axioms (1)–(4), while $T_{region_connection}$ is the module of $T_{region_mt}$ consisting of Axioms (5)–(7).

Following the requirement of compositional pluralism, we combine a mereology on physical bodies and a connection structure on physical bodies to axiomatize a mereotopology on physical bodies:

$T_{physical_mt}$ is the theory in the signature $\begin{matrix} {physical_body, physical_part, physical_C} \end{matrix}$ that is synonymous with $T_{mereograph}$ .
Definition 11.
$T_{physical_mt}$ is the following set of axioms $\begin{array}{l} (9) & (\forall x, y) physical_part (x, y) \supset physical_body (x) \land physical_body (y) \\ (10) & (\forall x) physical_body (x) \supset physical_part (x, x) \\ (11) & (\forall x, y) physical_part (x, y) \land physical_part (y, x) \supset (x = y) \\ (12) & (\forall x, y, z) physical_part (x, y) \land physical_part (y, z) \supset physical_part (x, z) \\ (13) & (\forall x, y) physical_C (x, y) \supset physical_body (x) \land physical_body (y) \\ (14) & (\forall x) physical_body (x) \supset physical_C (x, x) \\ (15) & (\forall x, y) physical_C (x, y) \supset physical_C (y, x) \\ (16) & (\forall x, y, z) physical_C (x, y) \land physical_part (y, z) \supset physical_C (x, z) \end{array}$

The modularity of $T_{physical_mt}$ also follows from the modularity of $T_{mereograph}$ . In particular, $T_{region_mereology}$ is the module of $T_{physical_mt}$ consisting of Axioms (10)–(12), while $T_{region_connection}$ is the module of $T_{physical_mt}$ consisting of Axioms (13)–(16).

For the requirement of mereotopological harmony, we axiomatize location as a mapping on mereologies ( $T_{occupy_mereology}$ ) as well as a mapping on connection structures ( $T_{occupy_connection}$ ).

$T_{occupy_mereology}$ is the theory in the signature $\begin{matrix} {region, part, physical_body, physical_part} \end{matrix}$ that is synonymous with $T_{mapping_preserve}$ .
Definition 12.
$T_{occupy_mereology}$ is the extension of $T_{physical_mereology} \cup T_{region_mereology}$ with the following sentences $\begin{array}{l} (OCC.1) & (\forall x) region (x) \supset \neg physical_body (x) \\ (OCC.2) & (\forall x, y) occupies (x, y) \supset physical_body (x) \land region (y) \\ (OCC.3) & (\forall x, y, z) occupies (x, y) \land occupies (x, z) \supset (y = z) \\ (OCC.4) & (\forall x) physical_body (x) \supset (\exists y) occupies (x, y) \\ (OM.1) & (\forall x, y, r_{1}, r_{2}) physical_part (x, y) \land occupies (x, r_{1}) \land occupies (y, r_{2}) \supset part (r_{1}, r_{2}) \end{array}$

$T_{occupy_connection}$ is the theory in the signature $\begin{matrix} {region, C, physical_body, physical_C} \end{matrix}$ that is synonymous with $T_{mapping_preserve}$ .
Definition 13.
$T_{occupy_connection}$ is the extension of $T_{physical_connection} \cup T_{region_connection}$ with Axioms (OCC.1) – (OCC.4) and the following sentence $\begin{matrix} (OC.1) & (\forall x, y, r_{1}, r_{2}) physical_C (x, y) \land occupies (x, r_{1}) \land occupies (y, r_{2}) \supset C (r_{1}, r_{2}) \end{matrix}$

Having specified the subtheories that axiomatize the substructures, we can now specify the entire theory.
Definition 14.
$\begin{matrix} T_{occupy_root} = T_{physical_mt} \cup T_{region_mt} \cup T_{occupy_mereology} \cup T_{occupy_connection} \end{matrix}$

The relationships among the different modules of $T_{occupy_root}$ are shown in Fig. 5.

Fig. 5.
Modules of $T_{occupy_root}$ . Arrows denote conservative extension.

This illustrates a technique known as design by reuse. We first formalize the requirements for the ontology by specifying classes of mathematical structures and then find the theory in COLORE that axiomatizes the class of structures and finally we reuse this mathematical theory to propose the axioms of the ontology via synonymy, which also provides a modularization of the ontology. In a sense, the axioms of the ontology are generated from the mathematical theories via translation definitions.
4.4. Representation Theorem for $Mod (T_{occupy_root})$

To this point, we have specified a set of ontological commitments based on mereotopological pluralism, and formalized them as a class of intended structures $M^{occupy_root}$ . We have also proposed a set of axioms for the location ontology $T_{occupy_root}$ . In this section, we prove that there is a one-to-one correspondence between $M^{occupy_root}$ and the models of $T_{occupy_root}$ . The key to this result is the relationship between $T_{occupy_root}$ and the subtheories that axiomatize the substructures of structures in $M^{occupy_root}$ – mereographs, preservation mutligeometries, and looped graph homomorphism strucures.

Theorem 7.
$T_{occupy_root}$ is reducible to $T_{mt}$ , $T_{mereograph}$ , $T_{mapping_preserve}$ , $T_{graph_hom}$ .

Looking at Fig. 5, we see that the five subtheories that we presented above correspond to the modules of $T_{occupy_root}$ .
Corollary 1.
The reductive modules (Aameri et al., 2016 ) of $T_{occupy_root}$ are:

$T_{region_mt}$ , $T_{physical_mt}$ , $T_{occupy_mereology}$ , $T_{occupy_connection}$ .

The weak reductive modules (Aameri et al., 2016 ) of $T_{occupy_root}$ are:

$T_{region_mereology}$ , $T_{region_connection}$ , $T_{physical_mereology}$ , $T_{physical_connection}$ .

Each structure in $M^{occupy_root}$ is the amalgamation of the structures $Q \oplus C$ and $P \oplus G$ (mereographs), $Q \oplus I \oplus P$ (preserved multigeometry), and $C \oplus I \oplus G$ (graph homomorphism). Theorem 7 shows that each model of $T_{occupy_root}$ is the amalgamation of two models of $T_{mereograph}$ , a model of $T_{mapping_preserve}$ , and a model $T_{graph_hom}$ . Combining these two properties leads us to the following central result:
Theorem 8.
There exists a bijection $φ : Mod (T_{occupy_root}) \to M^{occupy_root}$ such that

$φ (⟨ M, region, part, C, physical_body, physical_part, physical_C ⟩) = Q \oplus C \oplus I \oplus P \oplus G$ iff
$M = V_{1} \cup V_{2}$ ;

$⟨ x, y ⟩ \in C$ iff $(x, y) \in E_{1}$ ;

$⟨ x, y ⟩ \in part$ iff $x ⪯ y$ .

$⟨ x, y ⟩ \in physical_C$ iff $(x, y) \in E_{2}$ ;

$⟨ x, y ⟩ \in physical_part$ iff $x ⩽ y$ .

$⟨ x, y ⟩ \in occupies$ iff $(x, y) \in I$ ;

This theorem provides a justification for $T_{occupy_root}$ as the root theory for a hierarchy (Gruninger et al., 2012) of location ontologies. It is strong enough to axiomatize the existence of homomorphisms between a mereotopology on physical bodies and a mereotopology on spatial regions. On the other hand, removing any axiom from $T_{occupy_root}$ would lead to unintended models where such a homomorphism does not exist (or we would fail to have a mereotopology on either physical bodies or regions).

One final methodological note – In this paper we have followed a methodology in which we begin with a set of ontological commitments which are formalized through the specification of a class of required structures, and then find a logical theory that axiomatizes the class of structures. An alternative approach (suggested by a reviewer) would be to start with an axiomatization, construct its models, and then show how these models are related to the original ontological commitments. However, this presumes that the axiomatization of the ontology already exists, and hence is more appropriate to ontology analysis, whereas we are designing the ontology from requirements.
4.5. Discussion

$T_{occupy_root}$ provides the weakest axiomatization required for representing location and occupation, however, in most applications a stronger theory is required. The most straightforward modification to $T_{occupy_root}$ is to adopt a stronger spatial mereotopology. This can be achieved by extending $T_{region_mt}$ to stronger theories such as CEMT and CEMTC. In this case, the only required alteration is relativizing the new mereotopology to regions. It is important to emphasis that from a model-theoretical perspective, such extensions only change substructures corresponding with the spatial mereotopology. That is, the class of homomorphisms we present in this paper can still be used for the characterization of embedding physical object into space.

Another way of strengthening $T_{occupy_root}$ is to extend $T_{physical_mt}$ , or adopt an object mereotopology which is totally different than $T_{physical_mt}$ . The only condition that must be satisfied is that the spatial mereotopology must be at least as strong as the object mereotopology.

Additionally, $T_{occupy_root}$ can be strengthened by extensions $T_{occupy_mereology} \cup T_{occupy_connection}$ that capture different mereological harmony principles.

In the reminder of this part we describe how $T_{occupy_root}$ can be used or extended to address competency questions stated in Section 2.

[CQ1]: The signature of $T_{occupy_root}$ can be extended by the new occupy, parthood and connection predicates for each class of physical objects, where parthood and connection predicates capture the mereotopological relations among objects in the class, and the occupy predicate maps each object to a spatial region. The axioms corresponding with each occupy predicate could be the same as those of $T_{occupy_root}$ .

[CQ2]: When a physical object moves, the occupy relation corresponding to that object changes; that is, the object is mapped into a different region. When an object expands, the region that it occupies before the expansion is a proper part of the region it occupies after the expansion. To fully represent any kind of spatial change one also needs to represent time and process. A possible approach for that is to convert all axioms of $T_{occupy_root}$ to state axioms in the language of some process ontology. A syntactical procedure for such a conversion can be found in Aameri’s work (2012).

[CQ3]: Addresses of objects can be defined with respect to the regions the objects and their addresses occupy. All objects with the same address occupy regions that are parts of the region the address occupies (e.g., the regions occupied by two books in the same warehouse are parts of the region that is occupied by the warehouse).

[CQ4]: In physics, a rigid body is an object in which the distance between any two given points on it remains constant in time. From a qualitative perspective, this implies that the region occupied by a rigid object is never a proper part of the region the object occupies in the next state. However, spatial embedding is not sufficient for representing rigid bodies since the above implication is not for example sufficient for distinguishing a moving rigid object from a non-rigid object that expands as it moves. Therefore, the Occupy Ontology is necessary for representing rigid objects, but not sufficient.

5. Relationship to other location ontologies

The focus of most of the existing spatial ontologies is on axiomatizing properties of spatial or spatio-temporal regions and only a few explicitly axiomatize location.

Two approaches are taken by the existing mereotopological ontologies: in one approach connection is considered as the primitive relation and parthood is defined in terms of connection. Examples of this approach can be found in the work by Randell et al. (1992) and Asher and Vieu (1995). In the second approach, which is also adopted by the Occupy Ontology, both connection and parthood are primitives and the ontology includes axioms describing how the two relations are combined. MT, CMT, and CEMT are examples of the second approach (Casati and Varzi, 1999).

Spatio-temporal ontologies consider space and time as a whole which can be represented by four-dimensional regions. They adopt a spatial mereotopology, replace spatial regions in the mereotopology by spatio-temporal regions, and extend the mereotopology by axioms that capture temporal relationships between the spatio-temporal regions. Muller (2002) for examples adopts the spatial mereotopology of Asher and Vieu (1995), while Stell and West (2004) present a spatio-temporal ontology extending RCC.

Multi-dimensional spatial ontologies, such as INCH (Gotts, 1996), GFO (Baumann et al., 2016) and CODI (Hahmann, 2013), introduce primitive relations among spatial entities with different dimensionality, which enable capturing properties of multi-dimensional spatial regions and spatial boundaries.

None of the above-mentioned ontologies consider location. In the reminder of this section we present a detailed review of those ontologies that include a formal theory of location and describe how those theories are related to $T_{occupy_root}$ and its extensions.

5.1. Casati and Varzi’s location ontology

Casati and Varzi’s location ontology (Casati and Varzi, 1999) extends the mereotopology CEMT7

⁷
Casati and Varzi actually use GEMTC, which is a second-order theory. But we only consider CEMTC which is the first-order part of GEMTC.

with the axioms in Fig. 6. As observed earlier, Casati and Varzi’s theory is based on compositional monism, since it does not include a separate mereotopology for objects and regions. Moreover, regions are not primitives, but are defined as those objects that are located in themselves. Their ontology does not include separate mereotopological predicates for objects and spatial regions. That is, in models of

T_{location_root}

a spatial region can be part of an object.

Fig. 6.

$T_{location_root}$ : Axioms for Varzi’s original location ontology.

Varzi’s location relation is antisymmetric, and transitive:

Proposition 1.

$\begin{array}{l} T_{location_root} ⊧ (\forall x, y) L (x, y) \land L (y, x) \supset (x = y) \\ T_{location_root} ⊧ (\forall x, y, z) L (x, y) \land L (y, z) \supset L (x, z) \end{array}$

This might indicate that $T_{location_root}$ is synonymous with some class of partial orderings, but the verification of $T_{location_root}$ faces several hurdles. In particular, there can exist elements in models of $T_{location_root}$ such that the elements themselves have no location (that is, they are non-spatial), but their parts have location. This is a general difficulty in characterizing the models of location ontologies based on compositional monism.

Theorem 9.

$T_{location_root}$ is interpretable in $T_{occupy_root} \cup T_{cem_mereology}$ .

$T_{location_root}$ allows entities with no location. To capture mereological harmony (the mereotopological relations between objects are mirrored in the underlying spatial regions), additional axioms are needed.

Definition 15.

$T_{mt_location}$ is the extension of $T_{location_root}$ with the following axioms: $\begin{array}{l} (CV.4) & P (x, y) \land L (x, z) \land L (y, w) \supset P (z, w) . \\ (CV.5) & C (x, y) \land L (x, z) \land L (y, w) \supset C (z, w) . \end{array}$

Since axioms of $T_{mt_location}$ are conditional, $T_{mt_location}$ does not eliminate the existence of non-spatial elements that have spatial parts (Parsons, 2007).

Although a definitional extension of $T_{occupy_root}$ entails Sentences 17 and 18, which are very similar to the above axioms, $T_{occupy_root}$ does not interpret Axioms (CV.4) and (CV.5) . $\begin{array}{l} (17) & physical_part (x, y) \land L (x, z) \land L (y, w) \supset part (z, w) \\ (18) & physical_C (x, y) \land L (x, z) \land L (y, w) \supset C (z, w) \end{array}$

The main reason is that the P and C relations in models of $T_{mt_location}$ are not definable in models of $T_{occupy_root}$ : Both P and C may relate a spatial region to an element which is not a region (e.g., $T_{mt_location}$ allows a model in which x is a spatial region, y is a physical object, and x is part of y). However, within models of $T_{occupy_root}$ , the relationships between regions and non-region elements are specified using $occupy$ , which has very different properties than P and C. The relations in the signature of $T_{occupy_root}$ are restricted either to regions or non-region objects and hence the mereotopological relationships between region and non-region elements cannot be defined in models of $T_{occupy_root}$ .

5.2. BIT location ontologies

Basic Inclusion Theory (BIT; Donnelly et al., 2006) is a first-order theory of parthood and location which is developed for the purpose of qualitative spatial reasoning in biology and medicine. Like $T_{occupy_root}$ , BIT includes a mereology extended by axioms about location relations (hence, the theory is based on compositional monism). Moreover, parthood/connection relationship between elements guarantees parthood/connection relationship between regions they occupy (that is, the theory follows the Basic Harmony Principle). A function, r, maps each individual to the region at which it is located. In addition, BIT assumes that the region of a region is that region itself:

Fig. 7.

$T_{bit}$ : Axioms for Basic Inclusion Theory (BIT).

Location relations are defined based on the region function and the parthood relation: $\begin{matrix} (BIT.3) & LocIn (x, y) \equiv P (r (x), r (y)) . \end{matrix}$ Notice that $LocIn$ represents partial location, and not exact location.

The main difference between BIT location ontology and Casati and Varzi’s theory is that in Casati and Varzi’s theory location is a primitive relation and regions are defined in terms of location, while in BIT the region function is primitive and location can be defined based on the region function. Nevertheless, we have the following:

Theorem 10.

$T_{bit}$ (see Fig. 7 ) is synonymous with $T_{mt_location} \cup T_{nontrivial_region}$ . 8

⁸

colore.oor.net/location_varzi/nontrivial_loc.clif

Corollary 2.

$T_{bit}$ is interpretable by $T_{mt_occupy}$ .

5.3. SUMO location ontology

Suggested Upper Merged Ontology (SUMO; Pease et al., 2002) is an upper ontology intended to capture general concepts such as time and location. According to SUMO, every physical object is located on an individual and associated with a time: $\begin{matrix} (19) & Physical (x) \supset (\exists y, z) located (x, y) \land time (x, z) . \end{matrix}$

SUMO makes distinction between physical bodies and spatial regions (i.e., it takes substantivalism) but it makes ontological commitments which restrict its reusability. For example, it assumes that for every region, there exists an individual which is located on the region, which is not the case in many applications: $\begin{matrix} (20) & Region (x) \supset (\exists y) located (y, x) . \end{matrix}$

The ontology contains three locative primitives, namely $located$ , $exactlyLocated$ , and $partlyLocated$ . $located$ and $exactlyLocated$ are antisymmetric. In addition, $located$ is transitive. $exactlyLocated$ is stronger than $located$ , and $located$ is stronger than $partlyLocated$ . Than is, if an element is exactly located on an element, then it is also located on the same element, and if it is located on an element, then it is partly located on that element. Moreover, all parts of an individual are located where the individual is located: $\begin{matrix} (21) & located (x, y) \land part (s, x) \supset located (s, y) . \end{matrix}$

6. Summary

In this paper, we propose a new approach to the axiomatization of location ontologies based on the philosophical stance of merelogical pluralism, in which one uses different mereologies for different kinds of entities. In particular, we make the fundamental ontological commitment that the mereology for spatial regions is different than the mereology for physical bodies. The ontology we propose, $T_{occupy_root}$ , axiomatizes location as a homomorphism from the mereotopology of physical bodies to the mereotopology of regions in abstract space. We also provide a characterization of the models of the axiomatization $T_{occupy_root}$ up to isomorphism.

Two sequels to this paper will appear in the future. The first is a rigorous axiomatization of the different mereological harmony principles that have been proposed in the philosophical literature by Uzquiano (2011) and Leonard (2016). In this paper we have shown that the models of our location ontology $T_{occupy_root}$ correspond to homomorphisms of the mereologies and connection structures in the mereotopologies of physical bodies and spatial regions. Such homomorphisms formalize the Basic Harmony Principle. In the future paper, we show how the different mereological harmony principles are formalized by different classes of poset and graph homomorphisms.

Several approaches axiomatize location ontologies as time-varying, introducing an additional argument for a time object. This is typically used to represent motion as the change in location for a physical body (see the Motivating scenarios in Section 2). The second sequel to this paper will use the methodology of Aameri (2012) to the Occupy Ontology to axiomatize motion as a change in location.

Footnotes

Notation

Proofs of theorems

References

Aameri, B. (2012). Using partial automorphisms to design process ontologies. In Proceedings of the 7th International Conference on Formal Ontology in Information Systems (pp. 309–322). IOS Press.

Aameri, B. & Gruninger, M. (2015). A new look at ontology correctness. In 2015 AAAI Spring Symposium Series. AAAI Press.

Aameri, B. & Gruninger, M. (2017). Encountering the physical world. In Proceedings of the Joint Ontology Workshops 2017.

Aameri, B., Grüninger, M. & Chui, C. (2016). Anti-modules. In Proceedings of the Joint Ontology Workshops (JOWO at FOIS). CEUR Workshop Proceedings (Vol. 1660).

Asher, N. & Vieu, L. (1995). Toward a geometry of common sense: A semantics and a complete axiomatization of mereotopology. In IJCAI (pp. 846–852).

Baumann, R., Loebe, F. & Herre, H. (2016). Towards an ontology of space for GFO. In FOIS2016 (pp. 53–66).

Borgo, S., Guarino, N. & Masolo, C. (1997). An ontological theory of physical objects. In Proceedings of Qualitative Reasoning 11th International Workshop (pp. 223–231).

Casati, R. & Varzi, A. (1999). Parts and Places: The Structures of Spatial Representation. MIT Press.

Cohn, A.G., Bennett, B., Gooday, J. & Gotts, N. (1997). RCC: A calculus for region-based qualitative spatial reasoning. GeoInformatica, 1, 275–316. doi:10.1023/A:1009712514511.

10.

Donnelly, M., Bittner, T. & Rosse, C. (2006). A formal theory for spatial representation and reasoning in biomedical ontologies. Artificial Intelligence in Medicine, 36(1), 1–27. doi:10.1016/j.artmed.2005.07.004.

11.

Gilmore, C. (2017). Location and mereology. In

E.N.

Zalta (Ed.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, fall 2017 edition.

12.

Gotts, N.M. (1996). Formalising commonsense topology: The INCH calculus. In Proc. Fourth International Symposium on Artificial Intelligence and Mathematics.

13.

Grüninger, M. & Aameri, B. (2017). A new perspective on the mereotopology of RCC8. In Proceeding of the 13th International Conference on Spatial Information Theory (COSIT 2017). Leibniz International Proceedings in Informatics (pp. 2:1–2:13).

14.

Gruninger, M., Hahmann, T., Hashemi, A. & Ong, D. (2010). Ontology verification with repositories. In Proc. of the 6th Int. Conference on Formal Ontologies in Information Systems (FOIS2010) (pp. 317–330). IOS Press.

15.

Gruninger, M., Hahmann, T., Hashemi, A., Ong, D. & Ozgovde, A. (2012). Modular first-order ontologies via repositories. Applied Ontology, 7(2), 169–209. doi:10.3233/AO-2012-0106.

16.

Hahmann, T. (2013). A reconciliation of logical representations of space: From multidimensional mereotopology to geometry. PhD thesis, Univ. of Toronto, Dept. of Comp. Science.

17.

Lehmkuhl, D. (2018). The metaphysics of super-substantivalism. Noûs, 52(1), 24–46.

18.

Leonard, M. (2016). What is mereological harmony? Synthese, 193, 1949–1965.

19.

Lewis, D. (1991). Parts of Classes. Blackwell.

20.

Markosian, N. (2014). A spatial approach to mereology. In

Kleinschmidt (Ed.), Mereology and Location. Oxford University Press.

21.

McDaniel, K. (2004). Modal realism with overlap. Australasian Journal of Philosophy, 82, 137–152. doi:10.1080/713659792.

22.

McDaniel, K. (2007). Extended simples. Philosophical Studies, 133, 131–141. doi:10.1007/s11098-006-9010-y.

23.

McKeon, R. (2009). The Basic Works of Aristotle. Modern Library.

24.

Muller, P. (2002). Topological spatio-temporal reasoning and representation. Computational Intelligence, 18(3), 420–450. doi:10.1111/1467-8640.00196.

25.

Parsons, J. (2007). Theories of location. Oxford Studies in Metaphysics, 3, 201–232.

26.

Pease, A., Niles, I. & Li, J. (2002). The suggested upper merged ontology: A large ontology for the semantic web and its applications. In Working Notes of the AAAI-2002 Workshop on Ontologies and the Semantic Web (Vol. 28).

27.

Randell, D.A., Cui, Z. & Cohn, A. (1992). A spatial logic based on regions and connection. In Proceedings of the Third International Conference Principles of Knowledge Representation and Reasoning (pp. 165–176). San Mateo, California: Morgan Kaufmann.

28.

Saucedo, R. (2011). Parthood of location. Oxford Studies in Metaphysics, 6, 225–294. doi:10.1093/acprof:oso/9780199603039.003.0008.

29.

Schaffer, J. (2009). Spacetime the one substance. Philosophical Studies, 145, 131–148. doi:10.1007/s11098-009-9386-6.

30.

Schröder, B. (2003). Ordered Sets: An Introduction. Springer.

31.

Sider, T. (2007). Parthood. Philosophical Review, 116, 51–91. doi:10.1215/00318108-2006-022.

32.

Sklar, L. (1974). Space, Time, and Spacetime. University of California Press.

33.

Stell, J.G. (2000). Boolean connection algebras: A new approach to the region-connection calculus. Artificial Intelligence, 122, 111–136. doi:10.1016/S0004-3702(00)00045-X.

34.

Stell, J.G. & West, M. (2004). A four-dimensionalist mereotopology. In Proceedings of the International Conference on Formal Ontology in Information Systems (pp. 261–272).

35.

Uzquiano, G. (2011). Mereological harmony. Oxford Studies in Metaphysics, 6, 199–224. doi:10.1093/acprof:oso/9780199603039.003.0007.