=Paper=
{{Paper
|id=Vol-2050/foust-paper2
|storemode=property
|title=Upper Ontologies in COLORE
|pdfUrl=https://ceur-ws.org/Vol-2050/FOUST_paper_2.pdf
|volume=Vol-2050
|authors=Michael Gruninger,Carmen Chui,Megan Katsumi
|dblpUrl=https://dblp.org/rec/conf/jowo/GruningerCK17
}}
==Upper Ontologies in COLORE==
https://ceur-ws.org/Vol-2050/FOUST_paper_2.pdf
Upper Ontologies in COLORE
Michael GRÜNINGER a,1 , Carmen CHUI a and Megan KATSUMI a
a Department of Mechanical & Industrial Engineering, University of Toronto
Abstract. This paper explores an alternative vision for upper ontologies which is
more effective at facilitating the sharability and reusability of ontologies. The no-
tion of generic ontologies is characterized through the formalization of ontological
commitments and choices. Ontology repositories are used to modularize ontologies
so that any particular upper ontology is equivalent to the union of a set of generic
ontologies. In this way, upper ontologies are not replaced but rather integrated with
other theories in the ontology repository.
Keywords. upper ontologies, ontology design, ontology verification, modularization,
ontology repository, COLORE, DOLCE, SUMO, TUpperWare
1. Introduction
Within the applied ontology community, upper ontologies are widely recognized as tools
to support the tasks of ontology design and semantic integration. In both of these tasks,
the existence of unintended models (through an axiomatization that is too weak) or the
omission of models (through an axiomatization that is too strong) can lead to serious
problems. With semantic integration, for example, we must be able to guarantee that the
inferences made with sentences exchanged between software applications are equivalent
to the inferences made with respect to the applications’ intended models – given some
input the application uses these intended models to infer the correct output. The existence
of unintended models can therefore prevent semantic integration.
Verifying that upper ontologies do not have unintended models (which can be ruled
out with further axiomatization), and that they are not missing intended models, is there-
fore critical to the application of upper ontologies. This paper summarizes results about
the application of the mathematical ontologies within the Common Logic Ontology
Repository (COLORE)2 [7] for the verification of upper ontologies, as well as the ap-
plication of the generic ontologies within COLORE for the specification of mappings
between upper ontologies and the design of new upper ontologies. After providing back-
ground material on the use of an ontology repository for the design and verification of
upper ontologies, we review the extensive work that has been done in the verification
and modularization of two upper ontologies, the Descriptive Ontology for Linguistic and
Cognitive Engineering (DOLCE)3 and Suggested Upper Merged Ontology (SUMO)4 .
We then show how the translation definitions used for the verification of the upper on-
1 Corresponding Author: Michael Grüninger; E-mail: gruninger@mie.utoronto.ca
2 http://colore.oor.net/
3 http://www.loa.istc.cnr.it/old/DOLCE.html
4 http://www.adampease.org/OP/
tologies allows for the automatic generation of direct semantic mappings between the
ontologies themselves. We finish the paper with the design and verification of a new up-
per ontology based on the generic ontologies within COLORE, which will support the
semantic integration of international standards.
2. Building Upper Ontologies within a Repository
Upper ontologies have traditionally arisen from the approach in which concepts that are
common across a set of domains can be axiomatized at a general level. The rationale is
that reuse across domains is to be supported through specialization of the general con-
cepts from an upper ontology. Similarly, semantic integration between ontologies is to
be achieved through the general concepts they specialize. The work of [8] presented an
alternative perspective (referred to as the sideways approach) to the conventional upper
ontology paradigm. Rather than think of an upper ontology as a monolithic axiomati-
zation centred on a taxonomy, the sideways approach considers an upper ontology to
be a modular ontology composed of generic ontologies that cover concepts including
those related to time, process, and space. The verification of the upper ontology follows
from the verification of these generic ontologies, and the metalogical property known as
reducibility.
In this section, we will review the basic principles of COLORE that are needed in
order to characterize upper ontologies and their verification.The key techniques are based
on the identification of the different relationships between ontologies – nonconservative
extension for ontologies with the same signature, and synonymy for ontologies that have
different signatures. We will later see how this supports the specification of mappings
between upper ontologies.
2.1. Generic Ontologies
The basic organizational principle in COLORE is the notion of a hierarchy [7], which is
a set of ontologies5 with the same signature.
Within COLORE, there are many ontologies which axiomatize classes of mathe-
matical structures such as orderings, graphs, groups, and geometries. In the hierarchies
of such mathematical ontologies, the root theory axiomatizes an elementary class of
structures, and in principle, we can consider any consistent extension of the root theory
to axiomatize some subclass of the structures. On the other hand, COLORE also con-
tains many ontologies that axiomatize generic domains such as time, process, space, and
shape. How can we distinguish between generic ontologies (which are intuitively about
concepts) and the mathematical ontologies?
The work of [8] used the relationships among ontologies to propose necessary con-
ditions for generic ontologies through a formalization of the notions of ontological com-
mitments and ontological choices. While the ontological commitments are formalized by
the set of axioms that are inherent in a particular generic concept, i.e. the assumptions a
5 We follow previous work in terminology and notation treating ontologies as logical theories [7]. We do
not distinguish between logically equivalent theories. For every theory T , Σ(T ) denotes its signature, which
includes all the constant, function, and relation symbols used in T , and L (T ) denotes the language of T , which
is the set of first-order formulae that only use the symbols in Σ(T ).
relation must satisfy to be referred to by the concept’s name, ontological choices capture
the idea that certain additional assumptions may be desirable in a particular domain or
application, but which are not satisfied for all the various interpretations of the particular
generic concept. In terms of COLORE, ontological commitments are axiomatized within
the root theory of the hierarchy and the ontological choices are axiomatized by the trunk
theories of the hierarchy.
2.2. Redefining Upper Ontologies
The central claim of [8] is that an upper ontology is a reducible ontology that has a
reduction whose reductive modules are all generic ontologies. Each upper ontology is
therefore composed of a set of generic ontologies, and each generic ontology axioma-
tizes a particular set of generic concepts (e.g., the classes and relations relevant for time,
process, and space).
This approach leads to two observations. First, the verification of an upper ontology
leads to an understanding of the conceptual scope of the upper ontology as the set of
generic ontologies that are its reductive modules. This in turn allows us to compare upper
ontologies both in terms of coverage but also in terms of the axiomatizations of their
generic ontology modules.
Whereas the above discussion focuses on the analysis of upper ontologies, the sec-
ond observation that we can make is about the design of upper ontologies. New upper
ontologies can be designed by the union of different generic ontologies that already exist
within the ontology repository. We will apply this idea in the last section of this paper to
design and evaluate a new upper ontology.
3. Verification of Upper Ontologies
In this section, we review the work that has been done in ontology verification using
COLORE, as applied to upper ontologies (DOLCE and SUMO) and related generic on-
tologies (e.g., OWL-Time). Through verification, we characterize the models of an on-
tology up to isomorphism. For upper ontologies, we do not do this directly, but rather we
specify mappings between the upper ontology and existing mathematical ontologies in
COLORE whose models have already been characterized up to isomorphism.
Definition 1 Let T0 be a theory with signature Σ(T0 ) and let T1 be a theory with signature
Σ(T1 ) such that Σ(T0 ) ∩ Σ(T1 ) = 0.
/ Translation definitions for T0 into T1 are conservative
definitions in Σ(T0 ) ∪ Σ(T1 ) of the form
∀x pi (x) ≡ Φ(x)
where pi (x) is a relation symbol in Σ(T0 ) and Φ(x) is a formula in Σ(T1 ).
The key to this endeavour is the property of logical synonymy: two theories T1 and
T2 are synonymous iff there exist two sets of translation definitions ∆ and Π, respectively
from T1 to T2 and from T2 to T1 , such that T1 ∪ Π is logically equivalent to T2 ∪ ∆. By the
results in [13], there is a bijection on the sets of models for synonymous theories. We can
therefore characterize the models of the ontology being verified by demonstrating that
the ontology is synonymous with a logical theory whose models we understand.
Ontology verification allows us to identify unintended models (and hence propose
missing axioms) for the upper ontology, as well as identify omitted models (and hence
recommend the removal of axioms) for the upper ontology. Of course, this immediately
leads to the question of how we can determine that certain models of an upper ontology
are unintended. Whereas domain ontologies (e.g., in bioinformatics and commerce) are
often designed with respect to a set of semantic requirements and competency questions,
upper ontologies are implicitly designed to support interoperability. Since generic on-
tologies form reductive modules of an upper ontology, the problem of identifying the
unintended and omitted models of an upper ontology is equivalent to determining that
certain models of a generic ontology are unintended. In the following, we will see how
these ideas play out in the context of the generic ontologies for time and mereotopology
within the SUMO and DOLCE upper ontologies.
3.1. SUMO
SUMO [14] is an open source formal foundational ontology axiomatizing, among oth-
ers, general concepts such as those needed to represent temporal and spatial location,
mereotopology, units of measure, objects and processes. As an upper ontology, it is ex-
pected to be used as a global reference for semantics, and its axiomatization reused in
the construction of domain and application ontologies for automated reasoning in ex-
pressive languages. 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.
3.1.1. SUMO-Time
The work of [11] focused on the core axioms of the TEMPORAL subtheory covering
the complete axiomatization of time through intervals and points, which was referred
to as SUMO Time. In this subtheory, both timepoints and time intervals are elements
of the domain, which is similar to the ontological commitments made by generic time
ontologies such as OWL-Time and Endpoints.
The central result of [11] is the verification of a nonconservative extension of
SUMO-Time; that is, SUMO-Time was extended to a new ontology Tsumo ordered timepoints ∪
Tsumo timeintervals that is logically synonymous with the mathematical ontologies:
Tbounded linear ordering 6 ∪ Tstrict graphical 7
Without the additional axioms, this aforementioned Theorem cannot be proven, and this
is equivalent to saying that there are unintended models of SUMO-Time. In this way,
the verification of SUMO-Time in [11] led to the identification of three classes of un-
intended models – models with a unique timepoint, models with partially ordered sets
of timepoints (rather than linearly ordered sets), and models in which time intervals are
temporal parts of timepoints. Three new axioms were proposed to eliminate these unin-
tended models, and then the extended theory Tsumo ordered timepoints ∪ Tsumo timeintervals was
verified, characterizing its models up to elementary equivalence.
6 http://colore.oor.net/orderings/bounded_linear_ordering.clif
7 http://colore.oor.net/bipartite_incidence/strict_graphical.clif
3.1.2. SUMO-Mereotopology
SUMO also contains a subtheory that axiomatizes a part relation, together with other
mereological relationships such as the sum, product, and difference of elements. The
work of [12] and [15] provide a characterization of the models of this subtheory. As was
the case with SUMO-Time, the verification led to the identification of unintended mod-
els, so that a nonconservative extension of SUMO was proposed. It also led to the iden-
tification of omitted models, that is, the axiomatization of SUMO eliminated intended
models, namely, mereologies that are not equivalent to linear orderings. A proposal was
made to weaken the axioms, and the resulting subtheory was shown to be synonymous
the mereology Tcomp mereology .
3.2. DOLCE
The Descriptive Ontology for Linguistic and Cognitive Engineering DOLCE [6] [10]
originated as part of the WonderWeb project8 , which aimed to provide the infrastructure
required for a large-scale deployment of ontologies intended to be the foundation for
the Semantic Web. The work of [9] was the first to demonstrate the consistency of the
DOLCE upper ontology, but it only proved the existence of a model rather than provide
a characterization of all of the models of DOLCE. [2] and [3] provide the verification
of DOLCE. Unlike the case with SUMO, no unintended models were discovered, and
hence no additional axioms were proposed. A wide range of mathematical ontologies are
required to characterize the models of DOLCE.
4. TUpperWare
As we observed earlier in the paper, new upper ontologies can be designed by the union
of different generic ontologies that already exist within the ontology repository. In this
section, we propose a verified ontology whose reductive modules are generic ontologies
in COLORE.
4.1. Generic Ontology Modules
The goal for TUpperWare is to support the ontological analysis of relevant existing stan-
dards and to integrate the ontologies within those standards, in particular:
• ISO 18629 (PSL)9
• OWL-Time10
• ISO 19150 (GeoSPARQL)11 , ISO 1910712
• Semantic Sensor Network (SSN) Ontology13
In this sense, TUpperWare will be a requirements-driven upper ontology – the axioma-
tization must be strong enough to interpret the intended semantics of the terminology of
each of the participating standards.
8 http://wonderweb.semanticweb.org
9 https://www.iso.org/standard/35431.html
10 https://www.w3.org/TR/owl-time/
11 http://www.opengeospatial.org/standards/geosparql
12 https://www.iso.org/standard/26012.html
13 http://purl.oclc.org/NET/ssnx/ssn
Ontological Category Generic Ontology Module
time http://colore.oor.net/combined_time/interval_
with_endpoints.clif
activity, participation, state http://colore.oor.net/process_specification_
language/psl_outcore.clif
duration http://colore.oor.net/duration/point_duration.
clif
space, boundaries http://colore.oor.net/multidim_mereotopology_
codib/codib.clif
location, physical bodies http://colore.oor.net/occupy/occupy_root.clif
shape http://colore.oor.net/boxworld/boxworld.clif
mereotopology of physical objects http://colore.oor.net/component/component.clif
physical objects http://colore.oor.net/opo/opo.clif
Table 1. Ontological categories and modules within the TUpperWare ontology.
To this end, TUpperWare currently consists of the generic ontology modules shown in
Table 1. The scope of TUpperWare is determined by the task of standards integration
– each of the generic ontologies is needed to support one of the participating standards.
Each of the generic ontologies is a reductive module of TUpperWare. There are no ad-
ditional bridge axioms in a combined signature across these modules. The verification
of TUpperWare is therefore trivial, being equivalent to the verification of each of the
generic ontologies.
TUpperWare also contains modules for reasoning about state designed using the
methodology of [1], so that domain state ontologies and domain process ontologies are
specified based on corresponding generic ontologies. For example, the location module
Toccupy within TUpperWare leads to the motion ontology (i.e. how location changes),
the mereotopology of physical objects leads to the assembly ontology (i.e. how compo-
nents of a physical object change), and the ontology of physical objects Topo leads to
physical process ontology. This latter ontology includes the axiomatization of temporary
parthood.
5. Modularization of Upper Ontologies
The reduction of a theory can also be used to decompose an ontology [7]. If T is reducible
to S1 , ..., Sn , then there exist subtheories T1 , ..., Tn such that each Ti is synonymous with
Si . Since T is a conservative extension of each Ti , we refer to the subtheories as the
reductive modules of T . We can therefore use the results from verification to modularize
upper ontologies.
The verification of SUMO-Time led to its decomposition into two modules –
Tsumo ordered timepoints axiomatizes the linear ordering over timepoints, and Tsumo timeintervals
axiomatizes the relationship between timepoints and time intervals. An interesting out-
come was a restructuring of SUMO-Time as the definitional extension of two modules,
thus greatly simplifying the axiomatization.
The verification of DOLCE led to a modularization that was strikingly different from
the modularization that was used in the consistency proof by [9]. Rather than sets of
axioms for relations such as constitution and temporary parthood, the reductive mod-
ules of DOLCE are subtheories for classes of elements – perdurants, physical endurants,
nonphysical endurants, and qualities.
On the other hand, the TUpperWare Ontology itself is explicitly designed in a mod-
ular fashion (i.e. by combining subtheories together); there is no need to modularize
TUpperWare a posteriori.
TUpperWare Module DOLCE Module
activity Perdurant (Tdolce perdurant )
participation, state Participation (Tdolce participation )
state –
duration –
space, boundaries ?
location, physical bodies ?
shape ?
mereotopology of physical objects Mereology (Tdolce mereology )
physical objects Physical Endurant (Tdolce PED )
motion ontology –
assembly process ontology –
physical process ontology –
? Nonphysical Endurant (Tdolce NPED )
? Dependence (Tdependence )
– Quality (Tdolce Quality )
Table 2. Comparison of modules in the TUpperWare and DOLCE ontologies. A dash (–) indicates that no there
is no corresponding module. A question mark (?) indicates an open problem as to whether a corresponding
module exists.
Table 2 is a comparison of the modules of TUpperWare and the reductive mod-
ules of DOLCE. The primary differences between the modularization of the two ontolo-
gies arise from the way they treat space, shape, and location. Within DOLCE, these are
treated as qualities, but it currently appears that this is a fundamentally different from the
representation in TUpperWare.
6. Mappings between Upper Ontologies
The area of ontology mappings covers a diverse range of techniques [5]. What do we
mean by mappings between ontologies? First, we are specifying mappings between mod-
ules of the upper ontologies. Second, we are identifying synonymous subtheories of each
pair of modules. Note that we are using the axioms alone – we are not using any prior
intuitive understanding of the concepts involved.
Mappings between upper ontologies are automatically generated from the transla-
tion definitions used in the verification of the upper ontologies [4]. Since each generic
ontology is synonymous with a mathematical theory, we can exploit the transitivity of
synonymy to compose mappings and identify the synonymous “images” within each hi-
erarchy.
Suppose T1 , T2 are two different generic ontologies, and S1 , S2 are two mathemat-
ical ontologies in the same hierarchy such that T1 is synonymous with S1 and T2 is
synonymous with S2 . By the definition of synonymy, there exist translation definitions
∆1 , Π1 , ∆2 , Π2 such that
T1 ∪ ∆1 |= S1 S1 ∪ Π1 |= T1
T2 ∪ ∆2 |= S2 S2 ∪ Π2 |= T2
These translation definitions can be combined in the following way to entail new theories
T1 ∪ ∆1 ∪ Π2 |= T20 T2 ∪ ∆2 ∪ Π1 |= T10
where T1 , T10 are in the same hierarchy, and where T2 , T20 are in the same hierarchy. We
can therefore show that T1 and T20 are synonymous, and T2 and T10 are synonymous. The
relationship between the upper ontologies T1 and T2 is now equivalent to the relationship
between T1 and T10 on the one hand, and the relationship between T2 and T20 on the other.
Using the results from the previous section, the relationship of TUpperWare to other
ontologies can easily be determined, since the mappings to DOLCE, SUMO are com-
positions of the mappings used in the verification of the generic ontologies. From trans-
lation definitions for SUMO-Time and the Process Specification Language (PSL)14 , we
can use this technique to generate the translation definitions directly between theories in
the SUMO-Time and PSL Hierarchies:
(∀x) TimePoint(x) ≡ timepoint(x) (1)
(∀x) TimeInterval(x) ≡ timeinterval(x) (2)
(∀x, y) begin(x, y) ≡ (begino f (x) = y) (3)
(∀x, y) end(x, y) ≡ (endo f (x) = y) (4)
(∀x, y, z) interval(x, y, z) ≡ (between(x, y) = z) (5)
Figure 1 summarizes the results with the verification of generic time ontologies and time
modules within upper ontologies. Figure 1(a) shows the modules that axiomatize the
ordering over timepoints, as well as the relationship between time intervals and time-
points. Figure 1(b) shows the mereology of time intervals that is axiomatized in the upper
ontologies. Note that DOLCE only axiomatizes the mereology over time intervals, and
does not contain a distinction between time intervals and timepoints, and hence does not
specify an ordering over temporal elements.
7. Summary
The “sideways” perspective, in which upper ontologies are composed of generic ontolo-
gies, has been proposed as a way of more effectively using upper ontologies to support
semantic integration and ontology design. This approach has been successfully applied to
the verification and modularization of existing upper ontologies (SUMO and DOLCE).
It is also being utilized in the design of a new upper ontology, TUpperWare, with the
objective of semantically integrating a set of international standards. The design of TUp-
perWare addresses important research questions for upper ontologies:
14 http://colore.oor.net/psl_core
interval_psl_core
sumo_time psl_core
interval_with_endpoints endpoints
finite_endpoints
finite_sim_vc_end
interval_point lp_infinite_end
strict_graphical bounded_linear_ordering
sumo_timeintervals sumo_ordered_timepoints psl_core_time
(a)
sumo_time
cem_G
U sumo_temporal_mereology
dolce_time_mereology cem_mereology
m_mereology
(b)
Figure 1. (a) Relationships between the time modules within upper ontologies. (b) Relationships between
the mereology modules within upper ontologies. In both, cloud shapes denote hierarchies, dotted lines denote
nonconservative extension, thin solid lines denote conservative extension, and thick lines denote synonymy.
Question 1 In addition to the generic ontologies in Table 1, which ones are missing?
For example, there are no modules of TUpperWare that are comparable to the notion of
dependence in DOLCE.
Question 2 Since upper ontologies are not complete logical theories, how incomplete
can an upper ontology be without being trivial?
This is not the question of whether the upper ontology has unintended models, since this
can usually be addressed by extension with additional axioms. Instead, this question is
about whether or not the models of the ontology should even be intended. On the other
hand, if an upper ontology is essentially a taxonomy with few additional axioms, there
will be many models, and it is difficult to claim that all of them will be intended.
References
[1] Bahar AAmeri. Using Partial Automorphisms to Design Process Ontologies. In FOIS, pages 309–322,
2012.
[2] Carmen Chui. Axiomatized Relationships between Ontologies. Master’s thesis, University of Toronto,
November 2013.
[3] Carmen Chui and Michael Grüninger. Mathematical Foundations for Participation Ontologies. In For-
mal Ontology in Information Systems - Proceedings of the Eighth International Conference, FOIS 2014,
September, 22-25, 2014, Rio de Janeiro, Brazil, pages 105–118, 2014.
[4] Carmen Chui and Michael Grüninger. Merging the DOLCE and PSL Upper Ontologies. In KEOD 2014
- Proceedings of the International Conference on Knowledge Engineering and Ontology Development,
Rome, Italy, 21-24 October, 2014, pages 16–26, 2014.
[5] Jérôme Euzenat and Pavel Shvaiko. Ontology Matching, Second Edition. Springer, 2013.
[6] Aldo Gangemi, Nicola Guarino, Claudio Masolo, Alessandro Oltramari, and Luc Schneider. Sweetening
Ontologies with DOLCE. In Knowledge Engineering and Knowledge Management. Ontologies and
the Semantic Web, 13th International Conference, EKAW 2002, Siguenza, Spain, October 1-4, 2002,
Proceedings, pages 166–181, 2002.
[7] Michael Grüninger, Torsten Hahmann, Ali Hashemi, Darren Ong, and Atalay Özgövde. Modular First-
Order Ontologies via Repositories. Applied Ontology, 7(2):169–209, 2012.
[8] Michael Grüninger, Torsten Hahmann, Megan Katsumi, and Carmen Chui. A sideways look at up-
per ontologies. In Formal Ontology in Information Systems - Proceedings of the Eighth International
Conference, FOIS 2014, September, 22-25, 2014, Rio de Janeiro, Brazil, pages 9–22, 2014.
[9] Oliver Kutz and Till Mossakowski. A Modular Consistency Proof for DOLCE. In Proceedings of the
Twenty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2011, San Francisco, California, USA,
August 7-11, 2011, 2011.
[10] Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari. Wonder-
Web Deliverable D18 Ontology Library (Final). Technical report, IST Project 2001-33052 WonderWeb:
Ontology Infrastructure for the Semantic Web, 2003.
[11] Lydia Silva Muñoz and Michael Grüninger. Mapping and verification of the time ontology in SUMO. In
Formal Ontology in Information Systems - Proceedings of the 9th International Conference, FOIS 2016,
Annecy, France, July 6-9, 2016, pages 109–122, 2016.
[12] Lydia Silva Muñoz and Michael Grüninger. Verifying and Mapping the Mereotopology of Upper-Level
Ontologies. In Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowl-
edge Engineering and Knowledge Management (IC3K 2016) - Volume 2: KEOD, Porto - Portugal,
November 9 - 11, 2016., pages 31–42, 2016.
[13] David Pearce and Agustı́n Valverde. Synonymous theories and knowledge representations in answer set
programming. J. Comput. Syst. Sci., 78(1):86–104, 2012.
[14] A. Pease, I. Niles, and J. Li. The suggested upper merged ontology: A large ontology for the semantic
web and its applications. In A. Pease, editor, Ontologies and the Semantic Web, Papers from the AAAI
Workshop. AAAI Press, 2002.
[15] Lydia Silva-Munoz and Michael Grüninger. Lecture Notes in Communications in Computer and Infor-
mation Science, chapter The Mereologies of Upper Ontologies. Springer, 2017.