=Paper=
{{Paper
|id=Vol-1660/womocoe-paper2
|storemode=property
|title=Anti-Modules
|pdfUrl=https://ceur-ws.org/Vol-1660/womocoe-paper2.pdf
|volume=Vol-1660
|authors=Bahar Aameri,Michael Grüninger,Carmen Chui
|dblpUrl=https://dblp.org/rec/conf/fois/AameriGC16
}}
==Anti-Modules==
https://ceur-ws.org/Vol-1660/womocoe-paper2.pdf
Anti-Modules
Bahar AAMERI a , Michael GRÜNINGER b Carmen CHUI b
a Department of Computer Science, University of Toronto, Ontario, Canada M5S 3G8
b Department of Mechanical and Industrial Engineering, University of Toronto,
Ontario, Canada M5S 3G8
Abstract. Modules of a logical theory are subtheories that are conservatively ex-
tended by the theory. There are, on the other hand, subtheories that are not con-
tained in any proper module of the theory, which we refer to as the residue of the
theory. In this paper, we characterize properties of residues and explore their role in
ontology modularization. We discuss that there are ontological commitments that
cannot be captured by modules of a theory and must be axiomatized by residues.
We observe that sentences in the residue of a theory eliminate some possible com-
binations of models of modules of the theory. In that sense, ontological commit-
ments that are captured by residues basically determine how arbitrary models of
modules must be combined.
Keywords. Ontology Modularization, Residues, Ontology Composition, Ontology
Decomposition
1. Introduction
The modularization of an ontology is a indispensable technique in the analysis of an
ontology. Modules tell us about the organization of an ontology through the relationships
between its logical subtheories. Modules also constrain how we can extend an ontology;
one of the original motivations for modularity was the safety – how can we extend an
ontology and still preserve the intended interpretations of the terminology in the original
ontology? Nevertheless, modules do not tell us the whole story.
In general, an ontology is not equivalent to the union of its modules; there will be
axioms that are not contained in any module of the ontology. Since almost all of the
research within applied ontology has focused on the identification and extraction of the
modules of an ontology, it has neglected to investigate such sentences which cannot be
contained in any module.
In this paper, we formally define the notion of residue of a theory1 as the set of sen-
tences which are not contained in any module, and show how the residue gives us insight
into ontology design and evaluation. After introducing the notion of residue in Section 3,
and proving some basic properties, in Section 4 we explore the role that residues play in
the decomposition of an ontology that is the result of ontology verification. In Section 5,
we see the role of residues in understanding how ontologies can be composed as modules
of larger ontologies.
1 In this paper, we use the words “ontology” and “theory” interchangeably. We consider a theory to be a set
of first-order sentences closed under logical entailment, and a subtheory to be a theory which is contained by
another theory.
2. Relationships Among Ontologies
We first provide a short review of the relationships between ontologies that will be nec-
essary for introducing the notion of the residue of a theory.2
Definition 1 Let T1 , T2 be two first-order theories such that S(T1 ) ✓ S(T2 ).
T2 is an extension of T1 if and only if for any sentence F 2 L (T1 ),
T1 |= F ) T2 |= F.
T2 is a conservative extension of T1 if and only if for any sentence F 2 L (T1 ),
T1 |= F , T2 |= F.
Non-conservative and conservative extensions are generalized to theories with dif-
ferent signatures through the notions of non-faithful and faithful interpretations. We
adopt the definitions of these notions from [2]:
Definition 2 An interpretation p of a signature S1 into a theory T2 is a function on the
set of symbols in S1 such that
1. p assigns to 8 a formula p8 of L (T2 ) in which at most the variable v1 occurs
free, and
T2 |= (9v1 ) p8
2. p assigns to each n-place predicate symbol P a formula pP of L (T2 ) in which at
most n variables occur free.
3. p assigns to each n-place function symbol f a formula p f of L (T2 ) in which at
most the variables v1 , ..., vn , vn+1 occur free, and
T2 |= (8v1 , ..., vn ) p8 (v1 ) ^ ... ^ p8 (vn )
(9x)(p8 (x) ^ ((8vn+1 )(p f (v1 , ..., vn+1 ) ⌘ (vn+1 = x))))
Let T1 be a theory. An interpretation p of S(T1 ) into T2 is an interpretation of T1 in T2 if
and only if for all sentences F, F1 , F2 2 L (T1 ),
• if F is an atomic sentence with predicate symbol P, then p(F) = pP ;
• p(¬F) = ¬p(F);
• p(F1 ^ F2 ) = p(F1 ) ^ p(F2 );
• p(F1 _ F2 ) = p(F1 ) _ p(F2 );
• p(F1 F2 ) = p(F1 ) p(F2 );
• p(9x F) = (9x) p8 (x) ^ p(F);
• p(8x F) = (8x) p8 (x) p(F);
2 For every theory T , S(T ) denotes the signature of T , which is the set of all the constant, function, and
relation symbols used in T , L (T ) denotes the language of T , which is the set of all first-order formulae
generated by symbols in S(T ), and Mod(T ) denotes the class of all models of T .
• For any sentence F 2 L (T1 ),
T1 |= F ) T2 |= p(F).
An interpretation p of a theory T1 into a theory T2 is faithful iff for any sentence F 2
L (T1 ),
T1 6|= F ) T2 6|= p(F).
If an (faithful) interpretation from T1 into T2 exists, we say that T1 is (faithfully)
interpretable in T2 , or T2 (faithfully) interprets T1 . Interpretation preserves theorems of
the original theory, while faithful interpretation preserves decidability and satisfiability.
An interpretation of T1 into T2 defines symbols of T1 in terms of the language of
T2 . This indicates that relative interpretations are related to the notion of definitional
extension:
Definition 3 (adopted from [7]) Let T be a theory with signature S(T ).
T 0 is a definitional extension of T if and only if there exists a set of sentences D such that
1. for every predicate symbol P 2 S(T 0 ) \ S(T ), D includes a sentence of the form
(8x) P(x) ⌘ F(x),
where F is a formula in L (T );
2. T [ D is a conservative extension of T , and is logically equivalent with T 0 .
Interpretations between theories can be axiomatized in terms of translation defini-
tions between the theories:
Definition 4 D is a set of translation definitions for T1 into T2 if and only if T2 [ D is a
definitional extension of T2 and
T2 [ D |= T1 .
More formally, the results in [5] show that T1 is interpretable in T2 iff there exists a
set of translation definitions D for T1 into T2 such that T2 [ D entails T1 .
Finally, just as interpretations can be considered to be a generalization of extensions
to theories with disjoint signatures, the notion of logical synonymy generalizes the notion
of logical equivalence.
Definition 5 (adopted from [7]) Two ontologies T1 and T2 are logically synonymous if
and only if there exists an ontology T3 with the signature S(T1 ) [ S(T2 ) that is a defini-
tional extension of T1 and T2 .
If T1 and T2 are logically synonymous, then there exists a set of translation defini-
tions D for T1 into T2 , and a set of translation definitions P for T2 into T1 such that T2 [ D
is logically equivalent with T1 [ P.
3. What is a Residue?
3.1. Modules and Residues
We consider a module of a theory T to be a subtheory of T , and adopt the following
definition from [4].
Definition 6 T1 is a module of T2 if and only if T2 is a conservative extension of T1 .
Note that this is more general than the notion of module used in work such as [11]
and [8], in which a module is required to be a subset of the axioms in T . We believe that
it is a natural generalization of the notion of modularity because it is more robust with
respect to different possible logically equivalent axiomatizations of a theory.
We are not interested in finding a module of a theory, but rather in understanding
how a theory is related to sets of its modules.
Definition 7 A theory T is perfectly modularized into a set of proper modules T1 , ..., Tn
iff
T = T1 [ ... [ Tn
Many theories, however, cannot be perfectly modularized, that is, there are sentences
in the theory which are not contained in any proper module of the theory. We will refer
to the set of all such sentences as the residue of the theory, since it is the set of sentences
“leftover” after all of the modules have been determined:
Definition 8 Let T1 , ..., Tn be all proper modules of a theory T .
The residue R of T is the subtheory of T that is logically equivalent to
T \ (T1 [ ... [ Tn ).
Thus, a theory has a nontrivial residue iff it is not perfectly modularized.
Example: Let T be the theory3 with axioms {(9x) A(x), (9x) B(x), (8x) A(x) _ B(x)}.
T has two modules {(9x) A(x)}, {(9x) B(x)}.
The residue of T is {(8x) A(x) _ B(x)}. ⇤
Example: Consider the ontology Tdolce present 4 which is a subtheory of the DOLCE On-
tology that captures intuitions about how objects can be present at different points
in time. One module is equivalent to Tdolce time mereology 5 (which axiomatizes the
mereology on temporal regions); the other module consists of the axioms:
(8x) (ED(x) _ PD(x) _ Q(x)) (9t) PRE(x,t),
(8x,t) PRE(x,t) T (t).
3 Thank you to one of the reviewers, who suggested this example.
4 colore.oor.net/dolce_present/dolce_present.clif
5 colore.oor.net/dolce_time_mereology/dolce_time_mereology.clif
In addition, there are two axioms which are not contained in any module of
Tdolce present :
(8x,t,t1 ) PRE(x,t) ^ P(t1 ,t) PRE(x,t1 ),
(8x,t,t1 ,t2 ) PRE(x,t1 ) ^ PRE(x,t2 ) ^ SUM(t,t1 ,t2 ) PRE(x,t).
and these axioms form the residue for Tdolce present . Note that the signature of this
subset of axioms is the union of the signature of the two modules. ⇤
Example: Consider the ontology Twog 6 that plays a role in the verification of OWL-Time
[3].
One module is equivalent to the theory Tpartial bipartite 7 and the other module is
equivalent to the theory Tbetweenness 8 . The two sentences
(8x, y, z, w, l) in(x, l) ^ in(y, l) ^ in(z, l) ^ in(w, l)
^ between(x, y, z) ^ (y 6= z) ^ between(y, z, w) between(x, y, w),
(8x, y, z, w, l) in(x, l) ^ in(y, l) ^ in(z, l) ^ in(w, l)
^ between(x, y, w) ^ between(y, z, w) between(x, y, z)
are not contained in any module, and hence form the residue for Twog . ⇤
Example: There exist theories which have no modules, and hence are equivalent to their
residue.
The theories of partial orderings, semilinear orderings, and linear orderings are all
of the signature let, and no subtheory of these theories is conservatively extended
by the theory. ⇤
It is easy to see that a theory is a non-conservative extension of any subtheory that
contains its residue. Furthermore, if T has a residue R, then R is unique, up to logical
equivalence, since the set of all modules of T is uniquely determined. The following
theorem characterizes sentences in the residue of a theory:
Theorem 1 If R be the residue of a theory T , then S(R) = S(T ).
Proof: Let R be the residue of T . By definition, R is a subtheory of T , so S(R) ✓ S(T ).
Suppose, for a contradiction, that S(R) 6= S(T ). Then S(R) must be a proper subset
of S(T ). Since S(R) ⇢ S(T ), there must be a module T 0 of T which contains sentences
with the signature S(R). Since T 0 is a module of T , T has to be a conservative extension
of T 0 . This means that any sentence in T \ T 0 extends the signature of T 0 (otherwise T
would be a non-conservative extension of T 0 ). Thus, R must be included in T 0 , which is
a contradiction. ⇤
The above theorem shows that sentences in the residue of a theory specify how the
modules of the theory are composed; we will explore this in more detail in Section 5.
6 colore.oor.net/ordered_geometry/wog.clif
7 colore.oor.net/bipartite_incidence/partial_bipartite
8 colore.oor.net/betweenness/betweenness.clif
3.2. Residues and Strong Reducibility
The notion of reducibility presented in [5] uses the metalogical relationships among on-
tologies to modularize an ontology.
Definition 9 A theory T is strongly reducible to a set of theories S1 , ..., Sn iff
1. T faithfully interprets each theory Si ;
2. T is synonymous with S1 [ ... [ Sn .
If a theory T is strongly reducible to theories S1 , ..., Sn , then S1 , ..., Sn is called a
strong reduction of T .
Example: Consider the theory Tend points 9 of time endpoints which relates the notion of
linear time points with the notion of time intervals by defining the functions begi-
nof, endof, and between. begino f (i), endo f (i) indicate the begin and the end point
of an interval i respectively, while between(p, q) denotes the interval between time
points p and q. The theory includes a binary relation be f ore over time points which
is transitive and irreflexive.
Tend points is strongly reducible to the theory Tlinear ordering 10 of linear ordering and
the theory Tstrict graphical 11 of strict graphical incidence structures.
A strict graphical incidence structure [6] is a tuple G = hX,Y, ini such that
1. X and Y are disjoint sets, and
in ✓ (X ⇥Y ) [ (Y ⇥ X) [ (X ⇥ X) [ (Y ⇥Y ).
Two elements of G that are related by in are called incident;
2. all elements of Y are incident with exactly two elements of X, and for each pair
p, q 2 X there exists a unique element in Y that is incident with both p and q.
The reductive modules of Tend points are the subtheories which are logically synony-
mous with Tlinear ordering and Tstrict graphical . ⇤
Lemma 1 If T has an empty residue, then T is strongly reducible.
Proof: Let T1 , ..., Tn be all modules of a theory T , and suppose T has empty residue.
Then T is logically equivalent to T1 [ ... [ Tn , and consequently is synonymous with
T1 [ ... [ Tn . Moreover, T faithfully interpret each Ti , 1 j n, since T is a conservative
extension of Ti . Consequently, T is strongly reducible to T1 , ..., Tn . ⇤
Thus, any theory which is not strongly reducible will have a nonempty residue;
however, there do exist strongly reducible theories with nonempty residues. For example,
although Tend points is reducible, it has a nonempty residue. The following sentence, for
example, is not entailed by any module of Tend points :
(8i) timeinterval(i) be f ore(begino f (i), endo f (i)). (1)
9 colore.oor.net/combined_time/endpoints.clif
10 colore.oor.net/orderings/linear_ordering.clif
11 colore.oor.net/bipartite_incidence/strict_graphical.clif
This observation is rather counter-intuitive as it seems that if a strong reduction of
a theory exists, then each theory in the reduction should correspond with a module of
the theory. The following theorem shows that this is indeed the case. However, later on
in Theorem 3, we will show that residues are not preserved by reductions. Therefore,
having a strong reduction does not necessarily imply that a perfect modularization for a
theory exists.
Theorem 2 (from [4]) Let S1 , ..., Sn be a strong reduction of a theory T .
There exist theories T1 , ..., Tn such that
1. Ti is synonymous with Si .
2. Ti is a module of T , for 1 i n;
If S1 , ..., Sn is a strong reduction of T and Ti is a module of T which is synonymous
with a theory in the reduction, then Ti is called a reductive module of T .
It is easy to see that not all modules of a theory are reductive modules. For example,
neither Tdolce present nor Twog have reductive modules since neither of them is reducible.
Moreover, the following theorem proves our earlier observation that residues are not
preserved by strong reducibility:
Theorem 3 Let S1 , ..., Sn be a strong reduction of a theory T , and D be a set of translation
definitions from T into S1 [ ... [ Sn .
Let R be the residue of T . Then D |= R.
Proof: Suppose S1 , ..., Sn is a strong reduction of T . Then T and S1 [ ... [ Sn are
synonymous. There exist sets of translation definitions P and D such that T [ P and
S1 [ ... [ Sn [ D are logically equivalent. Hence,
S1 [ ... [ Sn [ D |= R.
On the other hand, by Theorem 2, T has a reductive modularization T1 , ..., Tn such
that Ti and Si are synonymous, for 1 i n. That is, for each Ti and Si , 1 i n, there
exist translation definitions Pi and Di such that Ti [Pi and Si [Di are logically equivalent,
and Pi ⇢ P and Di ⇢ D. Then we have (⌘ denotes logical equivalence)
T1 [ P1 [ ... [ Tn [ Pn ⌘ S1 [ D1 [ ... [ Sn [ Dn .
Since R is disjoint from T1 , ..., Tn , we can say that
S1 [ D1 [ ... [ Sn [ Dn 6|= R.
Thus, D must entail R. ⇤
Consider again Tend points ; using an automated theorem prover it can be verified
that the following sentences are translation definitions from Tend points to Tlinear ordering [
Tstrict graphical :
D: (8x) timepoint(x) ⌘ point(x).
(8x) timeinterval(x) ⌘ line(x).
(8x, y) (begino f (y) = x) ⌘
(in(x, y) ^ point(x) ^ (x 6= y) ^ (8z) point(z) ^ in(z, y)) leq(x, z).
(8x, y) (endo f (y) = x) ⌘
(in(x, y) ^ point(x) ^ (x 6= y) ^ (8z) point(z) ^ in(z, y)) leq(z, x).
(8x, y) be f ore(x, y) ⌘ leq(x, y).
(8x, y, z) (z = between(x, y)) ⌘ (point(x) ^ point(y) ^ line(z) ^ in(x, z) ^ in(y, z)).
It can be verified that the residue of Tend points (including sentence (1)) are entailed by D.
3.3. Residues and Weak Reducibility
Reducibility places strong conditions on the relationship between a theory and its mod-
ules. Yet, we have already seen several examples of theories which are not reducible and
still can be decomposed into modules. In order to capture this larger class of theories, we
introduce the following:
Definition 10 A theory T is weakly reducible to the theories S1 , ..., Sn iff
1. T faithfully interprets each theory Si , and
2. S1 [ ... [ Sn is synonymous with a subtheory T 0 of T which has the same signature
as T (that is, S(T 0 ) = S(T ).
It turns out that there are many theories which are weakly reducible.
Example: The ontology Tperiod , proposed by van Benthem in [10], specifies the weakest
ontology that is satisfied by time periods. The signature of the ontology consists of
two primitive relations, precedence and inclusion, and two defined relations, glb
and overlaps. According to the ontology, precedence is a transitive and irreflexive
relation which induces a strict partial ordering over elements of the domain, while
inclusion relation is transitive, reflexive, and antisymmetric and induces a partial
ordering over elements. The ontology further includes axioms which specify the
interplay between the precedence and inclusion relations, and guarantee the exis-
tence of greatest lower bounds between overlapping intervals. It can be shown that
Tperiods is weakly reducible to Tprod mereology and Tpartial ordering . ⇤
As we saw with reducibility, the notion of weak reducibility also leads to the identi-
fication of a class of modules for a theory:
Theorem 4 Let S1 , ..., Sn be a weak reduction of a theory T .
There exist theories T1 , ..., Tn such that
1. Ti is synonymous with Si ;
2. Ti is a module of T , for 1 i n.
If S1 , ..., Sn is a weak reduction of T , and Ti is a module of T which is synonymous
with a theory in the weak reduction, then Ti is called a weak reductive module of T .
If we look closely at the definition of weak reducibility, we can see that the sentences
in T \ T 0 are not synonymous with any sentences in any of the Si theories. Thus, the
sentences in T \ T 0 are also in the residue of T . Further, we can show that the residue of
T 0 is included in the residue of T .
Theorem 5 Let S1 , ..., Sn be a weak reduction of a theory T and T 0 be the subtheory of
T with S(T 0 ) = S(T ) which is synonymous with S1 [ ... [ Sn . 12
Let R0 and R be residues of T 0 and T , respectively. Then R0 ✓ R.
Proof: By definition, S(T 0 ) = S(T ). Also, by Theorem 1, S(T 0 ) = S(R0 ) and S(T ) =
S(R). Therefore, S(R0 ) = S(T ) and S(R0 ) = S(R).
Now suppose F 2 R0 . Then S(F) = S(T 0 ) = S(T ) (otherwise T 0 would be a non-
conservative extension of its module with the signature S(F), which is a contradiction
with the definition of modules). Then F cannot be in any module of T since T is a
non-conservative extension of any theory that contains F. Thus, F has to be in R. ⇤
For another perspective of the role that residues play in weakly reducible theories,
we can take a closer look at the relationship between models of the theory and the mod-
els of its weak reductive modules. Consider, for example, a model M of Tperiod . The
reduct of M to the signature inclusion is a model of the weak reductive module that is
synonymous with Tprod mereology , while the reduct of M to the signature precedence is a
model of the weak reductive module that is synonymous with Tpartial ordering . However,
we cannot amalgamate arbitrary models of these modules to construct a model of Tperiod ;
any such amalgamation must also satisfy the axioms in the residue. We can therefore see
that the residue eliminates some of the possible amalgamations of models of the weak
reductive modules.
4. Residues and Ontology Decomposition
Given the relationship between reducibility, weak reducibility, and residues, an obvious
question is how residues can be found through the reduction of a theory. This effectively
provides a decomposition of a theory into the residue and a set of reductive and weak
reductive modules. In this section, we use the reduction of a subtheory of the DOLCE
Ontology, and the resulting modularization, as a case study to illustrate the role that
residues play in the decomposition of an ontology.
The residue often determines whether or not a particular module is a reductive or a
weak reductive module, and such a modularization can be strikingly different from other
approaches to modularization. For example, The work in [9] used a modularization of the
DOLCE Ontology to prove the consistency of the ontology. This modularization can be
seen in Figure 1. On the other hand, the verification of the DOLCE Ontology presented
in [1] led to a set of reductive modules (and no residue for the ontology as a whole), yet
the reductive modules were organized around the ontological categories of endurants and
perdurants.
12 Note that by Definition 10, if T is weakly reducible, which is the case in this theorem, then T 0 exists.
Figure 1. Modularization of DOLCE. Ovals denote the modules found in [9].
ideal cem lower reflect down foliation [ ideal cem lower reflect down foliation [ ideal cem downward foliation [ ideal cem wmg ⌘ dolce constitution
ideal cem downward m foliation [ ideal cem downward m foliation [ ideal cem wmg [ ideal cem wmg ⌘ dolce temporary parthood
Non-Physical Endurant Physical Endurant
N P ED(x) P ED(x)
ideal cem wmg [ ideal cem wmg [ ideal cem wmg ⌘ dolce present
Endurants Perdurants Qualities
ED(x) P D(x) Q(x)
Figure 2. Modularization of DOLCE from [1]. Vertical sets of theories are reductive modules, with each theory
in the set being a weak reductive module. Horizontal sets correspond to the modules found in [9].
Looking more closely at these reductive modules, we can see that they are them-
selves weakly reducible. Effectively, the residues of each of these subtheories prevented
a further decomposition into smaller reductive modules. On the other hand, we can see
that the combination of the weak reductive modules of the reductive modules does lead
to an organization that is more aligned with that in Figure 1.
filter ideal
upper_set lower_set
subposet
lower_reverse lower_preserve chain_antichain upper_preserve upper_reverse
subposet_root
mereology partial_ordering
Figure 3. The hierarchy of ontologies obtained by composing mereologies and theories of partial orderings.
Dashed lines denote non-conservative extension and solid lines denote conservative extension.
5. Residues and Ontology Composition
So far, we have considered the role of residues in ontology decomposition. In this section
we explore the role of residues in ontology construction and composition.
A common practice in ontology design is to identify existing ontologies that satisfy
parts of the ontological commitments and requirements, and reuse them as building mod-
ules of the new ontology. However, often there are ontological commitments that cannot
be captured by the modules alone, and residues are needed to properly axiomatize such
commitments.
To illustrate the role of residues in ontology composition, we use some of the on-
tologies in the subposet hierarchy. 13 The subposet hierarchy is a collection of mathe-
matical ontologies which are developed for verification of spacial an temporal ontolo-
gies. The weakest ontology in this hierarchy is constructed by taking the weakest mere-
ology and the weakest axiomatization of orderings. Other ontologies in the hierarchy are
constructed by taking stronger mereologies or stronger theories of orderings. However,
strengthening the building modules does not always provide the required ontology.
13 A hierarchy is a set of ontologies with the same signature [5]. More formally, a hierarchy H = hH , i is
a partially ordered, finite set of theories H = T1 , ..., Tn such that
1. S(Ti ) = S(T j ), for all i, j;
2. T1 T2 iff T2 is an extension of T1 ;
3. T1 < T2 iff T2 is a non-conservative extension of T1 .
For example, the work in [6] shows that verification of Tperiods requires two ontolo-
gies, Tlower preserve and Tupper preserve , in the subposet hierarchy where Tlower preserve is
constructed by adding the following residue axiom to Tmereology [ Tpartial ordering
(8x, y, z) part(y, z) ^ leq(x, y) leq(x, z)
and Tupper preserve is constructed by adding the following residue axiom to Tmereology [
Tpartial ordering
(8x, y, z) part(z, x) ^ leq(x, y) leq(z, y).
Notice that both of these two axioms specify the relationship between the parthood re-
lation and the ordering relation. In other words, these axioms determine how models of
modules of Tlower preserve and Tupper preserve must be combined.
Another example is the theory of subposets (Tsubposet ) itself, which is obtained by
extending Tlower preserve [ Tupper preserve with the residue axiom
(8x, y) part(x, y) leq(x, y).
In all of these three examples, the residue eliminates some possible combinations
of models of the modules. All theories in Figure 3 are obtained by adding residues to
Tmereology [ Tpartial ordering .
This observation can be generalized in terms of an ontology composition principle:
Consider the root theory T of an ontology hierarchy so that T contains weak reduc-
tive modules T1 , ..., Tn and residue R. Other ontologies in the hierarchy are obtained by
strengthening at least one of T1 , ..., Tn , or strengthening R.
6. Summary
In this paper we have introduced the notion of the residue of a theory, which is the set
of sentences not contained in any module of the theory. Given the original motivations
for the study of modularity in the notion of ontology extension (safety) and ontology
reuse, it is perhaps not surprising that there does not appear to have been any earlier
work on the notion of residue. However, we have shown that residues play a critical
role in the design and verification of ontologies. For verification, residues are used to
distinguish between reductive modules and weak reductive modules of a theory. For
design, the residue constrains how models of the theory can be constructed from models
of its modules.
References
[1] Carmen Chui. Axiomatized Relationships between Ontologies. Master’s thesis, University of Toronto,
2013.
[2] H. Enderton. Mathematical Introduction to Logic. Academic Press, 1972.
[3] M. Gruninger. Verification of the OWL-Time Ontology. In Proceedings of the Tenth International
Semantic Web Conference, 2011.
[4] M. Gruninger and B. Aameri. Preservation of Modules. In 8th International Workshop on Modular
Ontologies, 2014.
[5] M. Gruninger, T. Hahmann, A. Hashemi, D. Ong, and A. Ozgovde. Modular first-order ontologies via
repositories. Applied Ontology, 7(2):169–209, 2012.
[6] Michael Gruninger and Darren Ong. Verification of Time Ontologies with Points and Intervals. In
TIME, pages 31–38, 2011.
[7] Wilfrid Hodges. Model theory. Cambridge University Press Cambridge, 1993.
[8] Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter. Formal Properties of Modularisation. In
Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, pages 159–
186, 2009.
[9] Oliver Kutz and Till Mossakowski. A Modular Consistency Proof for DOLCE. In Wolfram Burgard and
Dan Roth, editors, Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI
2011), August 7-11, 2011, pages 227–234, San Francisco, California, USA, 2011. AAAI Press.
[10] J. van Benthem. The Logic of Time: A Model-Theoretic Investigation into the Varieties of Temporal
Ontology and Temporal Discourse. Synthese Library. Springer, 1991.
[11] Chiara Del Vescovo, Bijan Parsia, Ulrike Sattler, and Thomas Schneider. The Modular Structure of
an Ontology: Atomic Decomposition. In Int. Joint Conference on Artificial Intelligence (IJCAI 2011),
pages 2232–2237, 2011.