The Mereologies of Upper Ontologies

Abstract

Mereology, the formal theory of parts and wholes, has a played a prominent role within applied ontology. As a fundamental set of concepts for commonsense reasoning, it also appears in a number of upper level ontologies. Furthermore, such upper-level ontologies provide an account of the most basic, domain-independent, existing entities, such as time, space, objects, and processes. In this paper, we verify the core characterization of mereologies of the Suggested Upper Merged Ontology (SUMO), and the mereology of the Descriptive Ontology for Linguistic and Cognitive Engineering (DOLCE), while relating their axiomatizations via ontology mapping. We show that the existing axiomatization of SUMO omits some of the intended models of classical mereology, and we propose the correction and addition of axioms to address this issue. In addition, we show the formal relationship between the axiomatization of mereology in both upper-level ontologies.

1 Introduction

Automatic applications appealing to ontologies for interoperation are unambiguously integrated only when the models of their shared features are equivalent. However, ontologies admitting unintended models ambiguously characterize their vocabularies, which can generate misunderstandings that hinder interoperability.

Upper-level ontologies, also called foundational ontologies, provide an account of the most basic, domain independent, existing entities, such as time, space, objects and processes. As ontologies are crucial for the Semantic Web, upper level ontologies are essential for the ontology engineering cycle in activities such as ontology building and integration. Upper level ontologies can be used as the foundational substratum on which new ontologies are developed, because they provide some fundamental ontological distinctions, which can help the designer in her task of conceptual analysis, [11]. They can be used as a backbone on top of which more specific concepts can be characterized while reusing their root vocabulary and their general knowledge. In ontology integration, they can be used as oracles for meaning clarification [6].

Upper-level ontologies are expected to be mostly consulted for meaning negotiation and not for terminological reasoning, therefore they have to be represented in expressive languages that can convey every feature of the characterized entities. However, less accurate representations in lightweight languages should be available too, which can be extended with domain specific axiomatizations when the use of lightweight languages is necessary.

Since foundational ontologies are expected to be broadly reused and extended, they are not expected to admit unintended models which the expressivity of their representation language can rule out, and it is also expected that they do not miss intended models. If a upper-level ontology does not admit those models which it is expected to admit, misunderstandings among applications who subscribe to their account of the world can occur.

Various upper level ontologies have been developed in languages with higher or equivalent expressivity to first-order logic, such as SUMO [18] and DOLCE [2, 8], and translations of them, with loss, to lightweight language OWL¹, made available. Therefore, semantic mappings connecting their axiomatizations are necessary to facilitate interoperability among applications that commit to the characterizations provided by different upper level ontologies. Those mappings need to be formal, which guarantees their interpretability by automatic agents, and also need to be represented in an expressive language such as standard first-order logic.²

Ontology verification [10] is the process by which a theory is checked to rule out unintended models, and possibly characterize missing intended ones. Therefore, ontology verification reduces semantic ambiguity. Since foundational ontologies are expected to be broadly reused, their verification results necessary.

In this paper³, we verify the subtheory of core mereotopological concepts of the SUMO foundational ontology and the mereology of the DOLCE-CORE, the fragment of DOLCE focused on entities that exist on time. In addition, we formally relate their respective axiomatizations via first-order logic mappings. As a result, we propose the correction, and addition, of some axioms which rule out unintended models or characterize missing ones. As an additional outcome of our work, we have produced a modular representation stated in standard first-order logic of the complete SUMO subtheory of mereotopology. We have used automatic theorem prover Prover9 and model finder Mace4 [15] for the automatic tasks involved in the work described in this paper.

2 Ontology Mapping and Verification

Ontology mapping, also called ontology matching, and ontology alignment, is concerned with the explicit representation of the existing semantic correspondences among the axiomatizations of different ontologies⁴ via bridge axioms [6], which are called translations definitions in the context of first-order logic.

Building a map between two first-order logic ontologies $T_1$ and $T_2$ that interprets the first into the second involves translating every symbol of theory $T_1$ into the language of $T_2$, translating every sentence of $T_1$ into the language of $T_2$, and checking the ability of $T_2$ to entail every axiom of $T_1$. The following definition formalizes the notion of relative interpretation between first-order logic theories.

Definition 1

A map $\pi$ interprets a theory $T_1$ into a theory $T_2$ iff for every sentence $\alpha$ in the language of $T_1$, $T_1\,\models \,\alpha \Rightarrow T_2\,\models \,\alpha ^\pi$; being $\alpha ^\pi$ the syntactic translation of $\alpha$ into the language of $T_2$.

The following theorem that follows fom [5], introduces a fundamental relation between the models of a theory and the models of the theories that it interprets. Given such a relation, in order to demonstrate that a given theory $T_2$ can represent every feature that another theory $T_1$ represents, it suffices to demonstrate that theory $T_2$ is able to interpret theory $T_1$.

Theorem 1

If a theory $T_1$ is interpreted by a theory $T_2$ by means of a given map $\pi$, there is another map $\delta$ that sends every model of $T_2$ into a model of $T_1$.

An ontology admits unintended models when it is possible to find features of its underlying conceptualization which are not characterized by its axiomatization. Ontology Verification in first-order logic [10] is based on the fact that theories with different vocabularies unambiguously characterize the same concepts only if their sets of models are equivalent. Verifying an ontology T ideally consists of classifying the actual models ${\mathfrak M}$ of T by means of a representation theorem,⁵ which relates the models of T with the models ${\mathfrak M}^{intended}$ of an alternative axiomatization of T built with well understood theories. Such a representation theorem must be either proved or disproved. The following definition from [19] relates the notion of ontology mapping with the fundamentals of ontology verification:

Definition 2

Two theories $T_1$ and $T_2$ are synonymous iff there exist two sets of translation definitions $\varDelta$ and $\varPi$, respectively from $T_1$ to $T_2$ and from $T_2$ to $T_1$, such that $T_1 \cup \varPi$ is logically equivalent to $T_2 \cup \varDelta$.

Given Definition 2, from Theorem 1 follows that the models of synonymous theories are equivalent, and therefore ontology mapping can be used for classifying the sets of models of two ontologies as equivalent.

3 SUMO

SUMO [18] is a freely available upper level ontology intended to describe the world as perceived by humans, based on human knowledge and culture, in opposition to ontological realism [9], which is meant to present the world as it is, independently of the bias of human perception. In addition to the main ontology, which contains about 4000 axioms, SUMO has been extended with a mid-level ontology and a number of domain specific ontologies, all of which account for 20,000 terms and 70,000 axioms. SUMO has been translated into OWL and WordNet [17]. The representation language of SUMO is SUO-KIF⁶, a very expressive dialect of KIF⁷ with many-sorted features, whose syntax permits higher-order constructions such as predicates that have other predicates, or formulas, as their arguments, and the existence of predicates and functions of variable arity [1].

Fig. 1.

Modular decomposition of the SUMO axiomatization of concepts related to mereotopology. Theories in the shaded region are discussed in this paper; the remaining subtheories of SUMO are left for future work. Arrows point to conservative extensions among modules. Signature members are shown in the module that first introduces them. (Original figure from [16].)

We have translated (with loss) into standard first-order logic, and modularized, the subset of SUMO that characterizes the notion of mereotopology, which resulted in the hierarchy of subtheories shown in Fig. 1, where each theory conservatively extends⁸ its related theories below. Due to space limitations, we only address in this work the study of modules $T_{part}$, $T_{sum}$, $T_{product}$, $T_{decomposition}$, $T_{topology}$, and $T_{mereotopology}$. The first-order logic axiomatization of all the modules shown in Fig. 1 can be found at colore.oor.net/ontologies/sumo/modules.

SUMO adopts various partial orderings to address the part-whole relationship in different categories. Regarding entities that are in space and time, classified as Physical in SUMO, relations part and subProcess respectively characterize part-whole relations for members of Object and Process, while relation temporalPart represents part-whole for members of TimePosition, which extends to points and intervals of time.

3.1 The Subtheory $T_{part}$

The subtheory $T_{part}$ represents the relation among a whole and its parts by axiomatizing the primitive relation part and using conservative definitions for the overlapsSpatially, overlapsPartially, and properPart relations. Extracting the sentences from SUMO that use the primitive signature $\{ Object, part \}$, we obtain the following subtheory:

Definition 3

$T_{part}$ is the subtheory composed by axioms (1) to (7).

$$\begin{aligned} (\forall x,y) part(x,y)\rightarrow Object(x) \wedge Object(y) \end{aligned}$$

(1)

$$\begin{aligned} (\forall x) Object(x)\rightarrow part(x,x) \end{aligned}$$

(2)

$$\begin{aligned} (\forall x,y) part(x,y) \wedge part(y,x) \rightarrow (x=y) \end{aligned}$$

(3)

$$\begin{aligned} (\forall x,y,z) part(x,y) \wedge part(y,z)\rightarrow part(x,z) \end{aligned}$$

(4)

$$\begin{aligned} (\forall x,y) overlapsSpatially(x,y)\leftrightarrow (\exists z (part(z,x) \wedge part(z,y))) \end{aligned}$$

(5)

$$\begin{aligned} (\forall x,y) overlapsPartially(x,y)\leftrightarrow \lnot part(x,y) \nonumber \\ \wedge \lnot part(y,x) \wedge (\exists z) part(z,x) \wedge part(z,y) \end{aligned}$$

(6)

$$\begin{aligned} (\forall x,y) properPart(x,y)\leftrightarrow part(x,y) \wedge \lnot part(y,x)\end{aligned}$$

(7)

The first question we need to address is whether or not this subtheory is a module of SUMO, or whether there are additional sentences in the signature $\{ Object, part \}$ that are entailed by the remaining axioms of SUMO. Before we can fully answer this question, we need to consider the other subtheories of SUMO that are related to mereology.

3.2 Subtheory $T_{sum}$

The mereological sum of two parts into a whole is represented in the subtheory $T_{sum}$ by the function symbol MereologicalSumFn.

Definition 4

The subtheory $T_{sum}$ is the subtheory that extends $T_{part}$ in the expanded signature $\{ Object,part,MereologicalSumFn \}$ by means of axioms (8) and (9).

$$\begin{aligned} (\forall x,y,z) Object(x) \wedge Object(y) \rightarrow \nonumber \\ ((z=MereologicalSumFn(x,y))\rightarrow (\forall p) (part(p,z)\leftrightarrow (part(p,x) \vee part(p,y))) \end{aligned}$$

(8)

$$\begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalSumFn(x,y)) \end{aligned}$$

(9)

Given two objects, the existence of their mereological sum is guaranteed in this theory due to the use of a function to represent such an operation (since functions in first-order logic are total).

We can immediately find some straightforward consequences⁹ of the axioms of $T_{sum}$:

Proposition 1

$$\begin{aligned} T_{sum}\,\models \,(\forall x,y,z) Object(x) \wedge Object(y){\wedge } \nonumber \\ (z=MereologicalSumFn(x,y))\rightarrow part(z,x) \vee part(z,y) \end{aligned}$$

(10)

$$\begin{aligned} T_{sum}\,\models \,(\forall x,y,z) Object(x) \wedge Object(y){\wedge } \nonumber \\ (z=MereologicalSumFn(x,y))\rightarrow part(x,z) \wedge part(y,z) \end{aligned}$$

(11)

Fig. 2.

With the original characterization of mereological sum, every two objects in every model of SUMO must be in relation part, such as objects x and y in (a). Models corresponding to (b) and (c) with overlapping objects without being one part of the other, or with disjoint objects, are not admitted by SUMO submodule $T_{sum}$. (Original figure from [16].)

Given theorems (10) and (11), and due to the antisymmetry of relation part, it holds that z must be x or y, this fact entails that every pair of objects in the universe of every interpretation of SUMO must be in relation part, which shows that SUMO omits models where there exist objects that are disjoint, or that overlap without being one part of the other, as depicted in parts (b) and (c) of Fig. 2. The following proposition formalizes this claim:

Proposition 2

$T_{sum}\,\models \,(\forall x,y) Object(x) \wedge Object(y) \rightarrow part(x,y) \vee part(y,x)$.

In other words, SUMO entails that the part relation is synonymous with a linear ordering. Although there is much discussion in the philosophical and applied ontology literature [20] over which axioms should constitute a mereology, there is nobody who proposes that all models of an axiomatization of mereology be synonymous with linear orderings. In order to allow those omitted models that Proposition 2 identifies, we propose a modification of $T_{sum}$:

Definition 5

$T_{extended\_sum}$ is the theory which extends $T_{part}$ with the sentences

$$\begin{aligned} (\forall x,y,z) Object(x) \wedge Object(y) \rightarrow \nonumber \\ ((z=MereologicalSumFn(x,y)\rightarrow (\forall p) (part(z,p)\leftrightarrow part(x,p) \wedge part(y,p))) \end{aligned}$$

(12)

$$\begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalSumFn(x,y)) \end{aligned}$$

(13)

The following proposition shows that $T_{extended\_sum}$ does not rule out models in which overlapping or disjoint objects exist.

Proposition 3

If we look more closely at the proposed axiomatization, we can see that the MereologicalSumFn function is commutative and idempotent:

Proposition 4

$$\begin{aligned} T_{extended\_sum}\,\models \,(\forall x,y,z)Object(x) \wedge Object(y) \wedge Object(z) \wedge \end{aligned}$$

$$\begin{aligned} (MereologicalSumFn(x,y)=z)\rightarrow (MereologicalSumFn(y,x)=z) \end{aligned}$$

$$\begin{aligned} T_{extended\_sum}\,\models \,(\forall x,y,z) part(x,y) \rightarrow (MereologicalSumFn(x,y)=y) \end{aligned}$$

This leads us to consider how $T_{extended\_sum}$ is related to lattice theory [4].

Theorem 2

$T_{extended\_sum}$ is synonymous with $T_{join\_semilattice}$¹⁰.

Proof

Let $\varDelta$ be the sentence

$$\begin{aligned} (\forall x,y,z) \, (MereologicalSumFn(y,x)=z) \leftrightarrow (join(x,y)=z) \end{aligned}$$

Using Prover9, we can show that $T_{extended\_sum} \cup \varDelta \,\models \,T_{join\_semilattice}$, and $T_{join\_semilattice} \cup \varDelta \,\models \,T_{extended\_sum}$    $\square$

We can also specify an extension of $T_{part}$ in the same signature.

Definition 6

$T_{part\_sum}$ is the extension of $T_{part}$ with the sentence

$$ (\forall x,y)(\exists j) \, (part(x,j) \wedge part(y,j) \wedge ((\forall z) \, (part(x,z) \wedge part(y,z) \supset part(j,z)))) $$

Theorem 3

$T_{part\_sum}$ is synonymous with $T_{strong\_lub\_mereology}$¹¹

Proof

To disambiguate the signatures of SUMO and other existing mereologies, let $part^sumo(x,y)$ be the relation in the signature of SUMO.

Let $\varDelta$ be the sentence

$$\begin{aligned} (\forall x,y) \, part^{sumo}(x,y) \leftrightarrow part(x,y)) \end{aligned}$$

Using Prover9, we can show that $T_{part\_sum}\,\models \,T_{strong\_lub\_mereology}$, and $T_{strong\_lub\_mereology}\,\models \,T_{part\_sum}$    $\square$

It should be noted that the axiomatization of $T_{strong\_lub\_mereology}$ corresponds to the sentence SA13 in [20].

Proposition 5

$$\begin{aligned} SUMO\,\models \,T_{part\_sum} \end{aligned}$$

3.3 Subtheory $T_{product}$

Given two objects, their mereological product intuitively corresponds to their intersection. SUMO represents the notion of mereological product by means of the function MereologicalProductFn.

Definition 7

$T_{product}$ is the subtheory of SUMO that extends theory $T_{part}$ in the expanded signature $\{ Object,part, MereologicalProductFn \}$ by the sentences:

$$\begin{aligned} (\forall x,y,z) Object(x) \wedge Object(y) \rightarrow \nonumber \\ ((z=MereologicalProductFn(x,y)) \rightarrow (\forall p) (part(p,z)\leftrightarrow part(p,x) \wedge part(p,y))) \end{aligned}$$

(14)

$$\begin{aligned} \begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalProductFn(x,y)) \end{aligned}\end{aligned}$$

(15)

Given two objects, the existence of their mereological product is guaranteed due to the use of a function to represent such an operation.

The characterization of mereological product in SUMO corresponds to the infimum or meet of the corresponding arguments on the lattice that relation part defines. We have found that from the characterization of mereological product of SUMO follows that every pair of objects must overlap, which indicates that SUMO omits those models where there exist objects that do not overlap (in other words, all elements overlap each other in all models of SUMO):

Proposition 6

$T_{product}\,\models \,(\forall x,y) Object(x) \wedge Object(y)\rightarrow (overlapsSpatially(x,y))$.

In order to allow models in which nonoverlapping elements exist, we propose a modification of SUMO:

Definition 8

$T_{extended\_product}$ is the theory which extends $T_{part}$ by the sentences

$$\begin{aligned} (\forall x,y,z) overlapsSpatially(x,y)\rightarrow \nonumber \\ ((z=MereologicalProductFn(x,y)) \rightarrow (\forall p) (part(p,z)\leftrightarrow part(p,x) \wedge part(p,y)))\end{aligned}$$

(16)

$$\begin{aligned} \begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalProductFn(x,y)) \end{aligned}\end{aligned}$$

(17)

The following propositions show that $T_{extended\_product}$ does not rule out models in which there exist nonoverlapping objects, and that MereologicalProductFn is commutative and idempotent.

Proposition 7

Proposition 8

$$\begin{aligned} T_{extended\_product}\,\models \,(\forall x,y,z)Object(x) \wedge Object(y) \wedge Object(z) \wedge \end{aligned}$$

$$\begin{aligned} (MereologicalProdFn(x,y)=z)\rightarrow (MereologicalProdFn(y,x)=z) \end{aligned}$$

$$\begin{aligned} T_{extended\_product}\,\models \,(\forall x,y,z) part(x,y) \rightarrow (MereologicalProdFn(x,y)=x) \end{aligned}$$

We can also specify an extension of $T_{part}$ in the same signature.

Definition 9

$T_{part\_prod}$ is the extension of $T_{part}$ with the sentence

$$ (\forall x,y)\, overlapsSpatially(x,y) \supset (\exists z) \, ((\forall u) \, (part(u,z) \leftrightarrow (part(u,x) \wedge part(u,y)))) $$

Calling $part^{sumo}$ to the relation part of $T_{part}$, the following property holds:

Theorem 4

$T_{part\_prod}$ is synonymous with $T_{prod\_mereology}$¹².

Proof

Let $\varDelta$ be the sentence

$$\begin{aligned} (\forall x,y) \, part^{sumo}(x,y) \leftrightarrow part(x,y)) \end{aligned}$$

Using Prover9, we can show that $T_{part\_prod}\,\models \,T_{prod\_mereology}$,

and $T_{prod\_mereology}\,\models \,T_{part\_prod}$    $\square$

3.4 Subtheory $T_{decomposition}$

The remainder between a whole and its proper parts is represented by the function MereologicalDifferenceFn.

Definition 10

$T_{decomposition}$ is the subtheory of SUMO that extends $T_{part}$ by the sentences

$$\begin{aligned} (\forall x,y,z) Object(x) \wedge Object(y) \rightarrow ((z=MereologicalDifferenceFn(x,y))\rightarrow \nonumber \\ (\forall p) properPart(p,z)\leftrightarrow properPart(p,x) \wedge \lnot properPart(p,y))\end{aligned}$$

(18)

$$\begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalDifferenceFn(x,y)) \end{aligned}$$

(19)

Because the mereological difference, or remainder, between a whole and one of its parts is represented in SUMO by a function, its existence is guaranteed in every case at the expenses of having arbitrary values of the function MereologicalDifferenceFn.

We have found that the axiomatization of MereologicalDifferenceFn given by (18) and (19) entails an unusual result in which the remainder overlaps with the subtrahend:

Proposition 9

$$\begin{aligned} T_{decomposition} \models (\forall x,y,z) Object(x) \wedge Object(y) \end{aligned}$$

$$\wedge (z=MereologicalDifferenceFn(x,y)) \wedge properPart(y,x) \rightarrow properPart(y,z)) $$

In order to eliminate such a class of unintended models, we propose the following modification, and prove by means of Proposition 10 that the new theory does not admit these models.

Definition 11

$T_{extended\_decomp}$ is the theory that extends $T_{part}$ with the following sentences

$$\begin{aligned} (\forall x,y,z) Object(x) \wedge Object(y)\rightarrow ((MereologicalDifferenceFn(x,y)=z)\rightarrow \nonumber \\ (\forall p)(part(p,z)\leftrightarrow part(p,x)\wedge \lnot overlapsSpatially(p,y)))\end{aligned}$$

(20)

$$\begin{aligned} (\forall x,y)Object(x) \wedge Object(y) \rightarrow Object(MereologicalDifferenceFn(x,y)) \end{aligned}$$

(21)

Proposition 10

$$\begin{aligned} T_{extended\_decomp} \not \models \,(\forall x,y,z) Object(x) \wedge Object(y) \end{aligned}$$

$$\begin{aligned} \wedge (z=MereologicalDifferenceFn(x,y)) \wedge properPart(y,x) \rightarrow properPart(y,z)) \end{aligned}$$

We can also specify an extension of $T_{part}$ in the same signature.

Definition 12

$T_{part\_decomp}$ is the extension of $T_{part}$ with the sentence

$$ (\forall x,w)\, \lnot part(w,x) \supset (\exists z) \, ((\forall y) \, (part(y,z) \leftrightarrow \lnot overlapsSpatially(y,x))) $$

Theorem 5

$T_{part\_decomp}$ is synonymous with $T_{comp\_mereology}$¹³.

Proof

Let $\varDelta$ be the sentence

$$\begin{aligned} (\forall x,y) \, part^{sumo}(x,y) \leftrightarrow part(x,y)) \end{aligned}$$

Using Prover9, we can show that $T_{part\_decomp}\,\models \,T_{comp\_mereology}$, and $T_{comp\_mereology}\,\models \,T_{part\_decomp}$    $\square$

3.5 Relationship to Classical Mereologies

We have so far evaluated four subtheories of SUMO and proposed revisions to their axiomatizations to address the problem of classes of omitted and unintended models regarding those normally associated with mereology. We now take a closer look at these revised theories.

Proposition 11

The theory

$$\begin{aligned} T_{part} \cup T_{extended\_sum} \cup T_{extended\_product} \cup T_{extended\_decomp} \end{aligned}$$

is consistent.

Given that the revised theories are consistent, can we characterize their models? In particular, how is the mereology within SUMO related to the classical mereologies that have been explored by the philosophical and applied ontology communities? Regarding the supplementation principles (22) to (25), respectively named in [21] as weak company, strong company, supplementation, and strong supplementation, Proposition 12 shows that those principles are not theorems of SUMO.

Proposition 12

The following sentences are not entailed by

$T_{part} \cup T_{extended\_sum} \cup T_{extended\_product} \cup T_{extended\_decomp}$:

$$\begin{aligned} (\forall x,y)properPart(x,y)\rightarrow \exists z(properPart(z,y) \wedge -(z=x)) \end{aligned}$$

(22)

$$\begin{aligned} (\forall x,y)properPart(x,y)\rightarrow (\exists z)(properPart(z,y) \wedge \lnot part(z,x)) \end{aligned}$$

(23)

$$\begin{aligned} (\forall x,y)properPart(x,y)\rightarrow (\exists z)(Part(z,y) \wedge \lnot overlapsSpatially(z,x)) \end{aligned}$$

(24)

$$\begin{aligned} (\forall x,y)\lnot part(y,x)\rightarrow (\exists z)(Part(z,y) \wedge \lnot overlapsSpatially(z,x)) \end{aligned}$$

(25)

This is closely related to the question of whether or not $T_{part}$ is a module of SUMO. We have already seen that the subtheories of SUMO entail additional mereological theories that are not entailed by $T_{part}$ alone. However, we can see that the addition of these new sentences does form a module of the revised axioms by combining the earlier theorems:

Theorem 6

$T_{part\_sum} \cup T_{part\_prod} \cup T_{part\_decomp}$ is a module of

$T_{part} \cup T_{extended\_sum} \cup T_{extended\_product} \cup T_{extended\_decomp}$ that is synonymous with $T_{strong\_lub\_mereology} \cup T_{prod\_mereology} \cup T_{comp\_mereology}$

3.6 Mereotopology in SUMO

Since mereology can only represent the relation of parts with their respective wholes, predicate connected is characterized in SUMO to represent a more general symmetric and reflexive spatial relationship among objects which are not necessarily in a part-whole relation.

Definition 13

$T_{topology}$ is the subtheory of SUMO consisting of the following axioms:

$$\begin{aligned} (\forall x) Object(x) \rightarrow connected(x,x)\end{aligned}$$

(26)

$$\begin{aligned} (\forall x,y) connected(x,y)\rightarrow Object(x) \wedge Object(y)\end{aligned}$$

(27)

$$\begin{aligned} (\forall x,y) connected(x,y)\rightarrow connected(y,x)\end{aligned}$$

(28)

The subtheory of SUMO that axiomatizes mereotopology, which we have called $T_{spatial\_relation}$ is intended to characterize the relationship between the notions of mereology and topology. In it, both predicates, meetsSpatially, which represents external connection among objects, and overlapsSpatially, are declared disjoint specializations of predicate connected.

Definition 14

$T_{spatial\_relation}$ is the subtheory of SUMO which is an extension of $T_{part} \cup T_{topology}$ consisting of the sentences

$$\begin{aligned} (\forall x,y) \, meetsSpatially(x,y) \rightarrow connected(x,y) \end{aligned}$$

(29)

$$\begin{aligned} (\forall x) \, \lnot meetsSpatially(x,x) \end{aligned}$$

(30)

$$\begin{aligned} (\forall x,y) \, meetsSpatially(x,y) \rightarrow meetsSpatially(y,x) \end{aligned}$$

(31)

$$\begin{aligned} (\forall x,y) \, overlapsSpatially(x,y) \rightarrow connected(x,y) \end{aligned}$$

(32)

$$\begin{aligned} (\forall x) \, overlapsSpatially(x,x) \end{aligned}$$

(33)

$$\begin{aligned} (\forall x,y) \, overlapsSpatially(x,y) \rightarrow overlapsSpatially(y,x) \end{aligned}$$

(34)

$$\begin{aligned} (\forall x,y) \, meetsSpatially(x,y) \rightarrow \lnot overlapsSpatially(x,y) \end{aligned}$$

(35)

$$\begin{aligned} (\forall x,y) \, connected(x,y) \rightarrow (meetsSpatially(x,y) \vee overlapsSpatially(x,y)) \end{aligned}$$

(36)

However, the axiomatization of this theory is already entailed by the following definitional extension of $T_{part} \cup T_{topology}$:

Definition 15

$T_{mereotop\_def}$ is the definitional extension of $T_{part} \cup T_{topology}$ consisting of the sentences

$$\begin{aligned} (\forall x,y) overlapsSpatially(x,y) \leftrightarrow connected(x,y) \wedge (\exists z) \, part(z,x) \wedge part(z,y)\end{aligned}$$

(37)

$$\begin{aligned} (\forall x,y) meetsSpatially(x,y)\leftrightarrow connected(x,y) \wedge \lnot (\exists z) \, part(z,x) \wedge part(z,y) \end{aligned}$$

(38)

Proposition 13

$$\begin{aligned} T_{mereotop\_def}\,\models \,T_{spatial\_relation} \end{aligned}$$

We have found that the monotony of relation connected with respect to parthood was not characterized in SUMO, which introduces unintended models as the one represented in Fig. 3, where all parts share one point, but only shaded ones result to be connected.

Fig. 3.

Model of SUMO where the monotony of relation connected with respect to parthood was not characterized. Even though connected(z, x), part(x, y), $part(y,u), {\text {and}} part(u,v)$ hold, connected(z, y) and connected(z, v) do not hold, while connected(z, u) does hold. (Original figure from [16].)

Proposition 14

In order to rule out those unintended models that proposition 14 identifies, we propose the following extension:

Definition 16

$T_{extend\_mereotop}$ is the theory which extends $T_{part}\,\cup \,T_{topology}$ with sentence (39).

$$\begin{aligned} (\forall x, y) part(x,y)\rightarrow \forall z (connected(z,x) \rightarrow connected(z,y)) \end{aligned}$$

(39)

4 DOLCE

The Descriptive Ontology for Linguistic and Cognitive Engineering DOLCE [8, 14] is a freely available upper ontology that is part of the WonderWeb project¹⁴, which is aimed to provide the infrastructure required for a large-scale deployment of ontologies intended to be the foundation for the Semantic Web. DOLCE has a cognitive approach, i.e., it presents the world as it is grasped by humans, based on human knowledge and culture, in opposition to ontological realism [9], which intends to present the world as it is, independently of the bias of human perception. The development of DOLCE has followed the principles of the OntoClean methodology [12]. The first version of DOLCE had a representation in Modal Logic, a translation with loss into standard first-order logic, a translation with further loss into OWL, and also an alignment with WordNet [7]. A new version of the fragment of the original ontology that focuses on entities that exist on time, called temporal particulars, was presented in [2], called DOLCE-CORE; we will circumscribe our work to the axiomatization of DOLCE-CORE.

At the top of DOLCE-CORE the category of temporal-particulars PT is partitioned into six basic categories: objects O, events E, individual qualities Q, regions R, concepts C, and arbitrary sums AS. Categories $ED \ (endurant)$ and $PD \ (perdurant)$ of DOLCE were, respectively, renamed $O \ (object)$ and $E \ (event)$ in DOLCE-CORE. The axiomatization of mereology in DOLCE-CORE is as follows,¹⁵ where predicate P represents parthood, and (40)–(42) respectively stand for the reflexivity, transitivity, and antisymmetry of relation P. Overlap of parts and mereological sum representing binary fusion of parts are respectively defined in (43) and (44), while (46)–(50) characterize the dissectivity of P across categories, and (51)–(56) close the sum of parts inside each category.

$$\begin{aligned} (\forall x)P(x,x)\end{aligned}$$

(40)

$$\begin{aligned} (\forall x,y)P(x,y) \wedge P(y,z) \rightarrow P(x,z)\end{aligned}$$

(41)

$$\begin{aligned} (\forall x,y)P(x,y) \wedge P(y,x) \rightarrow (x=y)\end{aligned}$$

(42)

$$\begin{aligned} (\forall x,y) Ov(x,y)\equiv (\exists z)(P(z,x) \wedge P(z,y)) \end{aligned}$$

(43)

$$\begin{aligned} (\forall x,y,z) SUM(z,x,y)\equiv (\forall v)Ov(v,z) \leftrightarrow Ov(v,x) \vee Ov(v,y)\end{aligned}$$

(44)

$$\begin{aligned} (\forall x,y)\lnot P(x,y) \rightarrow (\exists z)P(z,x) \wedge \lnot Ov(z,y)\end{aligned}$$

(45)

$$\begin{aligned} (\forall x,y) O(y)\wedge P(x,y)\rightarrow O(x) \end{aligned}$$

(46)

$$\begin{aligned} (\forall x,y) E(y)\wedge P(x,y)\rightarrow E(x) \end{aligned}$$

(47)

$$\begin{aligned} (\forall x,y) T(y)\wedge P(x,y)\rightarrow T(x) \end{aligned}$$

(48)

$$\begin{aligned} (\forall x,y) TQ(y)\wedge P(x,y)\rightarrow TQ(x) \end{aligned}$$

(49)

$$\begin{aligned} (\forall x,y) C(y)\wedge P(x,y)\rightarrow C(x) \end{aligned}$$

(50)

$$\begin{aligned} (\forall x,y,z) O(x) \wedge O(y) \wedge SUM(z,x,y) \rightarrow O(z) \end{aligned}$$

(51)

$$\begin{aligned} (\forall x,y,z) E(x) \wedge E(y) \wedge SUM(z,x,y) \rightarrow E(z) \end{aligned}$$

(52)

$$\begin{aligned} (\forall x,y,z) T(x) \wedge T(y) \wedge SUM(z,x,y) \rightarrow T(z) \end{aligned}$$

(53)

$$\begin{aligned} (\forall x,y,z) TQ(x) \wedge TQ(y) \wedge SUM(z,x,y) \rightarrow TQ(z) \ \ \ \ \end{aligned}$$

(54)

$$\begin{aligned} (\forall x,y,z) C(x) \wedge C(y) \wedge SUM(z,x,y) \rightarrow C(z) \end{aligned}$$

(55)

$$\begin{aligned} (\forall x,y,z) AS(x) \wedge AS(y) \wedge SUM(z,x,y) \rightarrow AS(z) \end{aligned}$$

(56)

Due to the ontological commitment represented by axiom (45), the mereology characterized in DOLCE-CORE is an extensional mereology¹⁶ according to [3, 21].

5 Mapping the Mereologies of SUMO and DOLCE

In order to relate SUMO and DOLCE we assume that the changes that we have proposed in Sect. 3 for eliminating unintended models and characterizing missing intended ones have been performed in SUMO. There is no axiomatization in DOLCE-CORE, neither in DOLCE, that corresponds to the notion of topology, therefore our mappings are circumscribed to the axiomatization of mereology in both theories.

By examining the predicates that characterize the participation of objects in events in both ontologies, and also by the type of relation that the main categories of SUMO and DOLCE-CORE have with time and space, we have built the translation definitions of Table 1 for the main these categories.

Table 1. Mapping of SUMO and DOLCE main categories.

Table 2. Translation definitions for $T_{dolce\_part\_t}$ into $T_{time\_mereology}$.

Table 3. Translation definitions for $T_{time_mereology}$ into $T_{dolce\_part\_t}$.

5.1 Mapping Time

The subtheory $T_{sumo\_time}$, whose modular structure is shown in Fig. 5, characterizes the axiomatization of time in SUMO. This theory, which was verified in [20], includes 3 submodules¹⁷ $T_{sumo\_ordered\_timepoints}$, $T_{sumo\_timeintervals}$, and $T_{time\_mereology}$, such that each module is a conservative extension of each connected subtheory below it in Fig. 5. These 3 subtheories respectively characterize a linear ordering between instants of time, a part-whole relation among intervals of time, and an account of Allen’s interval relations starts, finishes, during, earlier, and meetsTemporally [13]. Finally, $T_{sumo\_time}$ characterizes a part-whole relationship that includes intervals and instants of time.

On the other hand, $T_{dolce\_part}$ characterizes parthood by unique predicate P across every category, including T. By means of the following theorems we can characterize the relationship that exists among $T_{dolce\_part\_t}$ and $T_{sumo\_time}$.

Theorem 7

Let $T_{dolce\_part\_t}$ be the subtheory of $T_{dolce\_part}$ with signature $\{ T, part \}$, and Let $T_{time\_mereology}$ be the theory given by axioms (67)–(72). Then, $T_{time\_mereology}$ is synonymous with $T_{dolce\_part\_T}$.

$$\begin{aligned} (\forall x) TimeInterval(x) \rightarrow temporalPart(x,x). \end{aligned}$$

(67)

$$\begin{aligned} (\forall x,y) temporalPart(x,y) \wedge temporalPart(y,x) \rightarrow (x=y). \end{aligned}$$

(68)

$$\begin{aligned} (\forall x,y,z) temporalPart(x,y) \wedge temporalPart(y,z)\rightarrow temporalPart(x,z). \end{aligned}$$

(69)

$$\begin{aligned} (\forall x,y) overlapsTemporally(x,y)\rightarrow TimeInterval(x) \wedge TimeInterval(y)\end{aligned}$$

(70)

$$\begin{aligned} (\forall x) TimeInterval(x)\rightarrow overlapsTemporally(x,x)). \end{aligned}$$

(71)

$$\begin{aligned} (\forall x,y) TimeInterval(x) \wedge TimeInterval(y) \rightarrow (overlapsTemporally(x,y){\leftrightarrow } \nonumber \\ ((\exists z) (TimeInterval(z) \wedge temporalPart(z,x) \wedge temporalPart(z,y))))\qquad \end{aligned}$$

(72)

Proof

Let $\varDelta$ be the set of translations shown in Table 2, and $\varUpsilon$ the set of translations shown in Table 3. Using Prover9 we have shown that $T_{time\_mereology} \cup \varDelta \,\models \,T_{dolce\_part\_T}$, and $T_{dolce\_part\_T} \cup \varUpsilon \models$ $T_{time\_mereology}$.    $\square$

5.2 Mapping Events

Regarding the representation of events in SUMO and DOLCE, by means of the following definition and theorem we classify the relationship that their respective part-whole axiomatizations have as synonymy.

Table 4. Translation definitions for $T_{dolce\_part\_E}$ into $T_{sumo\_subprocess}$.

Table 5. Translation definitions for $T_{sumo\_subprocess}$ into $T_{dolce\_part\_E}$.

Definition 17

$T_{sumo\_subprocess}$ is the theory given by the axioms:

$$\begin{aligned} (\forall x,y)subProcess(x,y)\rightarrow Process(x) \wedge Process(y) \end{aligned}$$

(78)

$$\begin{aligned} (\forall x)Process(x)\rightarrow subProcess(x,x)\end{aligned}$$

(79)

$$\begin{aligned} (\forall x,y)subProcess(x,y) \wedge subProcess(y,z) \rightarrow subProcess(x,z) \end{aligned}$$

(80)

$$\begin{aligned} (\forall x,y)subProcess(x,y) \wedge subProcess(y,x) \rightarrow (x=y)\end{aligned}$$

(81)

Table 6. Translations DOLCE PART-O into SUMO PART.

Table 7. Translations SUMO PART into DOLCE PART-O.

Theorem 8

Let $T_{dolce\_part\_E}$ be the theory given by axioms (40)–(42) and (47). $T_{sumo\_subprocess}$ is synonymous with $T_{dolce\_part\_E}$.

Proof

Let $\varDelta$ be the set of translations shown in Table 4 and $\varGamma$ the set of translations shown in Table 5. Using Prover9 we have demonstrated that $T_{sumo\_subprocess} \cup \varDelta \,\models \,T_{dolce\_part\_E}$ and $T_{dolce\_part\_E} \cup \varGamma \,\models \,T_{sumo\_subprocess}$.    $\square$

5.3 Mapping Objects

Regarding the representation of objects in SUMO and DOLCE-CORE, by means of the following theorem we classify the relationship among their respective part-whole axiomatizations as synonymy.

Definition 18

SUMO PART is the theory given by axioms (1)–(7), and DOLCE PART-T is the theory given by axioms (40)–(43) and (46).

Theorem 9

Let $T_{sumo\_part}$ be the theory given by axioms (1)–(7), and $T_{dolce\_part\_O}$ the theory given by axioms (40)–(43) and (46). Then, $T_{sumo\_part}$ is synonymous with $T_{dolce\_part\_O}$.

Proof

Let us call $\varDelta$ to the set of translations shown in Table 6, and $\varPi$ the set of translations shown in Table 7. Using Prover9 we have shown that $T_{sumo\_part} \cup \varDelta \,\models \,T_{dolce\_part\_O}$ and $T_{dolce\_part\_O} \cup \varPi \,\models \,T_{sumo\_part}$.    $\square$

5.4 Mapping Mereologies with Sums

The theories $T_{dolce\_sum}$ in DOLCE and $T_{extended\_sum}$ for SUMO are both intended to axiomatize the intuitions regarding the fusion of parts. The key question is now whether or not they actually axiomatize the same class of intended models.

Fig. 4.

Objects x, y, z, t, which do not hold SUM(z, x, y) but hold $MereologicalSumFn(x,y)=z$. Arrows represent relation part of theory $T_{extended\_sum}$, and relation P of theory $T_{dolce\_sum}$. (Original figure from [16]).

Table 8. Translations DOLCE SUM into SUMO SUM.

The axiomatization of $T_{extended\_sum}$ from SUMO is weaker than the axiomatization of $T_{dolce\_sum}$ in DOLCE. In fact, let us consider objects x, y, z, t of Fig. 4, such that properPart(x, z), properPart(y, z), and properPart(t, z) hold, while none of overlapsSpatially(x, y), overlapsSpatially(t, y), or overlapsSpatially(x, t) hold. In parts (a), (b), and (c) of the bottom of Fig. 4 parthood is indicated with arrows from the part to the whole. According to the characterization of mereological sum in $T_{extended\_sum}$, we must have $(MereologicalSumFn(x,y)=z)$. However, parts (b) and (c) of Fig. 4 depict alternative additional conditions that the characterization of mereological sum in $T_{dolce\_sum}$ must satisfy. In DOLCE, any other object t which overlaps with the sum z must also overlap with at least one of the addends x or y, which is a condition indicated by dotted lines. Because neither overlapsSpatially(x, t) nor overlapsSpatially(y, t) hold, then SUM(z, x, y) does not hold in DOLCE. The following theorem formalizes our claim.

Theorem 10

$T_{extended\_sum}$ cannot interpret $T_{dolce\_sum}$.

Proof

Let us call $\varDelta$ to the translations shown in Table 6, and $\varPi$ to the translation shown in Table 8, and let $T_1$ be the theory that results from adding sentence (89) to theory $T_{extended\_sum}$. Using Mace4, we have built a model of $T_1 \cup \varDelta \cup \varPi$ (see footnote 17).

$$\begin{aligned} (\exists x,y,z) SUM(z,x,y) \wedge \lnot (\forall w) (Ov(w,z)\leftrightarrow Ov(w,x) \vee Ov(w,y)) \end{aligned}$$

(89)

   $\square$

In order to translate the symbol MereologicalSumFn of theory $T_{extended\_sum}$ into the language of DOLCE-CORE, we have represented the graph¹⁸ of function MereologicalSumFn by means of predicate MSum, as shown in Table 9.

Theorem 11

$T_{dolce\_sum}$ cannot interpret $T_{extended\_sum}$.

Proof

Let us call $\varDelta$ to the translations shown in Table 1, $\varPi$ to the translations in Table 7, and $\varUpsilon$ to the translation in Table 10, and let $T_1$ be the theory that results from adding sentence (90) to $T_{dolce\_sum}$. Using Mace4, we have built a model of $T_1 \cup \varDelta \cup \varPi \cup \varUpsilon$ (see footnote 18).

$$\begin{aligned} (\exists x,y) Object(x) \wedge Object(y) \wedge (\forall z)(\lnot Object(z) \vee \lnot MSum(z,x,y))\end{aligned}$$

(90)

   $\square$

Fig. 5.

Mappings between modules of DOLCE-CORE and SUMO (extracted from [16]). Black thin arrows point to conservative extensions, thick grey arrows are directed from interpreted theories to interpreting theories, and thick black arrows connect synonymous theories.

Table 9. Characterization of predicate MSum in SUMO.

Table 10. Translation of $T_{extended\_sum}$ into $T_{dolce\_sum}$.

Figure 5 shows conservative extensions by means of thin black arrows and relative interpretations (mappings), by thick grey arrows from interpreted to interpreting theories. Because every theorem of a theory is also a theorem of its conservative extensions, each conservative extension is capable of interpreting every theory that the modules that it extends interpret. In particular, the subtheory $T_{dolce\_part}$, shown in Fig. 5, is the theory resulting from the union of $T_{dolce\_part\_T}$, $T_{dolce\_part\_E}$, and $T_{dolce\_part_O}$, plus axioms (49), (50), while the subtheory DOLCE EXTENSIONAL MEREOLOGY is the union of $T_{dolce\_part}$, $T_{dolce\_sum}$, and axioms (45), (52), (53), (54), (55), and (56). As indicated by oriented grey arrows, the axiomatization of part-whole relations in categories Object, Process, and TimeInterval of SUMO are mappable to DOLCE minimal axiomatization of mereology represented by the subtheory $T_{dolce\_part}$. Although not represented in Fig. 5, it holds that because DOLCE EXTENSIONAL MEREOLOGY extends $T_{dolce\_part}$, it also interprets $T_{sumo\_part}$, $T_{sumo\_subprocess}$, and $T_{time\_mereology}$. In turn, $T_{sumo\_sum}$ interprets $T_{dolce\_part\_O}$. The strongest subtheories of SUMO and DOLCE-CORE that are synonymous, and therefore have equivalent models, are the pairs indicated by double black arrows, i.e, $T_{dolce\_part\_O}$ with $T_{sumo\_part}$, $T_{dolce\_part\_E}$ with $T_{sumo\_subprocess}$, and $T_{dolce\_part\_T}$ with $T_{time\_mereology}$.

6 Conclusions

Since the conceptual coverage of upper ontologies needs to be broad enough to cover the underpinnings of domain ontologies, we find a modules of upper ontologies for notions about time, space, objects, and processes. In this paper, we have focussed on how two upper ontologies (SUMO and DOLCE) axiomatize mereotopologies, that is, the notions of parthood (mereology) and connection (topology). By showing how different subtheories of SUMO and DOLCE are logically synonymous with different theories of lattices, we have identified unintended and omitted models of the original axiomatization of SUMO. There are additional subtheories of SUMO that capture additional spatial concepts such as containment, holes, orientation, and betweenness. Future work will provide a verification of these modules, thereby provided a firmer foundation for spatial reasoning.