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.
Access provided by Autonomous University of Puebla. Download conference paper PDF
Similar content being viewed by others
Keywords
- DOLCE
- DOLCE-CORE
- SUMO
- Ontology mapping
- Ontology verification
- Upper-level ontology
- Mereology
- Topology
- Mereotopology
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 OWLFootnote 1, 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.Footnote 2
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 paperFootnote 3, 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 ontologiesFootnote 4 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,Footnote 5 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-KIFFootnote 6, a very expressive dialect of KIFFootnote 7 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].
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 extendsFootnote 8 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).
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).
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 consequencesFootnote 9 of the axioms of \(T_{sum}\):
Proposition 1
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
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
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}\)Footnote 10.
Proof
Let \(\varDelta \) be the sentence
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
Theorem 3
\(T_{part\_sum}\) is synonymous with \(T_{strong\_lub\_mereology}\)Footnote 11
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
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
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:
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
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
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
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}\)Footnote 12.
Proof
Let \(\varDelta \) be the sentence
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
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
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
Proposition 10
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
Theorem 5
\(T_{part\_decomp}\) is synonymous with \(T_{comp\_mereology}\)Footnote 13.
Proof
Let \(\varDelta \) be the sentence
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
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}\):
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:
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
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
Proposition 13
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.
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).
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 projectFootnote 14, 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,Footnote 15 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.
Due to the ontological commitment represented by axiom (45), the mereology characterized in DOLCE-CORE is an extensional mereologyFootnote 16 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.
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 submodulesFootnote 17 \(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}\).
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.
Definition 17
\(T_{sumo\_subprocess}\) is the theory given by the axioms:
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.
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).
\(\square \)
In order to translate the symbol MereologicalSumFn of theory \(T_{extended\_sum}\) into the language of DOLCE-CORE, we have represented the graphFootnote 18 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).
\(\square \)
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.
Change history
05 February 2019
In a previous version of this publication, the affiliation of the second editor was incomplete. This has now been corrected.
Notes
- 1.
- 2.
The expressive power of first-order logic makes its use necessary for the representation of mappings that characterize features that are not representable in lightweight languages, such as Description Logics. In addition, checking the correctness of those mappings results facilitated by the fact that first-order theorem proving in standard first-order logic is a mature field, and, although semi-decidable, first-order reasoning on small modules results in an acceptable trade-off among expressivity and efficiency.
- 3.
This paper is an extended and expanded version of the paper “Verifying and Mapping the Mereotopology of Upper-Level Ontologies” that originally appeared in the Proceedings of Knowledge Engineering and Ontology Design (KEOD) 2016 [16].
- 4.
We assume that an ontology is a set of sentences called axioms closed under logical entailment that state the properties that characterize the behaviour of a set of symbols representing constants, relations and functions, called the signature of the ontology.
- 5.
A representation theorem is a theorem that formally classifies a given class of structures as equivalent to another class of structures whose properties are better understood. The stated equivalence makes possible the extrapolation of those properties to the classified structures, facilitating their understanding.
- 6.
- 7.
- 8.
A theory \({T'}\) is a conservative extension of a theory T if every theorem of T is a theorem of \({T'}\), and every theorem of \({T'}\) in the signature of T is also a theorem of T.
- 9.
The proofs for all Propositions have been found using the Prover9 automated theorem prover, and models were constructed using Mace4. Results are available at: colore.oor.net/ontologies/sumo/mereotopology/proofs.
- 10.
- 11.
- 12.
- 13.
- 14.
- 15.
Axioms (48), (49), (53), and (54) are the instantiation of DOLCE higher-order axiom schemas for the subcategories of main categories Q and R which are relevant for our work. A complete version of DOLCE-CORE mereology represented in first-order logic is available at colore.oor.net/ontologies/dolce-core/mereology.in.
- 16.
It can be proved that in an extensional mereology non-atomic entities whose proper parts are the same, are identical, i.e., every entity is exhaustively defined by its parts.
- 17.
Available at colore.oor.net/ontologies/sumo/modules.
- 18.
A n-ary function f from \(A^n\) to B is representable by a relation \(\varrho \) with arity (n+1), called the graph of f, such that:
(a) Every tuple of \(\varrho \) is a tuple \(\langle \bar{x}, f(\bar{x})\rangle \) with \(\bar{x}\in A^n\) and \(f(\bar{x}) \in range(f)\).
(b) If \(f(\bar{x})=b\) and \(f(\bar{z})=c\), then \(b=c\).
References
Benzmüller, C., Pease, A.: Higher-order aspects and context in SUMO. J. Web Sem. 12, 104–117 (2012)
Borgo, S., Masolo, C.: Foundational choices in DOLCE. In: Staab, S., Studer, R. (eds.) Handbook on Ontologies. IHIS, pp. 361–381. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-540-92673-3_16
Casati, R., Varzi, A.C.: Parts and Places: The Structures of Spatial Representation. A Bradford Book. MIT Press, Cambridge (1999)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002). Cambridge mathematical text books
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, Cambridge (1972)
Euzenat, J., Shvaiko, P.: Ontology Matching, 2nd edn. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38721-0
Gangemi, A., Guarino, N., Masolo, C., Oltramari, A.: Sweetening WORDNET with DOLCE. AI Mag. 24(3), 13–24 (2003)
Gangemi, A., Guarino, N., Masolo, C., Oltramari, A., Schneider, L.: Sweetening ontologies with DOLCE. In: Gómez-Pérez, A., Benjamins, V.R. (eds.) EKAW 2002. LNCS (LNAI), vol. 2473, pp. 166–181. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45810-7_18
Grenon, P., Smith, B.: SNAP and SPAN: towards dynamic spatial ontology. Spat. Cogn. Comput. 4(1), 69–103 (2004)
Grüninger, M., Hahmann, T., Hashemi, A., Ong, D.: Ontology verification with repositories. In: Proceedings of the Sixth International Conference Formal Ontology in Information Systems, FOIS 2010, Toronto, Canada, 11–14 May 2010, pp. 317–330 (2010)
Guarino, N.: Formal ontology and information systems. In: Formal Ontology in Information Systems - Proceedings of FOIS 1998, Trento, Italy, 6–8 June 1998, pp. 3–15. IOS Press, Amsterdam, pp. 3–15 (1998)
Guarino, N., Welty, C.: Evaluating ontological decisions with ontoclean. Commun. ACM 45(2), 61–65 (2002)
Hayes, P.: Catalog of temporal theories. Technical report UIUC-BI-AI-96-01. University of Illinois Urbana-Champagne (1996)
Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: WonderWeb deliverable D18 ontology library (final). Technical report, IST Project 2001–33052 WonderWeb: Ontology Infrastructure for the Semantic Web (2003)
McCune. W.: Prover9 and Mace4 (2005–2010). http://www.cs.unm.edu/mccune/prover9/
Silva Muñoz, L., Grüninger, M.: Verifying and mapping the mereotopology of upper-level ontologies. In: Knowledge Engineering and Ontology Design, KEOD 2016, Porto, Portugal, 9–11 November 2016, pp. 31–42 (2016)
Niles, I., Pease, A.: Linking lexicons and ontologies: mapping WordNet to the suggested upper merged ontology. In: Proceedings of the 2003 International Conference on Information and Knowledge Engineering (IKE 2003), Las Vegas, Nevada (2003)
Niles, I., Pease, A.: Towards a standard upper ontology. In FOIS 2001: Proceedings of the international conference on Formal Ontology in Information Systems, pp. 2–9. ACM, New York (2001)
Pearce, D., Valverde, A.: Synonymous theories and knowledge representations in answer set programming. J. Comput. Syst. Sci. 78(1), 86–104 (2012)
Silva Muñoz, L., Grüninger, M.: Mapping and verification of the time ontology in SUMO. In: Formal Ontology in Information Systems - Proceedings of the 9th International Conference, FOIS, 6–9 July 2016, Annecy, France (2016)
Varzi, A.C.: Spatial reasoning and ontology: parts, wholes, and locations. In: Aiello, M., Pratt-Hartmann, I., Van Benthem, J. (eds.) Handbook of Spatial Logicspages, pp. 945–1038. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4_15
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Silva Muñoz, L., Grüninger, M. (2019). The Mereologies of Upper Ontologies. In: Fred, A., Dietz, J., Aveiro, D., Liu, K., Bernardino, J., Filipe, J. (eds) Knowledge Discovery, Knowledge Engineering and Knowledge Management. IC3K 2016. Communications in Computer and Information Science, vol 914. Springer, Cham. https://doi.org/10.1007/978-3-319-99701-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-99701-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99700-1
Online ISBN: 978-3-319-99701-8
eBook Packages: Computer ScienceComputer Science (R0)