This paper outlines the reductive modularization and verification of the Descriptive Ontology for Linguistic and Cognitive Engineering (DOLCE). The ontology makes distinctions between enduring and perduring entities which is reflected in the resulting reductive modules, in contrast to previous work done to generate a consistency proof for DOLCE. We present our approach to verify DOLCE with mathematical theories in the Common Logic Ontology Repository (COL-ORE), and describe how the ontological commitments made by the authors of DOLCE have affected the resulting verification and reductive modularization.
Foundational ontologies, also called upper ontologies, characterize the semantics of general concepts that underlay every knowledge representation enterprise. Since foundational ontologies are expected to be broadly reused, verifying that they do not have unintended models and that they are not missing any intended models are of paramount interest for the knowledge representation community.
The Descriptive Ontology for Linguistic and Cognitive Engineering (DOLCE) 2 is an upper ontology of particulars that captures ontological categories found in natural language and human common sense [1,3]. DOLCE is widely used by a diverse array of domain ontologies, ranging from event recognition to geographical information systems [6], through specialization of its backbone taxonomy.
Previous work in [8] has demonstrated the consistency of DOLCE. In this paper, we give an overview of the verification of DOLCE, which in turn allows us to provide a characterization of the models of DOLCE up to isomorphism 3 . Ontology verification is the process by which a theory is checked to rule out its unintended models, and characterize any intended ones which might be missing. In this paper, we apply the definition of ontology verification based on representation theorems that was introduced in [4], which applies to the verification of ontologies axiomatized in first-order logic. It is particularly important to understand the models of upper ontologies such as DOLCE. First, it allows us to formally specify the relationships to other upper ontologies, and determine the similarities and differences among them. Second, a characterization of the models of DOLCE enables us to make its ontological commitments explicit. Ontology designers that create new domain-specific ontologies by extension of DOLCE can then be aware of the intended semantics of the concepts that they are using.
Verification is concerned with the relationship between the intended models of an ontology and the models of the axiomatization of the ontology. In particular, we want to characterize the models of an ontology up to isomorphism and determine whether or not these models are equivalent to the intended models of the ontology. This relationship between the intended models and the models of the axiomatization plays a key role in the application of ontologies in areas such as semantic integration and decision support.
Unfortunately, it can be quite difficult to characterize the models of an ontology up to isomorphism. Ideally, since the classes of structures that are isomorphic to an ontology's models often have their own axiomatizations, we should be able to reuse the characterizations of these other structures. We therefore specify mappings between the ontology being verified and some existing ontology 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 Σ(T 1 ) such that Σ(T 0 ) ∩ Σ(T 1 ) = / 0. Translation definitions for T 0 into T 1 are conservative definitions in Σ(T 0 ) ∪ Σ(T 1 ) of the form
where p i (x) is a relation symbol in Σ(T 0 ) and Φ(x) is a formula in Σ(T 1 ).
The key to this endeavour is the notion of logical synonymy: Definition 2 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 [10], 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.
Synonymy is a relationship between two ontologies; we can generalize this to a relationship among arbitrary finite sets of ontologies: Definition 3 (Adapted from [5]) A theory T is reducible to a set of theories T 1 , ..., T n iff 1. T faithfully interprets each theory T i , and 2. T 1 ∪ ... ∪ T n is synonymous with T .
The models of the reducible theory T can be constructed by amalgamating the models of the theories T 1 , ..., T n . We can thus provide a characterization of Mod(T ) up to isomorphism from the characterization of Mod(T i ) for each theory T i in the reduction.
The axioms of DOLCE are divided into a set of subtheories as shown in Figure 1. At the very bottom of the diagram is the DOLCE taxonomy subtheory, T dolce taxonomy , which consists of the categorization of the constructs found in DOLCE. The DOLCE Mereology and Time Mereology subtheories, T dolce mereology and T dolce time mereology , import the axioms of T dolce taxonomy , as denoted by the solid arrows in the figure . As well, T dolce mereology imports T dolce time mereology . We then see that the DOLCE Present subtheory, T dolce present , imports all of the axioms in T dolce time mereology , so T dolce taxonomy is included as well. Likewise, the DOLCE Dependence, Participation, and Temporary Parthood subtheories (denoted by T dolce dependence , T dolce participation , and T dolce temporary parthood , respectively) import T dolce present and all of the axioms contained therein. Finally, the DOLCE Constitution subtheory, T dolce constitution , imports all of the axioms in T dolce temporary parthood . Notice that there are four primary subtheories in DOLCE that are maximal with respect to importation, and which together constitute the entire set of axioms for DOLCE:
T dolce = T dolce constitution ∪ T dolce participation ∪ T dolce dependence ∪ T dolce mereology
The verification of T dolce mereology is a straightforward generalization of traditional mereology ontologies, and we will not cover it in this paper. To verify the remaining three pri-mary DOLCE subtheories, we map them with existing mathematical ontologies found in the Common Logic Ontology Repository (COLORE) 4 . Figure 2 illustrates the mappings between the DOLCE theories and COLORE theories. In the next section we will explore how this leads to the verification of T dolce .
In this section, we give an overview of the verification of T dolce . We open with an informal summary of the relevant mathematical ontologies that are required, and then consider the reductions of the subtheories of T dolce , namely, T dolce constitution , T dolce participation , and T dolce dependence .
A number of novel classes of mathematical structures have been axiomatized in order to adequately represent the models of DOLCE. Limited space does not allow us to provide all of the formal definitions for classes of mathematical structures; however, we can give a brief overview of the structures and their relationships to each other.
In our partial modularization of DOLCE, we utilized bipartite incidence structures found in mathematical theories of COLORE. Bipartite incidence structures are a generalization of two-dimensional plane geometries -there are two disjoint sets of points and lines, and the incidence relation in(x, y) specifies the set of points that are incident with a line. Tripartite incidence structures are a generalization of three-dimensional space geometries -in addition to points and lines, there exists another set of elements known as planes. The incidence relation applies over the sets of points and lines that are incident with a plane.
In our reduction of T dolce constitution , we utilized structures5 that arise from different ways of amalgamating mereologies and incidence structures.
A mereological geometry is the amalgamation of a bipartite incidence structure and a mereology that is specified on sets of collinear points (points that are all incident with the same line). Sets of collinear points need to satisfy axioms for a given mereology, and there may be a global mereology on a set of all points, regardless of collinearity. Mereological geometries are axiomatized by theories in the H mereological geometry Hierarchy 6 .
• ideal: collinear points form an ideal in the global classical extensional mereology (cem) mereology • cem: 'cem' refers to cem mereology, which is the global mereology on all points in this structure • wmg: collinear points form a weak mereology, wmg, which is a partial ordering In a mereological bundle, we find a generalization of the part(x, y) relation from mereology by introducing a ternary relation t part(x, y,t) that specifies a relativized parthood relation on sets of lines that are coincident with the same point. In mereological bundles, a quasiorder is specified on the set of lines that are incident with a point; a mereology is not specified on sets of intersecting lines due to the notion of temporary parthood. In the philosophical literature, the relation for temporary parthood is not considered to be antisymmetric, in contrast to the parthood relation in a mereology. Due to this, mereological bundles contain quasiorderings on sets of intersecting lines. Mereological bundles are axiomatized by theories in the H mereological bundle Hierarchy 7Mereological foliations are simply an amalgamation of mereological geometries and mereological bundles. A mereology is specified on each set of collinear points and mereological bundle is specified on each set of intersecting lines. Mereological foliations are axiomatized by theories in the H mereological f oliation Hierarchy8
The above classes of mathematical structures are amalgamations of incidence structures with mereologies. For the verification of T dolce participation , we generalized these ideas to the notions of incidence bundles and incidence foliations.
Incidence bundles extend tripartite incidence structures with an additional ternary relation that represents a triple of mutually incident points, lines, and planes. The name of this class of structures owes its origin to the similarity with the notion of fibre bundles from differential topology [7]. Incidence bundles are axiomatized by theories in the H incidence bundle Hierarchy 9 .
An incidence foliation is an amalgamation of a mereological geometry and an incidence bundle: a mereology is specified on each set of collinear points and an incidence bundle is specified on each set of coincident lines and planes. Incidence foliations are axiomatized by theories in the H incidence f oliation Hierarchy10 .
In addition to the mereological and incidence structures outlined above, we also utilize structures found in the subposet hierarchy11 , H subposet , in COLORE. Each ontology in this hierarchy is an extension of an ontology from the Mereology Hierarchy, H mereology , and an ontology from the Ordering Hierarchy, H ordering . The ontologies in this hierarchy form the basis for H subposet . The root ontology T subposet root is the union of T m mereology and T partial ordering , and is a conservative extension of each of these ontologies. Thus, each model of T subposet 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 in H subposet contain additional axioms that constrain how the mereology is related to the partial ordering. In models of T subposet , the mereology is a subordering of the partial ordering. T ideal strengthens this condition by requiring that the mereology is a subordering of the partial ordering which forms an ideal. In models of T chain antichain , elements that are ordered by the mereology are not comparable in the partial ordering.
All ontologies within H subposet combine one of the ontologies in the subposet hierarchy together with one of the ontologies in the mereology hierarchy and one of the ontologies in ordering hierarchy. We utilized the subposet bundle and subposet foliation structures constructed from models of theories H subposet in our reduction of DOLCE.
A subposet bundle is analogous to a mereological bundle: we find a generalization of the part(x, y) relation from mereology by introducing a ternary relation t part(x, y, z) that specifies a relativized parthood relation on sets of lines that are coincident with the same point. We also find a generalization of the leq(x, y) relation from the ordering theories introducing a ternary relation tleq(x, y, z) that specifies a relativized ordering relation on sets of lines that are coincident with the same point. Subposet bundles are axiomatized by theories in the H subposet bundle Hierarchy12 .
Subposet foliations are an amalgamation of mereological geometries and subposet bundles; they are axiomatized by theories in the H subposet f oliation Hierarchy13 .
T dolce constitution has three main subtheories. In the subtheory T dolce present , we have axioms that describe the existence of an endurant ED(x), perdurant PD(x), or a quality Q(x) during a time interval T (x).
Within the Temporary Parthood theory T dolce temporary parthood in DOLCE, the tP(x, y,t) relation only holds for endurants, so the verification tasks were broken down into three parts: a task to handle physical endurants PED(x), a task to handle nonphysical endurants NPED(x), and a task to handle both perdurants PD(x) and qualities Q(x). Collectively, PED(x) and NPED(x) make up endurants ED(x), but since they are disjoint constructs we were required to create two sets of translation definitions, ∆ 1 and ∆ 2 , to handle these endurant subcategories. The translation definitions for PD(x) and Q(x) are grouped together in ∆ 3 because the tP(x, y,t) does not involve either of these constructs.
Similar to the T dolce temporary parthood axioms, the theory of constitution T dolce constitution14 contains additional axioms that only apply to the physical endurants PED(x), nonphysical endurants NPED(x), and perdurants PD(x). The constitution axioms require the first two arguments to be of the same category; for example, only two non-physical endurants NPED(x) can constitute each other during a given time interval t. The remainder of the axioms show that constitution is irreflexive, transitive, enforces the existence of the two endurants or perdurants that are being constituted, constitution still holds for subintervals of a time interval, and that temporary parts of an endurant are also constituted.
The reduction of T dolce constitution uses theories about subposet foliations and mereological geometries: Theorem 1 T dolce constitution is synonymous with T ideal cem lower re f lect down f oliation ∪ T ideal cem downward m f oliation ∪T ideal cem wmg ∪ T ideal cem lower re f lect down f oliation
The theories in the reduction correspond to the subtheories of T dolce constitution that axiomatize constitution of physical endurants PED(x), non-physical endurants NPED(x), perdurants PD(x), and qualities Q(x), respectively.
We have seen that a fundamental ontological commitment of DOLCE is the distinction between enduring and perduring entities, where the fundamental difference between the two is related to their behaviour in time [9]. Endurants are wholly present at any time: they are observed and perceived as a complete concept, regardless of a given snapshot of time. Perdurants, on the other hand, extend in time by accumulating different temporal parts, so they are only partially present at any given point in time. In T dolce participation15 , endurants are involved in an occurrence, so the notion of participation is not considered parthood. Rather, participation is time-indexed in order to account for the varieties of participation in time, such as temporary participation and constant participation.
Intuitively, the mereological geometry in an incidence foliation corresponds to the subtheory of T dolce participation that axiomatizes the PRE(x,t) relation between perdurants or endurants (which are interpreted by lines) and time intervals (which are interpreted as points). This raises a challenge. On the one hand, we have the problem that in the incidence bundle, both endurants and perdurants can be interpreted by lines, yet one class must be interpreted by planes in the incidence foliation. On the other hand, there is no other distinction between these two classes. As a result, we need two separate incidence foliations for the verification.
In T ideal cem plane downward in f oliation , we interpret endurants as planes and perdurants as lines within the incidence bundle. In the mereological geometry, there is a classical extensional mereology on the set of points, while sets of collinear points form ideals within the mereology. Full details for the verification of T dolce participation can be found in [2].
Finally, DOLCE contains a rich formalization of the intuitions about ontological dependence between two entities [9], and it explicitly axiomatizes several different dependence relations. For example, an entity x is specifically dependent on another entity y iff, at any time t, the entity x cannot be present at time t unless the entity y is also present at time t. Furthermore, there are different dependence relations between entities in different classes within the DOLCE taxonomy, and this leads to seven different subtheories (see Table 1). The verification of these dependence theories requires tripartite incidence structures and ordered geometries:
Theorem 3 T mob apo dependence is synonymous with T plane proper dependence ∪ T ideal cem wmg . T tq pd dependence , T pq ped dependence , and T aq nped dependence are each synonymous with T plane mutual dependence ∪ T ideal cem wmg .
T f napo dependence , T sag apo dependence , and T naso sc dependence are each synonymous with T ideal cem wmg ∪ T atomic proper dependence .
In [8], the authors present a novel approach at establishing the consistency of DOLCE. They proposed a methodology that utilizes the HETS 16 to develop an architectural specification for DOLCE that is used to produce relative consistency proofs based on conservativity triangles. In HETS, an architectural specification is essentially a software specification that decomposes a large theory into smaller subtasks, which includes the construction of models for these small theories, proving the conservativity of theory extensions, and determining whether the constructed theories can be amalgamated together [8]. Relative consistency proofs are used by HETS to provide theory interpretations into another theory that is known or assumed to be consistent. HETS visualizes these relationships between smaller theories via development graphs by denoting the dependencies between the theories. The approach presented in [8] constructed a global model for DOLCE that is built from smaller models of subtheories together with amalgamability properties between such models. The authors hand-crafted an architectural specification of DOLCE which reflects the way models of the theory can be built, and utilized HETS to automatically verify the amalgamability conditions and produce a series of relative consistency proofs.
The authors of [8] note that the axioms in the dependence theory of DOLCE introduced complications in their first modularization attempt since subtle dependencies between parts of DOLCE's taxonomy were involved. Consequently, they restructured their architectural specification for DOLCE to utilize DOLCE's temporal mereology in a bottom-up manner. The end result consisted of thirty eight units within the architectural specification and eighteen amalgamations, allowing the generation of various finite models for DOLCE [8].
The reduction of a theory can also be used to decompose an ontology [5]. 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 T dolce -each theory in the reduction (see Theorem 1) is synonymous with a reductive module of T dolce constitution .
The verification of DOLCE led to a modularization that was strikingly different from the modularization that was used in the consistency proof in [8]. Rather than sets of axioms for relations such as constitution and temporary parthood, the reductive modules of DOLCE are subtheories for classes of elements -perdurants, physical endurants, nonphysical endurants, and qualities. We have already noted that a fundamental ontologi-cal commitment of DOLCE is the distinction between enduring and perduring entities, which are also referred to as continuants and occurrents, where the fundamental difference between the two is related to their behaviour in time [9]. It is interesting to discover that this distinction is also reflected in the modularity of the ontology itself.
The verification of the DOLCE subtheories is summarized in Figure 2. The resulting modularization is oriented around the distinction between endurants and perdurants; rather than divide the axioms into the T dolce temporary parthood and T dolce constitution subtheories, the modules correspond to constitution and temporary parthood for different classes of endurants and perdurants in the taxonomy. Several interesting observations about the modularization can be made. On the one hand, it is easy to see that the reductive modularization is quite different from the modularization of [8]. On the other hand, our modularization of DOLCE is coarser-grained than the modules presented in [8], in the sense that every (reductive) module in our modularization is a module of DOLCE, and every module in [8] is a module of the (reductive) modules we have presented in this work.