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.