Within the Common Logic Ontology Repository (COLORE), the notion of reducibility among ontologies has been used to characterize relationships among ontologies. This paper uses techniques such as relative interpretation to show how one set of ontologies within the repository can be reused to characterize the models of other ontologies that are used in a wide variety of domains. A central theme of the paper is that ontology design patterns can be formalized as core ontologies within the ontology repository.
The COLORE (Common Logic Ontology Repository) project1 is building an open repository of first-order ontologies that serve as a testbed for ontology evaluation and integration techniques, and that can support the design, evaluation, and application of ontologies in first-order logic. The logical relationships among the set of first-order ontologies in the repository can also be used as basis for the verification of an ontology with respect to its intended models as well as decomposition of ontologies into modules.
We will show how COLORE follows the vision of ontology design patterns as
proposed in [
After an informal discussion of ontology design patterns in the context of COLORE, we give an overview of the relationships between ontologies within COLORE. The notions of relative interpretation, definable equivalence, and reduction play a key role in formalizing the reuse of ontologies. In particular, these notions give us techniques for evaluating ontology design patterns and proving that a pattern is correctly and completely exemplified by a set of ontologies. We will illustrate this approach using sets of ontologies within COLORE. 1 http://code.google.com/p/colore/source/browse/trunk/
In general, Ontology Design Patterns (OPs) are meant to serve as reusable solutions
for various aspects of ontology design [
Of the six families of OPs recognized in [
Correspondence OPs include what are referred to as Reengineering and Mapping OPs. Mapping OPs provide a means to describe the relationship(s) that exist between elements in different ontologies. Similarly, relationships are defined between the terms used in different ontologies in COLORE. In this way the relationships represent specific instances of Mapping OPs. Relationships between ontologies themselves are also described so that users may compare their semantics; these relationships are based on the notion of reducibility discussed in the following section.
Content OPs (CPs) appear to be the most widely used family of OPs. They are
typically domain oriented and provide axioms that are intended to be reused as
“building blocks" in order to construct an ontology. CPs can also serve other functions
in ontology development such as evaluation. Although they are not necessarily
domain-oriented, we view the core theories of COLORE to be examples of
useful CPs, as all ontologies in COLORE are reducible to sets of these ontologies.
Using the notion of intended models, the core theories in COLORE can also be
used for ontology verification ([
The sets of ontologies within COLORE are organized based on the notion of the reduction of one ontology to a set of ontologies. In this section, we review the background for understanding reduction and the role it plays in organizing ontologies within the repository. 3.1
The notion of interpretability between theories2 is widely used within mathematical
logic and applications of ontologies for semantic integration [
of a theory T1 into a theory T2 is faithful iff T1 6j= ) T2 6j= ( ) for any sentence
Thus, the mapping is a faithful interpretation of T1 if it preserves satisfiability with respect to T1. We will also refer to this by saying that T1 is faithfully interpretable in T2.
Definable equivalence is a generalization of the notion of logical equivalence to theories that do not have the same signature.
For example, the theory of timepoints is definably equivalent to the theory of linear orderings. On the other hand, although the theory of partial orderings is faithfully interpretable in the theory of timepoints, these two theories are not definably equivalent, since the theory of timepoints is not interpretable in the theory of partial orderings.
signature (T1) such that (T0) \ (T1) = ;.
Translation definitions for T0 into T1 are sentences in (T0) and let T1 be a theory with (T0) [
(T1) of the form 8x pi(x) (x) where pi(x) is a relation symbol in (T0) and (x) is a formula in L(T1).
Translation definitions can be considered to be an axiomatization of the interpretation of T0 into T1. As noted in the previous section, the use of translation definitions in COLORE is similar to Mapping OPs, insofar as they specify relationships between terms used in different ontologies in order to compare their semantics. 2 In this paper, we consider an ontology to be a set of first-order sentences (axioms) that characterize a first-order theory, which is the closure of the ontology’s axioms under logical entailment.
The non-logical lexicon (signature) of a first-order theory T , denoted by (T ), is the set of all constant symbols, function symbols, and relation symbols that are used in T .
The language of T , denoted by L(T ), is the set of all first-order formulas that only use the non-logical symbols in the signature (T ). 3.2
If an ontology is characterized by its set of ontological commitments, then such commitments will be formalized by sets of axioms. Moreover, in order for the commitments to be comparable, their axiomatizations need to be expressed in the same language. Using these intuitions, we can define an ordering over a set of theories: Definition 4. A hierarchy H = hH; <i is a partially ordered, finite set of ontologies H = T1; :::; Tn such that 1. L(Ti) = L(Tj ), for all i; j; 2. T1 T2 iff for any
The theories within two hierarchies in COLORE are shown in Figures 1 and 2. The Ordering Hierarchy3 contains ontologies that axiomatize different classes of orderings, such as partial orderings, linear orderings, trees, and lattices.
The Mereology Hierarchy4 contains ontologies that axiomatize different intuitions
related to the concept of parthood (see [
no_end lindeiasrc_roerteder
discrete_chains discrete_forest semidliinsecarer_teorder padrtiisacl_reotreder chains linedaern_soerder
dense semilinear_order total_preorder partdiaeln_soerder weak_dseenpsaerative linbeoaurn_doerdder tree forest linear_order semiorder
lattice semilinear_order interval_order weak_order sepmairotiradler
semilattice series_parallel partial_order transitivity cem_mereology mem_mereology em_mereology ppp_mm_mereology
m_mereology ex_cm_mereology
ppp_m_mereology cm_mereology
ex_mm_mereology prod_mereology
ex_m_mereology sum_mereology
dense_mm_mereology mm_mereology
tree_mereology inclusion_space
tree_mm_mereology dense_mereology discrete_mereology
Note that all extensions of ontologies in the same hierarchy are nonconservative. An
ontology T is a root ontology iff it is not the extension of any other ontology in the same
hierarchy. Within the Hordering Hierarchy, the root ontology is the axiomatization of
a transitive relation. Within the Hmereology Hierarchy, the root ontology is the
axiomatization of a basic mereology (in which the parthood relation is transitive, reflexive,
and antisymmetric). This ontology is definably equivalent to the theory Tpartial_order
within the Hordering Hierarchy.
Definable equivalence is a relationship between two ontologies; we can generalize this
to a relationship among sets of ontologies. The basis for this approach is the
modeltheoretic notion of reducibility introduced in [
2. T1 [ ::: [ Tn faithfully interprets T .
We will also refer to the set of ontologies T1; :::; Tn in the definition as the reduction of T in the repository.
It is easy to see that two definably equivalent ontologies are reducible to each other. For example, within COLORE, the ontology Tmereology is reducible to the ontology Tlinear_ordering and vice versa.
The following result from [
T1 [ ::: [ Tn.
Section 4 will present the reductions of several different ontologies, and discuss their relationship to design patterns. (Tj ) = ; for all 3.4
The notion of the reducibility of ontologies can be used to specify an ordering on the set of hierarchies.
A repository R = hR; vi is a partially ordered set where – R = fH1; :::; Hng; – Hi v Hj iff each root ontology in Hj has a reduction that contains a ontology T in Hi.
For example, we can show that Hordering v Hmereology , since the root ontology in Hmereology is definably equivalent to the ontology Tpartial_ordering in Hordering . On the other hand, Hmereology 6< Hordering , since the root ontology for Hordering (which is Ttransitive) is not reducible to any ontology in Hmereology .
Since we are dealing with repositories that contain a finite set of hierarchies, we are guaranteed that the partial ordering v has minimal elements.
Definition 7. A hierarchy C = hC; i is a core hierarchy iff it is a minimal hierarchy in the repository R = hR; vi.
A complex hierarchy H = hH; i is a hierarchy which is not minimal in the repository hR; vi.
Through the notion of reducibility, we can see that core ontologies play the role of building blocks for all other ontologies within the repository. A complex ontology is either constructed from a set of core ontologies or it is an ontology that imposes additional ontological commitments on a core ontology (e.g. the root theory of theory of the Hmereology Hierarchy imposes additional ontological commitments that make the parthood relation reflexive and antisymmetric). If the repository contains multiple equivalent core hierarchies, then the reduction will contain multiple definably equivalent core ontologies, and hence there might exist multiple reductions that contain different sets of core ontologies.
Within COLORE, the notion of a core ontology is therefore based on the logical
notion of reducibility, rather than on the distinction between generic vs domain ontologies,
as in [
Core ontologies within the repository can be definably equivalent to multiple ontologies in other hierarchies. In this sense, they play the role of design patterns that are reused to verify other ontologies; that is, they can be used to prove that the intended models of an ontology are isomorphic to the models of the axiomatization of the ontology. In this section, we consider in detail one set of core ontologies and show how its relationships to a surprising variety of other ontologies from remarkably different domains. 4.1
Each ontology in the Subposet Hierarchy5 is an extension of an ontology from the Mereology Hierarchy and an ontology from the Ordering Hierarchy.
filter upper_set
ideal lower_set subposet subposet_root lower_reverse lower_preserve chain_antichain upper_preserve
upper_reverse mereology partial_ordering
The ontologies shown in Figure 3 form the basis for the Hsubposet Hierarchy. The root ontology Tsubposet_root is the union of Tm_mereology and Tpartial_ordering , and is a conservative extension of each of these ontologies. Thus, each model of Tsubposet_root (and hence each model of any ontology in the hierarchy) is the amalgamation of a mereology substructure and a partial ordering substructure.
The ontologies shown in Figure 3 contain additional axioms that constrain how the mereology is related to the partial ordering. In models of Tsubposet, the mereology is a 5 http://code.google.com/p/colore/source/browse/trunk/ontologies/core/subposet/ subordering of the partial ordering. Tideal strengthens this condition by requiring that the mereology is a subordering of the partial ordering which forms an ideal. In models of Tchain_antichain, elements that are ordered by the mereology are not comparable in the partial ordering.
All ontologies within the Hsubposet Hierarchy combine one of the ontologies in Figure 3 together with one of the ontologies in Figure 2 and one of the ontologies in Figure 1. In the following sections, we will explore how different ontologies in the Hsubposet Hierarchy serve as design patterns. 4.2
Motivated by biomedical ontologies such as GALEN and Foundational Model of Anatomy,
Bittner and Donnelly ([
The ontology for parthood-component-containment structures also contains three axioms that specify how the substructures are combined. The component-of structure is a subordering of the parthood structure, while the relationship between containment and parthood satisfies the following two conditions – parts are contained in the container of the whole and that if a part contains something then so does the whole.
Bittner and Donnelly give an informal description of the models of their ontology, but do not provide a complete characterization of the models up to isomorphism. We can, however, use theories within the Hsubposet Hierarchy to verify 6 that the models of the ontologies are isomorphic to the intended models of Bittner and Donnelly.
(Ttree_mm_mereology [ Tdense_weak_separative [ Tsubposet) [(Tdense_mm_mereology [ Tdiscrete_mereology [ Tlower_preserve [ Tupper_preserve).
In this sense, we can prove that an ontology design pattern is correctly exemplified for given ontology O by proving that the core ontology is definably equivalent to O.
We can also use definable equivalence to extract multiple design patterns from the same ontologies in those cases where an ontology can be decomposed into modules. 6 The proofs for all theorems can be found in
http://stl.mie.utoronto.ca/colore/subposet-theorems.pdf Recognizing that Tf o_pcc is actually definably equivalent to two different ontologies in the Hsubposet Hierarchy, we can specify two ontologies, Tppcmp and Tppcnt, which form a modular decomposition of Tf o_pcc.
Ttree_mm_mereology [ Tdense_weak_separative [ Tsubposet
Tdense_weak_separative [ Tdiscrete_mereology [ Tlower_preserve [ Tupper_preserve It is important to note that Tppcmp and Tppcnt are each definably equivalent to a unique ontology within the Hsubposet Hierarchy. As stated in the previous section, each ontology within the Hsubposet Hierarchy is a combination an ontology in the Hordering Hierarchy, an ontology in Hmereology Hierarchy, and one of the “building block" ontologies in Figure 3 that specifies how the mereology and partial ordering are amalgamated. 4.3
The axioms in the ontologies of the Hperiods Hierarchy7 were first proposed by van
Benthem in [
Tprod_mereology [Tpartial_ordering [(Tupper_preserve[Tlower_reverse[Tchain_antichain).
The relationships between the ontologies in this hierarchy were explored in [
The core ontology8 Tsubactivity alone does not specify any relationship between the occurrence of an activity and occurrences of its subactivities. For example, we can compose paint and polish as subactivities of some other activity, say surf acing, and we can compose make_body and make_f rame into another activity, say f abricate. However, this specification of subactivities alone does not allow us to say that surf acing is a nondeterministic activity, or that f abricate is a deterministic activity.
The primary motivation driving the axiomatization of Tatomic is to capture intuitions about the occurrence of concurrent activities. Since concurrent activities may have preconditions and effects that are not the conjunction of the preconditions and effects of their activities, concurrency in models of Tatomic is represented by the occurrence of one concurrent activity rather than multiple concurrent occurrences.
Atomic activities are either primitive or concurrent (in which case they have proper subactivities). The core ontology9 Tatomic introduces the function conc that maps any two atomic activities to the activity that is their concurrent composition. Essentially, what we call an atomic activity corresponds to some set of primitive activities – every concurrent activity is equivalent to the composition of a set of primitive activities. Although Tsubactivity can represent arbitrary composition of activities, the composition of atomic activities is restricted to concurrency.
Theorem 6. The ontology Tsubactivity [ Tatomic_act is definably equivalent to the ontology
Tcem_mereology [ Tdiscrete_partial_ordering [ Tideal
By this Theorem, models of Tsubactivity [ Tatomic_act are isomorphic to a structure in which a mereological field (on the set of atomic activities) forms an ideal within a discrete partial ordering (on the set of all activities). 4.5
Within the PSL Ontology, an occurrence tree10 is a partially ordered set of activity occurrences, such that for a given set of activities, all discrete sequences of their occurrences are branches of the tree. An occurrence tree contains all occurrences of all activities; it is not simply the set of occurrences of a particular (possibly complex) activity. Because the tree is discrete, each activity occurrence in the tree has a unique successor occurrence of each activity.
In addition, there are constraints on which activities can possibly occur in some domain. Although occurrence trees characterize all sequences of activity occurrences, not all of these sequences will intuitively be physically possible within the domain. 8 http://code.google.com/p/colore/source/browse/trunk/ontologies/complex/psl/subactivity 9 http://code.google.com/p/colore/source/browse/trunk/ontologies/complex/psl/atomic 10 http://code.google.com/p/colore/source/browse/trunk/ontologies/complex/psl/occtree We will therefore want to consider the subtree of the occurrence tree that consists only of possible sequences of activity occurrences; this subtree is referred to as the legal occurrence tree.
Ttree_mereology [ Ttree [ Tideal Theorem 7. The ontology Tpslcore [ Tocctree is definably equivalent to the ontology
By this Theorem, models of Tpslcore [ Tocctree are isomorphic to a structure in which a tree mereology (on the set of legal activity occurrences) forms an ideal within a tree ordering (on the set of all activity occurrences). It is interesting to notice that Tideal is used both for this ontology as well as for Tsubactivity, demonstrating how one core ontology can be reused as a pattern across very different generic ontologies. 5
In the previous section we provided examples of the ways in which core ontologies within COLORE can be utilised as CPs. We showed how a variety of real-world ontologies were comprised of core theories from the same hierarchy, and how even the same core theories were reused in different ontologies. We also demonstrated how core ontologies could be used to verify that an ontology contained the desired CPs (core theories), and how new core ontologies (CPs) could be identified by abstracting from ontologies in COLORE.
The ontologies in COLORE’s hierarchies (specifically the core theories) correspond
well to the definition of CPs provided by [
In this paper we have also explored the way in which the relationships defined in
COLORE may be considered OPs, as the assistance they provide for ontology
development is similar to the aid provided by OPs. Nevertheless, some of the features of
COLORE offer capabilities beyond what is currently offered by the OP community.
For example, because of the formalized nature of the relationships specified in
COLORE, automated reasoning can be implemented to verify the mappings between the
ontologies. In addition, the notion of reducibility can be implemented to identify useful
CPs from ontologies in COLORE – the more theories that are reducible to a particular
core theory, the more useful it is. Automated theorem provers may also be used to verify
that an ontology is in fact a core theory. Lastly, OPs were not intended to be restricted
to a particular representation language [
We should emphasize that we do not believe that COLORE can or should replace
traditional OPs. Although there are aspects of OPs for which COLORE offers similar
solutions, there are also OPs which are completely absent from the relationships in
COLORE. We believe that COLORE offers useful perspectives on OPs that may be
beneficial to the OP community. In the other direction, much attention has been paid to
promoting the use of OPs (CPs specifically); the results of this may be useful for the
future development of COLORE. In particular, we can learn from the use of generalized
use cases and competency questions to aid in users in the reuse of CPs [