1. Introduction

Verification and Modularization of the DOLCE Upper Ontology

Carmen CHUI

Michael GRU¨ NINGER

0 0 Department of Mechanical and Industrial Engineering, University of Toronto , Ontario , Canada

M5S 3G8

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 (COLORE), and describe how the ontological commitments made by the authors of DOLCE have affected the resulting verification and reductive modularization.

upper ontologies ontology verification modularization DOLCE COLORE

1. Introduction

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 isomorphism3. 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 ], 1Corresponding Author: Carmen Chui; E-mail: cchui@mie.utoronto.ca. 2http://www.loa.istc.cnr.it/old/DOLCE.html 3This paper only gives an overview of the verification of DOLCE; all of the proofs for the theorems can be found in the full papers: http://stl.mie.utoronto.ca/publications/participation.pdf and http://stl.mie.utoronto.ca/publications/dolce-verification.pdf 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.

2. Ontology Verification

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 T0 be a theory with signature S(T0) and let T1 be a theory with signature

S(T1) such that S(T0) \ S(T1) = 0/ . Translation definitions for T0 into T1 are conservative definitions in S(T0) [ S(T1) of the form 8x pi(x)

F(x) where pi(x) is a relation symbol in S(T0) and F(x) is a formula in S(T1). The key to this endeavour is the notion of logical synonymy:

Definition 2 Two theories T1 and T2 are synonymous iff there exist two sets of translation

definitions D and P, respectively from T1 to T2 and from T2 to T1, such that T1 [ P is logically equivalent to T2 [ D.

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 T1; :::; Tn iff 1. T faithfully interprets each theory Ti, and 2. T1 [ ::: [ Tn is synonymous with T .

The models of the reducible theory T can be constructed by amalgamating the models of the theories T1; :::; Tn. We can thus provide a characterization of Mod(T ) up to isomorphism from the characterization of Mod(Ti) for each theory Ti in the reduction.

3. Axiomatization of DOLCE

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, Tdolce taxonomy, which consists of the categorization of the constructs found in DOLCE. The DOLCE Mereology and Time Mereology subtheories, Tdolce mereology and Tdolce time mereology, import the axioms of Tdolce taxonomy, as denoted by the solid arrows in the figure. As well, Tdolce mereology imports Tdolce time mereology. We then see that the DOLCE Present subtheory, Tdolce present , imports all of the axioms in Tdolce time mereology, so Tdolce taxonomy is included as well. Likewise, the DOLCE Dependence, Participation, and Temporary Parthood subtheories (denoted by Tdolce dependence, Tdolce participation, and Tdolce temporary parthood , respectively) import Tdolce present and all of the axioms contained therein. Finally, the DOLCE Constitution subtheory, Tdolce constitution, imports all of the axioms in Tdolce temporary parthood .

dolce constitution dolce temporary parthood

dolce participation dolce dependence

dolce present dolce mereology dolce time mereology

dolce taxonomy

DOLCE Hierarchy 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:

Definition 4

Tdolce = Tdolce constitution [ Tdolce participation [ Tdolce dependence [ Tdolce mereology The verification of Tdolce mereology is a straightforward generalization of traditional mereology ontologies, and we will not cover it in this paper. To verify the remaining three primary 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 Tdolce.

4. Verification of DOLCE Subtheories

In this section, we give an overview of the verification of Tdolce. We open with an informal summary of the relevant mathematical ontologies that are required, and then consider the reductions of the subtheories of Tdolce, namely, Tdolce constitution, Tdolce participation, and

Tdolce dependence. 4.1. Mathematical Ontologies used in the Reduction of DOLCE

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.

4.1.1. Usage of Bipartite and Tripartite Incidence Structures

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.

4.1.2. Mereological Geometries, Bundles & Foliations

In our reduction of Tdolce 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 Hmereological geometry Hierarchy6. 4http://colore.oor.net/ 5Due to the various combinations of incidence structures, the names of the theories in COLORE may appear confusing. Here we briefly outline the naming convention used to describe these incidence structure theories. Consider the theory Tideal cem wmg in COLORE. The name ideal cem wmg is broken down as follows: 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 An ideal is a set closed under the P(x; y) and sum(x; y; z) relations. For any two points, its sum is also in the set. 6http://colore.oor.net/mereological_geometry/

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 Hmereological bundle Hierarchy7

Mereological 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 Hmereological f oliation Hierarchy8

4.1.3. Incidence Bundles & Foliations

The above classes of mathematical structures are amalgamations of incidence structures with mereologies. For the verification of Tdolce 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

Hincidence bundle Hierarchy9.

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 Hincidence f oliation Hierarchy10.

4.1.4. Subposet Bundles & Foliations

In addition to the mereological and incidence structures outlined above, we also utilize structures found in the subposet hierarchy11, Hsubposet , in COLORE. Each ontology in this hierarchy is an extension of an ontology from the Mereology Hierarchy, Hmereology, and an ontology from the Ordering Hierarchy, Hordering. The ontologies in this hierarchy form the basis for Hsubposet . 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 in Hsubposet contain additional axioms that constrain how the mereology is related to the partial ordering. In models of Tsubposet , the mereology is a 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 7http://colore.oor.net/mereological_bundle/ 8http://colore.oor.net/mereological_foliation/ 9http://colore.oor.net/incidence_bundle/ 10http://colore.oor.net/incidence_foliation/ 11http://colore.oor.net/subposet/ Tchain antichain, elements that are ordered by the mereology are not comparable in the partial ordering.

All ontologies within Hsubposet 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 Hsubposet 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 Hsubposet bundle Hierarchy12.

Subposet foliations are an amalgamation of mereological geometries and subposet bundles; they are axiomatized by theories in the Hsubposet f oliation Hierarchy13.

4.2. Verification of Tdolce constitution

Tdolce constitution has three main subtheories. In the subtheory Tdolce 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 Tdolce 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, D1 and D2, to handle these endurant subcategories. The translation definitions for PD(x) and Q(x) are grouped together in D3 because the tP(x; y; t) does not involve either of these constructs.

Similar to the Tdolce temporary parthood axioms, the theory of constitution Tdolce constitution 14 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 Tdolce constitution uses theories about subposet foliations and mereological geometries:

Theorem 1 Tdolce constitution is synonymous with

12http://colore.oor.net/subposet_bundle/ 13http://colore.oor.net/subposet_foliation/ 14http://colore.oor.net/dolce_constitution/dolce_constitution.clif

Tideal cem lower re f lect down f oliation [ Tideal cem downward m f oliation [Tideal cem wmg [ Tideal cem lower re f lect down f oliation

The theories in the reduction correspond to the subtheories of Tdolce constitution that axiomatize constitution of physical endurants PED(x), non-physical endurants NPED(x), perdurants PD(x), and qualities Q(x), respectively.

4.3. Verification of Tdolce participation

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 Tdolce 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 Tdolce 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.

Theorem 2 Tdolce participation is synonymous with Tideal cem plane downward in f oliation [ Tideal cem line downward in f oliation

In Tideal 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 Tdolce participation can be found in [ 2 ].

4.4. Verification of Tdolce dependence

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).

15http://colore.oor.net/dolce_participation/dolce_participation.clif Dependent Class Mental Object (MOB) Temporal Quality (TQ) Physical Quality Abstract Quality (AQ) Feature Social Agent (SAG) Non Agentive Physical Object (NAPO)

Class Agentive Physical Object (APO) Physical Endurant (PED) Physical Endurant (PED) Non Physical Endurant (NPED) Non Agentive Physical Object (NAPO) Agentive Physical Object (APO) Society (SC)

Subtheory Tmob apo dependence Ttq pd dependence Tpq ped dependence Taq nped dependence Tf napo dependence Tsag apo dependence Tnaso sc dependence

The verification of these dependence theories requires tripartite incidence structures and ordered geometries:

Theorem 3 Tmob apo dependence is synonymous with Tplane proper dependence [ Tideal cem wmg. Ttq pd dependence, Tpq ped dependence, and Taq nped dependence are each synonymous with Tplane mutual dependence [ Tideal cem wmg. Tf napo dependence, Tsag apo dependence, and Tnaso sc dependence are each synonymous with Tideal cem wmg [ Tatomic proper dependence. 5. Modularization of DOLCE 5.1. Consistency of DOLCE

In [ 8 ], the authors present a novel approach at establishing the consistency of DOLCE. They proposed a methodology that utilizes the HETS16 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

dolce_constitution U dolce_temporary_parthood

U dolce_present U dolce_time_mereology dolce_participation

U dolce_present U dolce_time_mereology ideal_cem_downward_m_foliation

U ideal_cem_cemmg plane_downward_in_foliation

U ideal_cem_cemmg MOB_APO_dependence