Specifying Ontology Design Patterns
                     with an Ontology Repository

                           Michael Grüninger and Megan Katsumi

           Department of Mechanical and Industrial Engineering, University of Toronto
                             Toronto, Ontario, Canada M5S 3G8
            gruninger@mie.utoronto.ca, katsumi@mie.utoronto.ca


         Abstract. Within the Common Logic Ontology Repository (COLORE), the no-
         tion 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 character-
         ize 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.


1      Introduction
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 on-
tologies 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 pro-
posed in [6] and [5]. Different notions of ontology design patterns have been used,
ranging from syntactic criteria to structural properties of ontologies. As a result, sev-
eral methodological questions remain challenges – How can we evaluate ontology de-
sign patterns and their application? How are design patterns reused? Within COL-
ORE, design patterns are formalized as core ontologies within the repository. Patterns
are reused via the metatheoretic relationships of relative interpretation and definable
equivalence. In this sense, the ontology design patterns within COLORE are semantic
(model-theoretic) rather than syntactic. On the other hand, the approach described in
this paper can also be used to generate axioms for new ontologies, in which case we
can consider core ontologies to serve as syntactic templates for axioms.
    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 no-
tions 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 com-
pletely 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/
2   COLORE and Ontology Design Patterns

In general, Ontology Design Patterns (OPs) are meant to serve as reusable solutions
for various aspects of ontology design [6], and the structure of the ontologies in COL-
ORE and the relationships defined between them can provide similar support. COLORE
provides a means of sharing content ontology design patterns (CPs) while providing so-
lutions that address specific instances of some of the modelling problems that other OPs
are designed to solve.
    Of the six families of OPs recognized in [6], the Structural, Correspondence, and
Content families of OPs have strong parallels in COLORE:


Structural OPs include what are referred to as Logical and Architectural OPs. Archi-
    tectural OPs represent possible structures for an ontology being designed. These
    structures are meant to assist with design choices when computational complexity
    is a concern, and also to serve as reference material to guide designers in creating
    their own structures. In particular, external Architectural OPs provide patterns for
    ontology modularization, (“meta-level constructs"). Examples of these external Ar-
    chitectural OPs can be found in COLORE as each ontology is stored in modules[9]
    that are connected to form the ontology using the imports relation.
Correspondence OPs include what are referred to as Reengineering and Mapping
    OPs. Mapping OPs provide a means to describe the relationship(s) that exist be-
    tween 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 sec-
    tion.
Content OPs (CPs) appear to be the most widely used family of OPs. They are typi-
    cally domain oriented and provide axioms that are intended to be reused as “build-
    ing 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 use-
    ful 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 ([11],[8]).



3   Relationships between Ontologies in COLORE

The sets of ontologies within COLORE are organized based on the notion of the reduc-
tion 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     Relative Interpretation

The notion of interpretability between theories2 is widely used within mathematical
logic and applications of ontologies for semantic integration [14]. We will adopt the
definition of relative interpretation from [4], in which the mapping π is an interpretation
of a theory T1 with language. L1 into a theory T2 with language L2 iff it preserves the
theorems of T1 .

Definition 1. An interpretation π of a theory T1 into a theory T2 is faithful iff

                                       T1 6|= σ ⇒ T2 6|= π(σ)

for any sentence σ ∈ L(T1 ).

    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.

Definition 2. Two theories T1 and T2 are definably equivalent iff T1 is faithfully inter-
pretable in T2 and T2 is faithfully interpretable in T1 .

    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 in-
terpretable 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.

Definition 3. Let T0 be a theory with signature Σ(T0 ) and let T1 be a theory with
signature Σ(T1 ) such that Σ(T0 ) ∩ Σ(T1 ) = ∅.
Translation definitions for T0 into T1 are sentences 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 L(T1 ).

    Translation definitions can be considered to be an axiomatization of the interpreta-
tion 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 charac-
     terize a first-order theory, which is the closure of the ontology’s axioms under logical entail-
     ment.
        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       Hierarchies
If an ontology is characterized by its set of ontological commitments, then such com-
mitments 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. Us-
ing 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
                                                                     T1 |= σ ⇒ T2 |= σ
        for any σ ∈ L(T1 ).


         discrete
                                final_discrete
      linear_order                               initial_discrete   bounded discrete     initial_dense              bounded dense     final_dense          dense
                                 linear_order
         no_end                                    linear_order       linear_order        linear_order               linear_order     linear_order     linear_order
                                                                                                                                                          no_end




         discrete                                                                                                                         dense
      linear_order                                                                                                                    linear_order
                                          bounded
                                        linear_order




                  discrete_chains
                                                       tree           linear_order
     discrete_forest


                                                     forest
    discrete                                                                                                                             dense
 semilinear_order                                                                                                                   semilinear_order


                                                                                       semiorder
                                                                                                                                                   dense
                                                                                                                                               weak_separative

                                                                                                                  lattice
                                                                    semilinear_order interval_order

                                                                                                        partial             total_preorder
                       chains                                                                         semiorder
       discrete                                                                                                                         dense
                                                                                       weak_order
     partial_order                                                                                           semilattice             partial_order


                                                                     series_parallel




                                                                     partial_order




     discreteness                max_exists        min_exists         quasi-order                                                       density




                                                                       transitivity




Fig. 1. Ontologies in Hordering : the core hierarchy of orderings. Dashed lines denote nonconser-
vative extension. Theories in bold are ones which are used in this paper.


    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 [15] for a full discussion of these ontologies).
 3
     http://code.google.com/p/colore/source/browse/trunk/ontologies/core/ordering
 4
     http://code.google.com/p/colore/source/browse/trunk/ontologies/core/mereology
                                 cem_C            cem_G        cem_notG            cem_notC




                                                    cem_mereology




                                                    mem_mereology



                                                     em_mereology




                                                   ppp_mm_mereology                     tree_mm_mereology
               ex_cm_mereology
                                                                      inclusion_space

                                 ppp_m_mereology
      cm_mereology                                 ex_mm_mereology


                                                                    dense_mm_mereology

                                 ex_m_mereology      mm_mereology                         tree_mereology

  prod_mereology        sum_mereology

                                                                      dense_mereology discrete_mereology




                                                     m_mereology




Fig. 2. Ontologies in Hmereology : the hierarchy of mereologies. Dashed lines denote nonconser-
vative extension. Theories in bold are ones which are used in this paper.


    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 axiom-
atization 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.

3.3     Reducibility
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 model-
theoretic notion of reducibility introduced in [8].

Definition 5. A ontology T is reducible to a set of ontologies T1 , ..., Tn iff
 1. T faithfully interprets each Ti , and
 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 [9] characterizes the relationship between reducibility
and definable equivalence, and it will be used in this paper to prove results about re-
ducibility:
Theorem 1. Let T1 , ..., Tn be a set of ontologies such that Σ(Ti ) ∩ Σ(Tj ) = ∅ for all
1 ≤ i, j ≤ n, i 6= j.
   A ontology T is reducible to T1 , ..., Tn iff T is definably equivalent to
   T1 ∪ ... ∪ Tn .
    Section 4 will present the reductions of several different ontologies, and discuss
their relationship to design patterns.

3.4   Core and Complex Hierarchies
The notion of the reducibility of ontologies can be used to specify an ordering on the
set of hierarchies.
Definition 6. Let H1 , ..., Hn be a finite set of hierarchies.
   A repository R = hR, vi is a partially ordered set where
 – R = {H1 , ..., Hn };
 – 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.
    An ontology T is a core ontology theory iff it is in a core hierarchy.
    A complex hierarchy H = hH, ≤i is a hierarchy which is not minimal in the reposi-
tory hR, vi.
    An ontology T is a complex ontology iff it is in a complex hierarchy.
    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 addi-
tional ontological commitments on a core ontology (e.g. the root theory of theory of the
Hmereology Hierarchy imposes additional ontological commitments that make the part-
hood relation reflexive and antisymmetric). If the repository contains multiple equiva-
lent 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 no-
tion of reducibility, rather than on the distinction between generic vs domain ontologies,
as in [13].
4      Hierarchies as Design Patterns
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     Subposet Hierarchy
Each ontology in the Subposet Hierarchy5 is an extension of an ontology from the
Mereology Hierarchy and an ontology from the Ordering Hierarchy.


                                       filter                         ideal




                                    upper_set                       lower_set




                                                    subposet




            lower_reverse   lower_preserve       chain_antichain         upper_preserve   upper_reverse




                                                  subposet_root




                                     mereology                     partial_ordering



Fig. 3. Ontologies in Hsubposet : the hierarchy of theories of relationships between partially or-
dered sets. Dashed lines denote nonconservative extension and solid lines denote conservative
extension. Ontologies in bold are ones which are used in this paper.


    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     Multimereology Hierarchy
Motivated by biomedical ontologies such as GALEN and Foundational Model of Anatomy,
Bittner and Donnelly ([2],[3]) have investigated a class of ontologies that combine
different kinds of mereological relations. In particular, they axiomatized three rela-
tions for part, component, and containment in an ontology which they call Tf o_pcc .
The subtheory for the part_of relation has models which are isomorphic to a dense
mereology with the weak supplementation principle. Models of the subtheory for the
component_of relation are isomorphic to discrete mereologies which satisfy the weak
supplementation principle as well as what Bittner and Donnelly refer to as the no-
partial-overlap property – if x and y are distinct overlapping objects, then either x is a
part of y or y is a part of x. Finally, models of the subtheory for the contained_in rela-
tion are isomorphic to a discrete partial ordering. Models of Tf o_pcc are amalgamations
of the models of the three subtheories, and they are referred to as parthood-component-
containment structures. Within the COLORE repository, these theories appear in the
Hmultimereology Hierarchy.
    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.

Theorem 2. Tf o_pcc is definably equivalent to
   (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 .

Theorem 3. Tppcmp is definably equivalent to the ontology
   Ttree_mm_mereology ∪ Tdense_weak_separative ∪ Tsubposet

Theorem 4. Tppcnt is definably equivalent to
   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" on-
tologies in Figure 3 that specifies how the mereology and partial ordering are amalga-
mated.


4.3     Periods Hierarchy

The axioms in the ontologies of the Hperiods Hierarchy7 were first proposed by van
Benthem in [1]. The key ontology of this hierarchy, referred to as Tperiod , constitutes
the minimal set of conditions that must be met by any period structure and has two
relations (precedence and inclusion) and two conservative definitions (for the glb and
overlaps relations) as its signature. Transitivity and irreflexivity axioms for the prece-
dence relation make it a strict partial order, and transitivity, reflexivity, and antisymme-
try axioms for the inclusion relation make it a partial order; the axioms of monotonicity
enforce correct interplay between the precedence and inclusion relations. Van Benthem
further includes an axiom that guarantees the existence of greatest lower bounds be-
tween overlapping intervals.

Theorem 5. Tperiod is definably equivalent to the ontology
Tprod_mereology ∪Tpartial_ordering ∪(Tupper_preserve ∪Tlower_reverse ∪Tchain_antichain ).


    The relationships between the ontologies in this hierarchy were explored in [12].
In particular, additional theories within the Hsubposet Hierarchy were shown to be de-
finably equivalent to various extensions of Tperiod as axiomatized by van Benthem.
This illustrates how we can use design patterns to specify the axiomatization of new
ontologies in a hierarchy. Conversely, a subtheory of Tperiod was used to identify a
new ontology within the Hsubposet Hierarchy, thus illustrating how we can abstract new
design patterns from a set of existing ontologies.

 7
     http://code.google.com/p/colore/source/browse/trunk/ontologies/complex/periods
4.4   Subactivities in the PSL Ontology

The PSL Ontology uses the subactivity relation to capture the basic intuitions for the
composition of activities. This relation is a discrete partial ordering, in which primitive
activities are the minimal elements.
     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 intu-
itions 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 occur-
rence 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. Al-
though 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 on-
tology
    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   Occurrence Trees in the PSL Ontology

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 oc-
currences 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) ac-
tivity. 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.

Theorem 7. The ontology Tpslcore ∪ Tocctree is definably equivalent to the ontology
   Ttree_mereology ∪ Ttree ∪ Tideal

    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   Discussion Points
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 on-
tologies 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 [6]: “CPs are small ontologies that mediate
between use cases (problem types) and design solutions. They are used as modelling
components: ideally, an ontology results from a composition of CPs, with appropri-
ate dependencies between them, plus the necessary design expansion based on specific
needs". Based on this definition, each ontology in COLORE could be considered to be
a CP as any of the modules could conceivably be reused to build other ontologies. How-
ever, in this paper we have focused on the core theories as they are most recognizable as
CPs - although they are not necessarily domain-oriented, they are definably equivalent
to theories that appear in multiple, different domains. They serve as syntactic templates
for axioms in a variety of domains, so in a sense they combine aspects of CPs with the
more domain-independent Logical OPs.
    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 devel-
opment 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 COL-
ORE, 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 [6] and the use of first-order logic in COLORE
supports this ideal as patterns from a wide range of languages may be represented.
    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 [6, 5], as future
plans for COLORE include the incorporation of competency questions as requirements
[10] to identify suitable ontologies.


References
1. van Benthem, Johan F. A. K. (1991) The Logic of Time: A Model-Theoretic Investigation into
   the Varieties of Temporal Ontology and Temporal Discourse, Springer; 2nd edition.
2. Bittner, T. (2004) Axioms for parthood and containment relations in bio-ontologies, Proceed-
   ings of KR-MED 2004: First International Workshop on Formal Biomedical Knowledge Rep-
   resentation.
3. Bittner, T. and Donnelly, M. (2005) Computational ontologies of parthood, componenthood,
   and containment. Proceedings of the Nineteenth International Joint Conference on Artificial
   Intelligence 2005 (IJCAI05). Kaelbling
4. Enderton, H.: Mathematical Introduction to Logic. Academic Press (1972)
5. Gangemi, A. (2005) Ontology Design Patterns for Semantic Web Content. Proc. of Interna-
   tional Semantic Web Conference, pp. 262–267, Springer.
6. Gangemi, A., and Presutti, V. (2009) Ontology Design Patterns. In: Handbook of Ontologies,
   2nd Edition, S. Staab (ed.), pp. 221–243, Springer.
7. Grüninger, M. (2009) Process Ontologies. In: Handbook of Ontologies, 2nd Edition, S. Staab
   (ed.), pp. 419–421, Springer.
8. Grüninger, M., Hahmann, T., Hashemi, A., and Ong, D. (2010) Ontology Verification with
   Repositories. Proc. of the Sixth Int. Conference on Formal Ontologies in Information Systems
   (FOIS 2010), pp. 317–330, IOS Press.
9. Grüninger, M., Hahmann, T., Hashemi, A., Ong, D., and Ozgovde, A. (2012) Modular first-
   order ontologies via repositories, Applied Ontology, 7:169-210.
10. Katsumi, M. (2011) A Methodology for the Development and Verifi-
   cation of Expressive Ontologies (Master’s Thesis). Retrieved from verb-
   https://tspace.library.utoronto.ca/bitstream/1807/31274/1/Katsumi_Megan_S_201111_MASc_thesis.pdf
11. Katsumi, M., and Grüninger, M. (2010) Theorem Proving in the Ontology Lifecycle. Proc.
   of Knowledge Engineering and Ontology Design
12. Ong, D. and Gruninger, M. (2011) Constructing an Ontology Repository: A Case Study with
   Theories of Time Intervals, Fourth International Workshop on Modular Ontologies. Ljubljana,
   Slovenia.
13. Scherp, A., Saathof, C., Franz, T. and Staab, S. (2011) Designing core ontologies, Applied
   Ontology 6:177-221.
14. Schorlemmer, M. and Kalfoglou, Y. (2008) Institutionalising Ontology-Based Semantic In-
   tegration, Applied Ontology 3:131-150.
15. Tsai, Hsing-chien (2009) Decidability of mereological theories, Logic and Logical Philoso-
   phy 18:45-63.