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 therefore 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 application of the generic ontologies within COLORE for the specification of mappings between upper ontologies and the design of new upper ontologies. After providing background 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-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 upper ontology based on the generic ontologies within COLORE, which will support the semantic integration of international standards.
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 concepts 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 axiomatization 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.
The basic organizational principle in COLORE is the notion of a hierarchy [7], which is a set of ontologies 5 with the same signature.
Within COLORE, there are many ontologies which axiomatize classes of mathematical 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 contains 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 conditions for generic ontologies through a formalization of the notions of ontological commitments 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 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.
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 axiomatizes 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 second 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.
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 ontologies (e.g., OWL-Time). Through verification, we characterize the models of an ontology 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 T 0 be a theory with signature Σ(T 0 ) and let T 1 be a theory with signature
The key to this endeavour is the property of logical synonymy: two theories T 1 and T 2 are synonymous iff there exist two sets of translation definitions ∆ and Π, respectively from T 1 to T 2 and from T 2 to T 1 , such that T 1 ∪ Π is logically equivalent to T 2 ∪ ∆. 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 ontologies 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.
SUMO [14] is an open source formal foundational ontology axiomatizing, among others, 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 expected 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 expressive 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.
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 T sumo ordered timepoints ∪ T sumo timeintervals that is logically synonymous with the mathematical ontologies:
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 unintended 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 unintended models, and then the extended theory T sumo ordered timepoints ∪ T sumo timeintervals was verified, characterizing its models up to elementary equivalence.
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 models, so that a nonconservative extension of SUMO was proposed. It also led to the identification 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 T comp mereology .
The Descriptive Ontology for Linguistic and Cognitive Engineering DOLCE [6] [10] originated as part of the WonderWeb project 8 , 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.
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.
The goal for TUpperWare is to support the ontological analysis of relevant existing standards and to integrate the ontologies within those standards, in particular:
• ISO 18629 (PSL) 9• OWL-Time10
• ISO 19150 (GeoSPARQL) 11 , ISO 19107 12• Semantic Sensor Network (SSN) Ontology 13In this sense, TUpperWare will be a requirements-driven upper ontology -the axiomatization must be strong enough to interpret the intended semantics of the terminology of each of the participating standards. 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 additional 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 T occupy 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 components of a physical object change), and the ontology of physical objects T opo leads to physical process ontology. This latter ontology includes the axiomatization of temporary parthood.
The reduction of a theory can also be used to decompose an ontology [7]. If T is reducible to S 1 , ..., S n , then there exist subtheories T 1 , ..., T n such that each T i is synonymous with S i . Since T is a conservative extension of each T i , 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 -T sumo ordered timepoints axiomatizes the linear ordering over timepoints, and T sumo timeintervals axiomatizes the relationship between timepoints and time intervals. An interesting outcome 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 modular fashion (i.e. by combining subtheories together); there is no need to modularize TUpperWare a posteriori. Table 2 is a comparison of the modules of TUpperWare and the reductive modules of DOLCE. The primary differences between the modularization of the two ontologies 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.
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 modules 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 translation 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 hierarchy.
Suppose T 1 , T 2 are two different generic ontologies, and S 1 , S 2 are two mathematical ontologies in the same hierarchy such that T 1 is synonymous with S 1 and T 2 is synonymous with S 2 . By the definition of synonymy, there exist translation definitions
These translation definitions can be combined in the following way to entail new theories
where T 1 , T 1 are in the same hierarchy, and where T 2 , T 2 are in the same hierarchy. We can therefore show that T 1 and T 2 are synonymous, and T 2 and T 1 are synonymous. The relationship between the upper ontologies T 1 and T 2 is now equivalent to the relationship between T 1 and T 1 on the one hand, and the relationship between T 2 and T 2 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 compositions of the mappings used in the verification of the generic ontologies. From translation 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) TimeInterval(x) ≡ timeinterval(x)
(∀x, y) begin(x, y) ≡ (begino f (x) = y)
(∀x, y) end(x, y) ≡ (endo f (x) = y)
(∀x, y, z) interval(x, y, z) ≡ (between(x, y) = z)
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 timepoints. 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.
The "sideways" perspective, in which upper ontologies are composed of generic ontologies, 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: 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.