Towards a reference ontology of the spatial location of physical objects

Abstract

Expressing spatial location and spatial relations between physical objects is an essential requirement for building conceptual models for domains that deal with the material world. Although the Unified Foundational Ontology (UFO) provides a well-founded ontological theory implemented in a suite of languages that aid in building ontology-driven conceptual models, it still lacks a theory for the spatial location of physical objects. This paper proposes a reference ontology in which spatial location is an intrinsic moment of physical objects. Spatial regions are the possible values of spatial locations, and they are part of abstract relative spaces. We propose a taxonomy of spatial relations, adapted from the Region Connection Calculus (RCC), that hold either between two spatial regions or physical objects. The ontology is implemented both in OntoUML and first-order logic.

1. Introduction

The representation of space and how entities are spatially related is a foundational problem. Spatial information is necessary in multiple domains that deals with locations and position of entities, including geology, engineering, geography, and robotics. The metaphysics of space is a particular contentious subject and, as a consequence, diferent ontologies adopt diferent views or modeling strategies to deal with space [ 1, 2, 3, 4 ]. In addition, many notions have been developed in the fields of mereotopology [ 5, 6 ] and spatial reasoning [ 7 ], which give insight in how to integrate spatial location into foundational

CEUR Workshop

ISSN1613-0073 • CQ3 - How do we compare the spatial location of physical objects? • CQ4 - How does spatial location relate to mereology and constitution?

To achieve this goal, we propose a first-order logic (FOL) formalization of the concepts used, extending the UFO theory proposed in [ 8 ]. This FOL theory is implemented in an interactive theorem prover [ 11 ]. We also complement this formalization with an OntoUML model.

The remainder of this work is organized as follows. In Section 2, we provide a short review of the philosophical concepts regarding the ontology of space. Section 3 summarizes how other top-level ontologies model the space or the spatial location of objects. Section 4 provides the main concepts of the Unified Foundational Ontology (UFO) that grounds the proposed ontology. Section 5 presents the contribution of this work, a reference ontology for the spatial location of physical objects. We conclude the paper in Section 6 with the discussions and final considerations.

2. Background

In this chapter, we outline the key concepts and metaphysical discussion about space that frame the ontological modeling decisions taken in the remainder of this work. The first important debate is about the metaphysical nature of space itself. There are two main thesis in this regard, named the absolutist view and the relational view. Discussions between these two views go back to Newton, who defended an absolutist view, and Leibniz, who argued in favor of the relational view [ 12, 5 ].

The absolutist view treats space as a substantive container that exists independently of any objects. In this view, space is metaphysically prior to other entities [ 12 ]. Space exists before and after other physical entities, but not the inverse. A relational view rejects space as an independent entity, and defends that it is relative to the relationship of the physical objects [ 13 ]. This debate has immediate consequences on how to include space (and spatial regions) in foundational ontologies. An approach following the absolutist view will consider spatial regions as concrete independent individuals. A relational-based approach would not. In fact, the standard relational would not include space and spatial regions in the universe of discourse at all, only the spatial relations between physical objects.

One further distinction, is between absolute and relative space [ 14 ]. A relative space is defined in relation to one or more reference object. Furthermore, while absolute space is unique, multiple relative spaces might exist using distinct objects as references. These relative spaces is what is commonly used for representing and reasoning about space [ 14 ]. We defend that these relative spaces (sometimes called reference frames and the coordinate systems associated with them) are also compatible with a relational view of space. In this view, a relative space is a conceptual cognitive space [sensu 15]. And the spatial regions that are included in this relative space are abstract entities derived from physical objects and the spatial relation between them.

Now, assuming a relational view, spatial relations do exist. And they only hold directly between physical objects1. So, there is a property of physical objects of being spatially extended and being related to each other. We reify this property as the spatial location of a physical object. It is an intrinsic moment, a quality [sensu 9], that have spatial regions as its possible values. And, in that sense, spatial regions are a way of qualifying the spatial relation between objects.

3. Related Work

In this chapter, we summarize how three upper-level ontologies (DOLCE, BFO, and SUMO) handle space or spatial location of entities. Each reflects a diferent design philosophy (descriptive vs. realist vs. integration-focused), influencing their treatment of space.

DOLCE (Descriptive Ontology for Linguistic and Cognitive Engineering) [ 2, 16 ] is a foundational ontology that emphasizes cognitive distinctions and descriptive adequacy. In DOLCE, spatial location 1It is possible to derive that spatial relations hold indirectly between other types of entities. For example, qualities and events. But that will only be true in virtue of the spatial relations between physical bearers and participants, respectively. is reified as a kind of quality [ 2 ]. Every physical object (a physical endurant in DOLCE) has a spatial location, and this quality’s “value” is what DOLCE considers a space region [ 2 ]. In other words, DOLCE does not treat spatial regions as concrete entities; rather, a space region is an abstract entity, existing outside of space and time [ 2 ]. DOLCE also aligns with a region-based structure of physical space i.e., regions are the primitive entity for their abstract conceptual spaces. DOLCE’s approach follows a descriptive (or cognitive) way of modeling space. Although there is no specific commitment against an absolute concrete space, they argue that this stance allows homogeneity and neutrality regarding the properties of space that can be adopted using their framework [ 2 ].

BFO (Basic Formal Ontology) [17] is an upper ontology rooted in realist philosophy, and it is used heavily in scientific domains. BFO explicitly includes spatial regions as part of its independent continuant taxonomic branch [17]. Spatial Region is a class of immaterial continuants, they are entities that persist through time but are not material objects. They are efectively the “pieces of space” that material entities occupy. BFO further describes a spatial region as a 0D, 1D, 2D, or 3D extent in space (point, line, surface, volume)[18].

Although spatial regions are independent continuants, they “are continuants of a peculiar (“abstract”) sort” [17, p. 115]. They have no qualities other than shape, size, and relative location [18]. They are pure spatial extents. Moreover, BFO’s documentation clearly requires that spatial regions be defined in terms of reference frame: “We recommend that users of BFO: spatial region specify the coordinate frame which they are employing…” [18]. For example, if one is talking about a spatial region on Earth’s surface, one should specify that it’s relative to the latitude/longitude frame [18].

BFO thus takes what we consider to be a hybrid approach regarding space. They classify spatial regions as independent continuants, a decision that is compatible with an absolutist view of space. But they recommend using frame of references associated and accept a sort of “abstract” nature for spatial regions, position that lean towards an relational view.

SUMO (Suggested Upper Merged Ontology)[19] was developed as a proposed standard upper ontology for the IEEE, with the aim of combining content from multiple existing ontologies. SUMO includes the concept of Region as a kind of physical entity [20]. However, a Region is a topographic location, which is more related to the concepts of Feature in Dolce and Site in BFO. From our understanding, Region is not meant to represent “spatial region” as a portion of space. Nevertheless, SUMO provides a set of relations for how objects are located on each other, and also how they are topologically related.

4. Unified Foundational Ontology

Our proposed ontology of spatial locations is grounded on the Unified Foundational Ontology (UFO) [ 9 ]. In this section, we review the main concepts used in this work. We refer to [ 8 ] for a complete overview of UFO. The foundational reference ontology is implemented in OntoUML [ 9 ], a well-founded profile of UML with rules established in UFO. It is also formalized using a quantified modal logic in the works of [ 9, 21, 8 ].

UFO taxonomy starts with the core diferentiation between types (things that have instances) and individual entities (things that do not have instances). Individuals are further classified into perdurants (events) and endurants. Endurants are entities that persist through time while maintaining their identity and being completely present at each instant. Endurants are further divided into moments and substantials.

Substantials, in UFO, include both entities that are founded in matter and parasitic entities (such as holes) [ 9 ]. Substantials are further classified in functional complexes, collectives and quantitites. UFO also includes a division of objects 2 in physical objects and social objects [22].

Moments represent reified aspects of an endurant, upon which they are existentially dependent. Moments are related to their bearers through an inheres in relation. Moments can be extrinsic (if they existentially depend on something else than their bearers) or intrinsic (depend solely on their bearers). 2In their seminal work, [ 9 ] use the term “object” to refer to a type specialized by functional complex, collective, and quantity. However, the term “object” is used as equivalent to functional complex in [ 8 ]. We follow the former. Intrinsic moments are classified in qualities (have a value in a quality space) and modes (do not have mensurable values, e.g., an intention, a thought, a capability).

UFO also features types as things in the world that can instantiate higher-order types [23]. UFO has a taxonomy of endurant types, structured according to metaproperties of sortality and rigidity. In UFO, types are categorized as either sortals or non-sortals, based on whether their instances have a unique identity criterion. Regarding rigidity, an endurant type might be rigid (if it is necessary for all its instances), anti-rigid (if it is contingent for all its instances), or semi-rigid (necessary for some, contingent for others).

Although UFO adopts a realist view towards qualities, it takes qualia (quality values) and quality structures as abstract entities [ 9 ]. Similarly to DOLCE [16], UFO uses the notion of conceptual spaces [ 15 ], and splits quality, as a concrete specifically dependent endurant, from its value on a quality structure.

The value of a quality is distinct from the quality itself and is named Quale. A Quale is defined as “a point in a n-dimensional quality domain can be represented as a vector =< 1... > where each represents each of the integral dimensions that constitute the domain” [9, p. 227]. Although [ 9 ] use the term point in their definition, the examples used show some flexibility. For instance, something that is a “point” of a certain quality domain, such as a quale red in an enumerated color domain, could be corresponding to a region in the other, red would be a region in the RGB or HSV color domain. Thus, we may represent an apple as bearing an instance of color quality, and that particular color has red as its value.

Zamborlini and Guizzardi [24] defend a replacement view, in which qualities cannot change their qualia; instead, they are replaced by some other particular quality with a distinct value. For instance, an apple a might bear a color quality instance c with a value red at a certain instant and, at a distinct instant, have a diferent color quality instance c” with a value brown. Guizzardi et al. [ 8 ][p. 25] adopt the opposite view and state that the relation between a quality and its value is one of generic dependence. According to this view, qualities can change their values.

5. A Spatial Location Ontology

In this work, we propose a formalization in first-order logic (FOL) that is complemented by an OntoUML model that is reusable by other ontologies3. We adopt some notation conventions used regularly in the UFO literature [ 21, 8 ] to simplify the following formalizations. Free variables are implicitly universally quantified. Predicates are in typewriter type, with upper camel case used for the unary predicates and the lower camel case used for the higher-arity predicates. The “d=ef” symbol is used to introduce predicates derived from primitive notions. The “∃!” symbol represents unique existential quantification. The axioms, theorems and definitions are indexed using ”(a n)”, ”(tn)”, ”(dn)”, respectively. The ”UFO:” prefix is used to refer to the predicates defined in [ 8 ]. The theorem proofs are implemented in the Lean proof assistant language [ 11 ] and available in a public repository3.

The quantification domain is restricted to UFO:Individuals. We use the following list of symbols as variables: ”, , , , 1, ..., ”, where n is a natural number. Although variables can be used interchangeably, to aid in the readability of the formalization, we will use the symbols r, whenever the variables are restricted to regions.

5.1. A formalization of regions

In our spatial ontology we adopt a region-based point-free representation of physical space [ 7, 1, 25, 6, 26, 27 ], treating it as a conceptual space [sensu 15]. This choice is motivated both cognitively and pragmatically. Cognitively, regions better reflect human spatial perception, since points are never directly perceived [ 1 ]. Pragmatically, regions sufice to express qualitative spatial relations without first deriving them from a point primitive. 3The artifacts generated in this work are available in https://github.com/UFO-GEO/spatial-location-ontology

Beyond serving as the values of objects’ spatial locations, regions can play the same role in any geometric conceptual space. Hence, we give a broad definition of region that encompasses both regions as subsets of a quality structure and as urelements (primitive elements). Therefore, a Region is an

UFO:AbstractIndividual (a1). A QualityRegion is a Region that subsets a UFO:QualityStructure (d1) [9, 28]. A RegionQuale is a Region that is also a UFO:Quale (d2). QualityRegion and

RegionQuale form a disjoint (t1)4 and incomplete (a2) partition of Region. (a1) Region() → UFO:AbstractIndividual() (d1) QualityRegion() d=ef Region() ∧ ∃( UFO:QualityStructure() ∧ ⊂ ) (d2) RegionQuale() d=ef Region() ∧ Quale() (t1)

¬(RegionQuale() ∧ QualityRegion()) (a2) ∃( Region() ∧ ¬( RegionQuale() ∨ QualityRegion())) 5.1.1. Binary relations With regions positioned in the taxonomy of UFO’s abstract individuals, we can propose our region-based topological theory, which is based on the Region Connection Calculus (RCC) [ 7 ]. We change the names of the relations to avoid abbreviations and also because UFO already uses some names used by [ 7 ] in their mereology formalization [ 8 ]5.

The isRegionConnectedTo6 is an external non-descriptive relation between two regions (a3). The classification as non-descriptive and external is because we do not have any intrinsic property of the relata to which we can reduce the isRegionConnectedTo relation [29]. A region is connected to another if “the topological closures of the two regions share at least one point” [7, p. 102]. The isRegionConnectedTo relation is symmetric (a4), reflexive ( a5) and intransitive (a6). (a3) isRegionConnectedTo( 1, 2) → Region( 1) ∧ Region( 2) (a4)

Region() → isRegionConnectedTo(, )

(a5) isRegionConnectedTo( 1, 2) ↔ isRegionConnectedTo( 2, 1) (a6) ∃ 1, 2, 3(isRegionConnectedTo( 1, 2) ∧ isRegionConnectedTo( 2, 3)∧

¬isRegionConnectedTo( 1, 3))

From the isRegionConnectedTo relation, we can define a set of spatial relations between spatial regions (d3-d15) (Fig. 1). We also need the axiom that isRegionIdenticalWith is equivalent to the identity relation (a7). Let ℒ be the set of leaf sub-types of binary spatial relations {isRegionIdenticalWith, isRegionDisconnectedFrom, regionPartiallyOverlaps, isRegionExternallyConnectedTo, isRegionTangentialProperPartOf, hasRegionTangentialProperPart, isRegionNonTangentialProperPartOf, hasRegionNonTangentialProperPart}. These leaf relation types are pairwise disjoint (t2) 7 and complete (t3) (Fig. 2). (d3) isRegionDisconnectedTo( 1, 2) d=ef Region( 1) ∧ Region( 2) ∧ ¬isRegionConnectedTo( 1, 2) def (d4) isRegionPartOf( 1, 2) = Region( 1) ∧ Region( 2)∧

∀ 3(isRegionConnectedTo( 3, 1) → isRegionConnectedTo( 3, 2)) (d5) hasRegionPart( 1, 2) d=ef isRegionPartOf( 2, 1) (d6) isRegionProperPartOf( 1, 2) d=ef isRegionPartOf( 1, 2) ∧ ¬isRegionPartOf( 2, 1) (d7) hasRegionProperPart( 1, 2) d=ef isRegionProperPartOf( 2, 1) 4The proof relies on the axiom stating that UFO:Quale and UFO:Set are disjoint [8, p.16 a85] 5For instance, UFO:P [ 8 ], which stands for “is part of”, is used in a topo-mereological sense. 6The isRegionConnectedTo relation is equivalent to the “C” relation in [ 7 ] 7The theorem proofs are included in the supplementary materials3. In there, the disjunction theorem is divided into each pair. (d12) isRegionExternallyConnectedTo( 1, 2) d=ef isRegionConnectedTo( 1, 2)∧ ¬regionOverlaps( 1, 2) (d13) isRegionTangentialProperPartOf( 1, 2) d=ef isRegionProperPartOf( 1, 2)∧ ∃ 3(isRegionExternallyConnectedTo( 3, 1) ∧ isRegionExternallyConnectedTo( 3, 2)) (d14) hasRegionTangentialProperPart( 1, 2) d=ef isRegionTangentialProperPartOf( 2, 1) (d15) isRegionNonTangentialProperPartOf( 1, 2) d=ef isRegionProperPartOf( 1, 2)∧ ¬∃ 3(isRegionExternallyConnectedTo( 3, 1) ∧ isRegionExternallyConnectedTo( 3, 2)) (d16) hasRegionNonTangentialProperPart( 1, 2) d=ef isRegionNonTangentialProperPartOf( 2, 1) (a7) isRegionIdenticalWith( 1, 2) ↔ Region( 1) ∧ Region( 2) ∧ 1 = 2 (t2)

⋀ ,∈ℒ ,≠

¬(( 1, 2) ∧ ( 1, 2)) (t3) Region( 1) ∧ Region( 2) → ⋁ ( 1, 2)

∈ℒ

Regions follow a classical mereology [sensu 30]. Therefore, we need a supplementation principle to state that if a region has another region as proper part, there must be a complementary part of the larger region. Then, there is a remainder axiom (a8) for regions, that encapsulate this notion in a general form [based on 30, p.25]. (a8) Region( 1) ∧ Region( 2) ∧ ¬isRegionPartOf( 1, 2) → (∃ 3(Region( 3)∧

∀ 4(isRegionPartOf( 4, 3) ↔ (isRegionPartOf( 4, 1) ∧ isRegionDiscreteFrom( 4, 2))))) 5.1.2. Ternary relations Beyond the binary relations between regions defined above, there is also a set of “Boolean functions” [sensu 7] that are useful to add expressiveness to the theory. Diferently from [ 7 ], we define these operations as ternary predicates. First, the regionsUnion relation holds between three spatial regions in which the third relatum is the sum of the first two relata. Therefore, every region connected to the third relatum is also connected to either the first region or the second region ( d17). For every two spatial regions, there is a unique spatial region that is their sum (existence by a9 8 and uniqueness by t4). The relation regionsUnion is also commutative (t5) and idempotent (t6). (d17) regionsUnion( 1, 2, 3) d=ef Region( 1) ∧ Region( 2) ∧ Region( 3)∧ ∀ 4(isRegionConnectedTo( 4, 3) ↔ (isRegionConnectedTo( 4, 1)∨

isRegionConnectedTo( 4, 2))) (a9) Region( 1) ∧ Region( 2) → ∃ 3(regionsUnion( 1, 2, 3)) (t4) (t5) regionsUnion( 1, 2, 3) ↔ regionsUnion( 2, 1, 3) (t6) Region() → regionsUnion(, , )

regionsUnion( 1, 2, 3) ∧ regionsUnion( 1, 2, 4) → 3 = 4

Second, the regionsDifference relation holds between three regions in which the third is the diference between the two first regions. Therefore, every region that is part of the third region is also part of the first region, but not part of the second region ( d18). The existence of a diference between two regions is conditional to the first not being part of the second ( t7). The diference between two regions is unique (t8). And lastly, the diference is not commutative ( t9). (d18) regionsDifference( 1, 2, 3) d=ef Region( 1) ∧ Region( 2) ∧ Region( 3)∧

∀ 4(isRegionPartOf( 4, 3) ↔ (isRegionPartOf( 4, 1) ∧ ¬regionOverlaps( 4, 2))) (t7) (t8) (t9)

Region( 1) ∧ Region( 2) → (¬isRegionPartOf( 1, 2) ↔ ∃ 3(regionsDifference( 1, 2, 3))) regionsDifference( 1, 2, 3) ∧ regionsDifference( 1, 2, 4) → 3 = 4 regionsDifference(1, 2, 3) → ¬ regionsDifference(2, 1, 3)

Third, the regionIntersection predicate holds between two regions and a third region which includes all mutual parts of the two first regions ( d19). The existence of an intersection region is conditional to the first two regions overlapping ( t10). The region intersection is also unique (t11) and idempotent (t12). (d19) regionsIntersection( 1, 2, 3) d=ef Region( 1) ∧ Region( 2) ∧ Region( 3)∧

∀ 4(isRegionPartOf( 4, 3) ↔ isRegionPartOf( 4, 1) ∧ isRegionPartOf( 4, 2)) (t10) Region( 1) ∧ Region( 2) → (regionOverlaps( 1, 2) ↔ ∃ 3(regionsIntersection( 1, 2, 3))) (t11) regionsIntersection( 1, 2, 3) ∧ regionsIntersection( 1, 2, 4) → 3 = 4 (t12) Region() → regionsIntersection(, , ) 8This axiom means that there is unrestricted fusion [sensu 30] between regions. 5.1.3. Convex hull and concave hull Although we can express many spatial location facts using the isRegionConnectedTo and derived relations, there are some that we do not. Among those, one of particular interest is the convexity of regions. Let us use three examples: “the cofee is contained in the mug”, “the hand holds the mug”, and “a sponge is soaked with water” (Fig. 3). If we model only the spatial relation of the spatial regions in which these entities are located, in each example the two objects would all be externally connected, but we can add expressivity by including a couple of primitive relations to our proposed ontology, that would help diferentiate the illustrative cases above.

Before presenting these relations, we will define some concepts. A convex region is a region in which any two points inside could be connected through a straight line contained in the region. A concave region is a region that is not convex. The convex hull of a region r is the smallest convex region which has region r as a part. A concave hull of a region x is a concave region, that contains the region x and is contained by its convex hull. It is sort of an “intermediate” between a region and its convex hull that includes internal holes but not external holes.

Using the definitions above, we could analyze the three examples in Fig. 3. If “the cofee is contained in the mug” and “the hand holds the mug”, we can assert for that specific case, using regions, that the cofee-location region is externally connected to the mug-location region, and it is a proper part of the mug-location convex hull, while the hand-location region is externally connected to both the mug-location region and its convex hull (Fig. 3A). Of course, diferent configurations of reality will require diferent assertions, such as if the mug has a handle and someone grabs it. In that case, one could describe the convex hull of the handle as diferent from the convex hull of the body, and each diferently related to the hand-location region and the cofee-location region.

If “a sponge is soaked with water”, considering that it has a concave shape, we can select a concave hull9 (of the many possible) and the convex hull, and assert that the water-location region is externally connected to the sponge-location region and is a proper part of that particular concave hull (Fig. 3B). In this case, we could also assert that the union of the water-location and sponge-location regions is equal to that particular concave hull.

We formalize the concepts described above by including hasConvexHull and hasConcaveHull as primitive relations that hold between regions and their convex hull and concave hulls, respectively. Since we do not have internal angles or points in our theory, we will define convex and concave regions using these two relations in the next section (Section 5.1.4).

The hasConvexHull relation holds between two regions (a10), it is idempotent (a11), and consequently transitive (t13). Every region has a unique convex hull (a12). A region is either a tangential proper part or identical to its convex hull (a13). The hasConvexHull relation is monotonic, therefore, if a region is part of another region, the convex hull of the first region is also part of the convex hull of 9Selecting which concave hull is best for any purpose is an epistemic issue that is domain-specific. Our intention in this work is simply state that concave hulls exist and that they are arguably useful to express facts about physical objects. the second region (a14). Some of the axioms described above (a11, a13 and a14) are translated directly from RCC [ 7 ]. The remaining axioms of convexity from RCC are not included because their entailment is still being evaluated. (a10) hasConvexHull( 1, 2) → Region( 1) ∧ Region( 2) (a11) hasConvexHull( 1, 2) ∧ hasConvexHull( 2, 3) → 2 = 3 (t13) hasConvexHull( 1, 2) ∧ hasConvexHull( 2, 3) → hasConvexHull( 1, 3) (a12) Region( 1) → ∃! 2(hasConvexHull( 1, 2)) (a13) hasConvexHull( 1, 2) → isRegionTangentialProperPartOf( 1, 2)∨

isRegionEqualWith( 1, 2) (a14) isRegionPartOf( 1, 2) ∧ hasConvexHull( 1, 3) ∧ hasConvexHull( 2, 4) → isRegionPartOf( 3, 4)

The hasConcaveHull relation holds between two concave spatial regions (a15). A region is a proper tangential part or equal to any of its concave hulls (a16). Unlike convex hulls, concave hulls are not necessarily unique; therefore, some regions might have multiple concave hulls (a17). Lastly, a region’s convex hull is also the convex hull of the region’s concave hulls (a18). (a15) hasConcaveHull( 1, 2) → Region( 1) ∧ Region( 2) (a16) hasConcaveHull( 1, 2) → isRegionTangentialProperPartOf( 1, 2)∨

isRegionIdenticalWith( 1, 2) (a17) ∃ 1, 2, 3(hasConcaveHull( 1, 2) ∧ hasConcaveHull( 1, 3) ∧ 2 ≠ 3) (a18) hasConcaveHull( 1, 2) ∧ hasConvexHull( 1, 3) → hasConvexHull( 2, 3) 5.1.4. Specializations of region Using the relations above, we define four specializations of Region (Fig. 4). A Convex Region is a region that is equal to its convex hull (d20). A Concave Region is a region that is not convex (d21). Consequently, Convex Region and Concave Region form a disjoint and complete partition of Region (t14). A Self-Connected Region is a region where any two other regions that sum up to it will be connected to each other (d22). A Disconnected Region is a region that is not self-connected (d23). From these definitions it follows that Self-Connected Region and Disconnected Region form a complete and disjoint partition of Region (t15). (d20) ConvexRegion( 1) d=ef Region( 1) ∧ ∀ 2(hasConvexHull( 1, 2) ↔

isRegionIdenticalWith( 1, 2)) (d21) ConcaveRegion() d=ef Region() ∧ ¬ ConvexRegion() (t14) Region() ↔ ( ConvexRegion() ∨ ConcaveRegion())∧ ¬(ConvexRegion() ∧ ConcaveRegion())

def (d22) SelfConnectedRegion( 1) = ∀ 2, 3(regionsUnion( 1, 2, 3) →

isRegionConnectedTo( 2, 3)) (d23) DisconnectedRegion() d=ef Region() ∧ ¬ SelfConnectedRegion() (t15) Region() ↔ ( SelfConnectedRegion() ∨ DisconnectedRegion())∧

¬(SelfConnectedRegion() ∧ DisconnectedRegion())

5.2. Physical objects and their spatial location

After describing regions in a formalization compatible with UFO, we shift our focus to the spatial location of objects. More precisely, we limit our model to instances of Physical Object10, and consequently restrict our analysis to objects that are three-dimensional. A Physical Object is a substantial that is

UFO: Abstract Individual

Region {disjoint, complete}

{disjoint, complete} /Concave Region /Convex Region /Disconnected

Region /Self-connected

Region spatially extended, that includes both material objects (such as a book and a rock) and also some parasitic substantials [sensu 9] (such as holes and pores).

A Spatial Location is an intrinsic moment of physical objects. It embodies the fact that they are spatially extended entities. Spatial Location is related but distinct from Shape, as an object might retain its shape while having diferent values for its spatial location at diferent times.

Physical Object is a rigid non-sortal type that specializes UFO:Substantial (a19) and instantiates UFO:Category (Fig. 5). Spatial Location is a rigid sortal type that specializes UFO:Quality (a20) and instantiates UFO:Kind (Fig. 5).

The isLocationOf relation holds between a Spatial Location and a Physical Object (a21).

Moreover, a Physical Object bears a unique Spatial Location (a22). The isLocationOf relation

is a specialization of the UFO:inheresIn relation (a23), and consequently, it is non-descriptive and external [sensu 29]. (a19) PhysicalObject() → UFO:Substantial() (a20) SpatialLocation() → UFO:Quality() (a21) isLocationOf(, ) →

SpatialLocation() ∧ PhysicalObject()

(a22) PhysicalObject() → ∃!( SpatialLocation() ∧ isLocationOf(, )) (a23) isLocationOf(, ) →

UFO:inheresIn(, )

The quality Spatial Location is structured by a Spatial Structure whose members are instances of Spatial Region. A Spatial Structure might be a standard adopted to describe space and spatial relations. In this sense, they include all spatial regions on a relative space [sensu 14], which is determined in relation to some conveniently chosen material object. For example, the International Celestial Reference Frame, which has its spatial regions determined relative to the barycenter of the Solar System. There are also terrestrial reference frames which are defined in relation to Earth or some part of it. The choice of the best way to structure space is domain dependent and can vary depending on the requirements.

A Spatial Structure is a specialization of UFO:Quality Structure (a24). Spatial Region is a specialization of UFO:Quale and Region (a25). Every instance of Spatial Region is a member of a single Spatial Structure (a26) The value of a Spatial Location is a Spatial Region (a27). (a24) SpatialStructure() → UFO:QualityStructure() (a25) SpatialRegion() → Region() ∧ UFO:Quale() (a26) SpatialRegion() → ∃!( SpatialStructure() ∧ ∈ ) (a27) SpatialLocation() ∧ UFO:hasValue(, ) →

SpatialRegion()

Using the above formalization, we derive the relation isLocatedInRegion that directly connects a

Physical Object with a Spatial Region that is the value of its Spatial Location (d24). We can also

10Physical object is defined in UFO-C, an ontology focused on social and intentional entities [ 31, 22]. However, it is not included in the formalization of UFO [ 9, 8 ]. The intensional meaning we use is the same as that from the UFO-C ontology. derive spatial relations that hold directly between physical objects, mirroring the taxonomy of relations between regions. These relations are classified as internal and descriptive [ sensu 29], as they compare two objects and the truthmaker is their instances of SpatialLocation. Due to space constraints, we will define here only the isSpatiallyIdenticalTo (d25) and isSpatiallyProperPartOf (d26) relations. The remaining relations follow the same axiomatic pattern and are included in the supplementary materials. (d24) isLocatedInRegion(, ) d=ef PhysicalObject() ∧ SpatialRegion()∧

∃( UFO:isLocationOf(, ) ∧ UFO:hasValue(, )) (d25) isSpatiallyIdenticalTo(, ) d=ef PhysicalObject() ∧ PhysicalObject()∧ ∃ 1, 2(isLocatedInRegion(, 1) ∧ isLocatedInRegion(, 2)∧

isRegionIdenticalWith( 1, 2)) (d26) isSpatiallyProperPartOf(, ) d=ef PhysicalObject()∧

PhysicalObject() ∧ ∃ 1, 2(isLocatedInRegion(, 1)∧

isLocatedInRegion(, 2) ∧ isRegionProperPartOf( 1, 2)) 5.2.1. Further connections with UFO theory In this section, we propose some additional axioms that connect our proposed spatial ontology with UFO. First, Quantities are defined as maximally self-connected portions of matter [ 9, 32, 8 ]. Entities such as portion of water and portion of gold are classified as quantities. In the following, we complement the axiomatization of UFO:Quantity using the spatial location ontology described above. Therefore, every UFO:Quantity is also a Physical Object (a28). And Quantities are located in self-connected regions (a29). (a28) UFO:Quantity() → PhysicalObject() (a29) UFO:Quantity() ∧ isLocatedInRegion(, ) →

SelfConnectedRegion()

Second, there is a relation between the spatial relations of physical objects and their constitution and mereology. As defined in [ 8 ], constitution is restricted to entities of the same ontological category. Moreover, the UFO:constitutedBy relation is irreflexive [8, p.11] and asymmetric [8, p.12]. To the restriction that an endurant could only be constituted by another endurant, we can go one category further and afirm that a PhysicalObject can only constitute and be constituted by another PhysicalObject (a30). If a PhysicalObject is constituted by another PhysicalObject, then they are spatially identical (a31). This axiom follows the definition of material constitution that consti tuent and constituted entities must be co-localized in space [33, 34]. Mereological proper parthood also implies spatial proper parthood between physical objects (a32). As spatial proper parthood is disjoint with spatial identity, we can derive that constitution and mereological proper parthood are disjoint (t16). (a30) UFO:constitutedBy(, ) → ( PhysicalObject() ↔ PhysicalObject()) (a31) PhysicalObject() ∧ UFO:constitutedBy(, ) → isSpatiallyIdenticalTo(, ) (a32) PhysicalObject() ∧ PhysicalObject( ) ∧ UFO:PP(, ) → isSpatiallyProperPartOf(, ) (t16) PhysicalObject() ∧ PhysicalObject( ) → ¬( UFO:constitutedBy(, ) ∧ UFO:PP( , ))

These axioms and theorem above are definitively not comprehensive. There are many more ways in which we could use this spatial ontology to better discuss and define the constitution and mereology of physical entities. For instance, one can use the spatial relations to better frame a discussion about the iflling and hosting relations between holes and objects [ 35], or how to relate the mereology of portions of matter and functional complexes.

6. Final Considerations

In this paper, we propose a reference ontology for the spatial location of physical objects, grounded in the Unified Foundational Ontology (UFO). Our ontology is based on the region-connected calculus (RCC) [ 7 ], proposed in predicate first-order logic and integrated with the formalization of UFO. We also provide implementation of the theory in an interactive theorem prover and in the OntoUML language, which allows further verification under the UFO theory and reusability in other ontologies.

We modeled spatial location as an intrinsic moment of physical objects (CQ1), in an approach that closely resembles the DOLCE ontology [ 2 ]. In this approach, the value of a spatial location is a spatial region (CQ2), which is a member of a spatial structure. Both spatial regions and spatial structures are relative spaces [14, sensu] and abstract entities, following the theory of conceptual spaces [sensu 15] that is also used in UFO for other quality structures [ 9, 28 ].

We adopted a relational view on spatial regions (Section 2). The decision of modeling spatial regions and structures as an abstract conceptual space is justified by two arguments. First, it better fits the way space is used by domains such as geology and geography, which deal within a spatial meso-scale (not included quantic or relativistic scales). In those domains, spatial locations are attributed using coordinate systems in a reference frame, that is defined arbitrarily according to the local necessities (although there are standards for global positioning, for instance), therefore, in relation to some physical object. The second reason is that it fits better with the existing theories of UFO. For instance, UFO avoids using homeomerous concepts as they have undesirable computational properties, such as finite satisfiability (this is one of the arguments in [ 32] against using amounts of matter). We understand that a concrete space would be homeomerous.

To compare the spatial locations of physical objects, we included a set of relations between regions, based on the Region Connection Calculus (RCC) [ 7 ] (CQ3). In our ontology, we placed region as a primitive type of abstract entity, specialized by spatial region. In this manner, it is possible to specialize region and use its relations to make comparisons of qualities with values on other conceptual spaces. Moreover, there is a set of internal descriptive relations to compare two physical objects directly.

Lastly, the spatial relations of physical objects are associated with their mereology and constitution (CQ4). With respect to the mereology of physical objects, proper parthood implies spatial proper parthood. An arm is a component of the body, and it is a proper spatial part of the body. A portion of alcohol is a sub-quantity of a portion of wine, and it is spatially a proper part of the same portion. Regarding material constitution [sensu 33], constituent and constituted are co-located, therefore the constitution relation implies location in identical spatial regions.

In terms of future research, there is much to advance after this work. We implemented the theory in a proof assistant, which allows one to verify theorems included in this work and in the supplementary materials. However, it is still necessary to implement the theory in a model checker to ensure satisfiability and, consequently, consistency. Moreover, a model checker will also aid in checking if the theory is not under- or over-constrained. A validation tactic would be applying the ontology in real-world scenarios to test for non-functional requirements and usability of the ontology.

In the future, we intend to extend this ontology to consider changes in time and events involving changes in object location, as this work assumes a single time slice. The convexity and concavity of regions are also minimally defined in this work and can be enhanced in the future. Lastly, this work is intended as a foundational basis for discussing other ontological questions, such as the relation between material and immaterial objects and the constitution and mereology of physical objects.

Acknowledgments

We thank Adrien Barton and three anonymous reviewers for their comments and corrections. This study is part of L. V. Vieira PhD project, which is supported and funded by Petrobras S.A., Brazil. M. Abel is supported by CAPES Finance Code 001 and CNPq, the Brazilian Finance Council.

Declaration on Generative AI

During the preparation of this work, the author(s) used ChatGPT o4-mini-high and Writefull to: draft content, grammar and spelling check, paraphrase, and reword. ChatGPT o4-mini-high was also used to aid in formalization by content enhancement and theorem proofs. After using these tools, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. [16] S. Borgo, R. Ferrario, A. Gangemi, N. Guarino, C. Masolo, D. Porello, E. M. Sanfilippo, L. Vieu, Dolce: A descriptive ontology for linguistic and cognitive engineering, Applied ontology 17 (2022) 45–69. [17] R. Arp, B. Smith, A. D. Spear, Building ontologies with basic formal ontology, Mit Press, 2015. [18] B. Smith, M. Almeida, J. Bona, M. Brochhausen, W. Ceusters, M. Courtot, R. Dipert, A. Goldfain, P. Grenon, J. Hastings, W. Hogan, et al., Basic formal ontology 2.0 - specification and user’s guide (2015). [19] A. Pease, I. Niles, J. Li, 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, volume 28, 2002, pp. 7–10. [20] L. S. Munoz, M. Gruninger, Mapping and verification of the time ontology in SUMO, in: Formal

Ontology in Information Systems, 2016. [21] A. B. Benevides, J. P. A. Almeida, G. Guizzardi, Towards a unified theory of endurants and perdurants: Ufo-ab, in: Proceedings of the Joint Ontology Workshops 2019. Episode V: The Styrian Autumn of Ontology, volume 2518, CEUR-WS, 2019. [22] G. Guizzardi, R. d. A. Falbo, R. S. S. Guizzardi, Grounding software domain ontologies in the unified foundational ontology (ufo): the case of the ode software process ontology., 2008, pp. 127–140. [23] V. A. Carvalho, J. P. A. Almeida, C. M. Fonseca, G. Guizzardi, Multi-level ontology-based conceptual modeling, Data & Knowledge Engineering 109 (2017) 3–24. [24] G. Guizzardi, V. Zamborlini, Using a trope-based foundational ontology for bridging diferent areas of concern in ontology-driven conceptual modeling, Science of Computer Programming 96 (2014) 417–443. [25] S. Borgo, C. Masolo, Full mereogeometries, The Review of Symbolic Logic 3 (2010) 521–567. [26] N. Asher, L. Vieu, Toward a geometry of common sense: A semantics and a complete axiomatization of mereotopology, in: Proceedings of the 14th international joint conference on Artificial intelligence, volume 1, 1995, pp. 846–852. [27] M. Donnelly, B. Smith, Layers: A new approach to locating objects in space, in: Spatial Information Theory. Foundations of Geographic Information Science, Lecture Notes in Computer Science, 2003, pp. 46–60. [28] A. Albuquerque, G. Guizzardi, An ontological foundation for conceptual modeling datatypes based on semantic reference spaces, IEEE 7th International Conference on Research Challenges in Information Science (RCIS) (2013) 1–12. [29] C. M. Fonseca, D. Porello, G. Guizzardi, J. P. A. Almeida, N. Guarino, Relations in ontology-driven conceptual modeling, in: Conceptual Modeling: 38th International Conference, ER 2019, Salvador, Brazil, November 4–7, 2019, Proceedings 38, Springer, 2019, pp. 28–42. [30] A. Cotnoir, A. C. Varzi, Mereology, Oxford University Press, United Kingdom, 2021. [31] A. C. O. Bringuente, R. Falbo, G. Guizzardi, The role of foundational ontologies for domain ontology engineering: a case study in the software process domain, Journal of Information and Data Management 3 (2011) 511–526. [32] G. Guizzardi, On the representation of quantities and their parts in conceptual modeling., in: 6th

International Conference on Formal Ontology in Information Systems (FOIS), 2010, pp. 103–116. [33] L. R. Baker, Persons and bodies: A constitution view, Cambridge University Press, 2000. [34] L. F. Garcia, J. L. Carbonera, F. H. Rodrigues, C. R. Antunes, M. Abel, What rocks are made of: towards an ontological pattern for material constitution in the geological domain, in: Conceptual Modeling: 38th International Conference, ER 2019, Salvador, Brazil, November 4–7, 2019, Proceedings 38, Springer, 2019, pp. 275–286. [35] A. C. Varzi, Reasoning about space: The hole story (1996).

References

[1] J. Bateman , S. Farrar , Spatial Ontology Baseline, Technical Report , University of Bremen, Germany, 2006 .

[2] C. Masolo , S. Borgo , A. Gangemi , N. Guarino , A . Oltramari, WonderWeb Deliverable D18 , Technical Report , 2003 .

[3] P. Grenon , B. Smith , SNAP and SPAN: Towards dynamic spatial ontology , Spatial Cognition & Computation 4 ( 2004 ) 69 - 104 .

[4] F. Cicconeto , L. V. Vieira , M. Abel , R. dos Santos Alvarenga, J. L. Carbonera , A spatial relation ontology for deep-water depositional system description in geology ., in: ONTOBRAS , 2020 , pp. 35 - 47 .

[5] R. Casati , A. C. Varzi , Spatial entities ( 1997 ).

[6] S. Borgo , N. Guarino , C. Masolo , A pointless theory of space based on strong connection and congruence , in: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning , 1996 , pp. 220 - 229 .

[7] A. G. Cohn , B. Bennett , J. Gooday , N. M. Gotts , Qualitative spatial representation and reasoning with the region connection calculus , Geoinformatica 1 ( 1997 ) 275 - 316 .

[8] G. Guizzardi , A. Botti Benevides , C. M. Fonseca , D. Porello , J. P. A. Almeida , T. Prince Sales , Ufo: Unified foundational ontology, Applied ontology 17 ( 2022 ) 167 - 210 .

[9] G. Guizzardi , Ontological foundations for structural conceptual models , Centre for Telematics and Information Technology , 2005 .

[10] J. P. A. Almeida , C. M. Fonseca , V. A. Carvalho , A comprehensive formal theory for multi-level conceptual modeling , in: Conceptual Modeling: 36th International Conference, ER 2017, Valencia, Spain, November 6- 9 , 2017 , Proceedings 36, Springer, 2017 , pp. 280 - 294 .

[11] L. d. Moura , S. Ullrich, The lean 4 theorem prover and programming language , in: International Conference on Automated Deduction, Lecture Notes in Computer Science , 2021 , pp. 625 - 635 .

[12] J. K. McDonough , Leibniz's Philosophy of Physics , in: E. N. Zalta , U. Nodelman (Eds.), The Stanford Encyclopedia of Philosophy , Fall 2024 ed., Metaphysics Research Lab, Stanford University, 2024 .

[13] R. Casati , B. Smith , A. Varzi , Ontological tools for geographic representation , in: Formal ontology in information systems , Amsterdam: IOS Press, 1998 , pp. 77 - 85 .

[14] M. Donnelly , Relative places, Applied Ontology 1 ( 2005 ) 55 - 75 .

[15] P. Gardenfors , Conceptual Spaces: The Geometry of Thought, The MIT Press, 2000 .