=Paper=
{{Paper
|id=Vol-2050/foust-paper1
|storemode=property
|title=Verification and Modularization of the DOLCE Upper Ontology
|pdfUrl=https://ceur-ws.org/Vol-2050/FOUST_paper_1.pdf
|volume=Vol-2050
|authors=Carmen Chui,Michael Gruninger
|dblpUrl=https://dblp.org/rec/conf/jowo/ChuiG17
}}
==Verification and Modularization of the DOLCE Upper Ontology
==
https://ceur-ws.org/Vol-2050/FOUST_paper_1.pdf
Verification and Modularization of the
DOLCE Upper Ontology
Carmen CHUI a,1 , Michael GRÜNINGER a
a Department of Mechanical and Industrial Engineering, University of Toronto, Ontario,
Canada M5S 3G8
Abstract. This paper outlines the reductive modularization and verification of the
Descriptive Ontology for Linguistic and Cognitive Engineering (DOLCE). The on-
tology makes distinctions between enduring and perduring entities which is re-
flected in the resulting reductive modules, in contrast to previous work done to gen-
erate 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.
Keywords. upper ontologies, ontology verification, modularization, DOLCE,
COLORE
1. Introduction
Foundational ontologies, also called upper ontologies, characterize the semantics of gen-
eral concepts that underlay every knowledge representation enterprise. Since founda-
tional ontologies are expected to be broadly reused, verifying that they do not have un-
intended 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 char-
acterize any intended ones which might be missing. In this paper, we apply the defini-
tion of ontology verification based on representation theorems that was introduced in [4],
1 Corresponding Author: Carmen Chui; E-mail: cchui@mie.utoronto.ca.
2 http://www.loa.istc.cnr.it/old/DOLCE.html
3 This 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 par-
ticularly 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 on-
tology 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 on-
tology’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 Σ(T0 ) and let T1 be a theory with signature
Σ(T1 ) such that Σ(T0 ) ∩ Σ(T1 ) = 0.
/ Translation definitions for T0 into T1 are conservative
definitions 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 Σ(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 ∆ and Π, respectively from T1 to T2 and from T2 to T1 , such that T1 ∪ Π is
logically equivalent to T2 ∪ ∆.
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 rela-
tionship 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 isomor-
phism 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
Figure 1. Relationships between DOLCE modules. Solid arrows denote conservative extensions, dashed ar-
rows denote non-conservative extensions, and dashed boxes indicate individual hierarchies.
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 mere-
ology 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 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. Mereo-
logical geometries are axiomatized by theories in the Hmereological geometry Hierarchy6 .
4 http://colore.oor.net/
5 Due 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.
6 http://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 part-
hood 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 mere-
ology is not specified on sets of intersecting lines due to the notion of temporary part-
hood. In the philosophical literature, the relation for temporary parthood is not consid-
ered 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 mere-
ological 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 bun-
dles 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 inci-
dence 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 mere-
ology is related to the partial ordering. In models of Tsubposet , the mereology is a sub-
ordering 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
7 http://colore.oor.net/mereological_bundle/
8 http://colore.oor.net/mereological_foliation/
9 http://colore.oor.net/incidence_bundle/
10 http://colore.oor.net/incidence_foliation/
11 http://colore.oor.net/subposet/
Tchain antichain , elements that are ordered by the mereology are not comparable in the par-
tial ordering.
All ontologies within Hsubposet combine one of the ontologies in the subposet hi-
erarchy 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 non-
physical 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 Tdolce temporary parthood axioms, the theory of constitution Tdolce constitution
14 contains additional axioms that only apply to the physical endurants PED(x), non-
physical 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 re-
mainder of the axioms show that constitution is irreflexive, transitive, enforces the ex-
istence 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 mereo-
logical geometries:
Theorem 1 Tdolce constitution is synonymous with
12 http://colore.oor.net/subposet_bundle/
13 http://colore.oor.net/subposet_foliation/
14 http://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 ax-
iomatize 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 participation 15 ,
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 ex-
tensional 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 depen-
dence 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).
15 http://colore.oor.net/dolce_participation/dolce_participation.clif
Dependent Class Class Subtheory
Mental Object (MOB) Agentive Physical Object (APO) Tmob apo dependence
Temporal Quality (TQ) Physical Endurant (PED) Ttq pd dependence
Physical Quality Physical Endurant (PED) Tpq ped dependence
Abstract Quality (AQ) Non Physical Endurant (NPED) Taq nped dependence
Feature Non Agentive Physical Object (NAPO) T f napo dependence
Social Agent (SAG) Agentive Physical Object (APO) Tsag apo dependence
Non Agentive Physical Object (NAPO) Society (SC) Tnaso sc dependence
Table 1. Dependence subtheories in DOLCE.
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 .
T f 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 spec-
ification for DOLCE that is used to produce relative consistency proofs based on conser-
vativity triangles. In HETS, an architectural specification is essentially a software specifi-
cation that decomposes a large theory into smaller subtasks, which includes the construc-
tion of models for these small theories, proving the conservativity of theory extensions,
and determining whether the constructed theories can be amalgamated together [8]. Rel-
ative 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 be-
tween 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 automat-
ically 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 in-
troduced complications in their first modularization attempt since subtle dependencies
between parts of DOLCE’s taxonomy were involved. Consequently, they restructured
16 http://hets.eu/.
dolce_constitution
U dolce_temporary_parthood ideal_cem_lower_reflect_down_foliation
U dolce_present U ideal_cem_downward_m_foliation
U dolce_time_mereology
dolce_temporary_parthood
ideal_cem_downward_m_foliation
U dolce_present
U ideal_cem_cemmg
U dolce_time_mereology
dolce_participation
plane_downward_in_foliation
U dolce_present
U ideal_cem_cemmg
U dolce_time_mereology
MOB_APO_dependence
plane_proper_dependence
U dolce_present
U ideal_cem_cemmg
U dolce_time_mereology
TQ_PD_dependence
U dolce_present
U dolce_time_mereology
PQ_PED_dependence plane_mutual_dependence
U dolce_present U ideal_cem_cemmg
U dolce_time_mereology
AQ_NPED_dependence
U dolce_present
U dolce_time_mereology
F_NAPO_dependence
atomic_plane
U dolce_present
_proper_dependence
U dolce_time_mereology
SAG_APO_dependence
U dolce_present
U dolce_time_mereology
NASO_SC_dependence
U dolce_present
U dolce_time_mereology
dolce_present
ideal_cem_cemmg
U dolce_time_mereology
dolce_time_mereology cem_mereology
Figure 2. DOLCE subtheories and the mathematical ontologies from COLORE that are used in the verifica-
tion. Solid arrows denote conservative extensions and solid lines indicate synonymy.
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 architec-
tural specification and eighteen amalgamations, allowing the generation of various finite
models for DOLCE [8].
5.2. Reductive Modularization of DOLCE
The reduction of a theory can also be used to decompose an ontology [5]. If T is reducible
to S1 , ..., Sn , then there exist subtheories T1 , ..., Tn such that each Ti is synonymous with
Si . Since T is a conservative extension of each Ti , we refer to the subtheories as the
reductive modules of T . We can therefore use the results from verification to modularize
Tdolce – each theory in the reduction (see Theorem 1) is synonymous with a reductive
module of Tdolce 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 ax-
ioms for relations such as constitution and temporary parthood, the reductive modules of
DOLCE are subtheories for classes of elements – perdurants, physical endurants, non-
physical 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 differ-
ence 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.
6. Discussion and Summary
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 Tdolce temporary parthood and Tdolce constitution subtheo-
ries, 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 modu-
larization is quite different from the modularization of [8]. On the other hand, our mod-
ularization 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.
References
[1] Stefano Borgo and Claudio Masolo. Foundational Choices in DOLCE. In Steffen Staab and Ruder
Studer, editors, Handbook on Ontologies. Springer, second edition, 2009.
[2] Carmen Chui and Michael Grüninger. Mathematical Foundations for Participation Ontologies. In For-
mal Ontology in Information Systems - Proceedings of the Eighth International Conference, FOIS 2014,
September, 22-25, 2014, Rio de Janeiro, Brazil, pages 105–118, 2014.
[3] Aldo Gangemi, Nicola Guarino, Claudio Masolo, Alessandro Oltramari, and Luc Schneider. Sweetening
ontologies with DOLCE. In Knowledge Engineering and Knowledge Management. Ontologies and
the Semantic Web, 13th International Conference, EKAW 2002, Siguenza, Spain, October 1-4, 2002,
Proceedings, pages 166–181, 2002.
[4] Michael Grüninger, Torsten Hahmann, Ali Hashemi, and Darren Ong. Ontology verification with repos-
itories. In Formal Ontology in Information Systems, Proceedings of the Sixth International Conference,
FOIS 2010, Toronto, Canada, May 11-14, 2010, pages 317–330, 2010.
[5] Michael Grüninger, Torsten Hahmann, Ali Hashemi, Darren Ong, and Atalay Özgövde. Modular first-
order ontologies via repositories. Applied Ontology, 7(2):169–209, 2012.
[6] Torsten Hahmann and Boyan Brodaric. The void in hydro ontology. In Formal Ontology in Information
Systems - Proceedings of the Seventh International Conference, FOIS 2012, Gray, Austra, July 24-27,
2012, pages 45–58, 2012.
[7] Dale Husemöller. Fibre Bundles. Graduate Texts in Mathematics. Springer-Verlag New York, 1994.
[8] Oliver Kutz and Till Mossakowski. A Modular Consistency Proof for DOLCE. In Proceedings of the
Twenty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2011, San Francisco, California, USA,
August 7-11, 2011, 2011.
[9] Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari. Wonder-
Web Deliverable D18 Ontology Library (Final). Technical report, IST Project 2001-33052 WonderWeb:
Ontology Infrastructure for the Semantic Web, 2003.
[10] D. Pearce and A. Valverde. Synonymous theories and knowledge representations in answer set program-
ming. Journal of Computer and System Sciences, 78(1):86 – 104, 2012. JCSS Knowledge Representa-
tion and Reasoning.