Preservation of Modules Michael GRÜNINGER a , Bahar AAMERI b a Department of Mechanical and Industrial Engineering, University of Toronto, Ontario, Canada M5S 3G8 b Department of Computer Science, University of Toronto, Ontario, Canada M5S 3G8 Abstract. Within the Common Logic Ontology Repository (COLORE), relation- ships among ontologies such as the notions of faithful interpretability, logical syn- onymy, and reducibility have been used for ontology verification. Earlier work has shown how to use these relationships to find modules of theories, so a natural ques- tion is to determine how we can use the decomposition of one theory into modules to find the modules of another theory in the repository. In this paper, we examine a number of ontologies for which faithful interpretability and logical synonymy do not preserve their modules. Nevertheless, we identify a class of interpretations among theories which guarantees that the modules of a theory are preserved. We also show that the modules of reducible theories are preserved by logical synonymy. Keywords. modules, first-order theories, logical synonymy, faithful interpretation, reducibility, translation definitions 1. Introduction The task of decomposing a first-order ontology into modules – subtheories which are conservatively extended by the ontology – remains a significant challenge for the field of ontological engineering [1]. Understanding the structure of an ontology’s modules gives us insight into a wide range of properties, from the characterization of the ontology’s models to the relationship among other ontologies in the same domain. Given the com- putational intractability of automatically identifying the modules of an ontology [2], [3], one approach is to reuse the modularizations of existing theories. This idea leads to a key research question — under what conditions can we use the decomposition of one theory into a set of modules to find the modularization of another theory? The notion of reusing modularizations arises in particular with an approach to on- tology verification that is based on repositories. Verification is concerned with the rela- tionship between the intended models of an ontology and the models of the axiomati- zation 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 in- tended models of the ontology. In practice, the verification of an ontology is achieved by demonstrating that it is synonymous with a theory in the repository whose models have already been characterized up to isomorphism. Given two theories which are logically synonymous, we would ideally like to be able identify the modules of the new theory based on the modules of the synonymous theory in the repository. A key observation of this paper is that there exist logically synonymous theories which have very different modular decompositions. In Section 2, we survey two different sets of ontologies – for lattices and time intervals – and find ontologies which have no proper modules yet which are synonymous with ontologies that have multiple modules. In the remainder of the paper, we explore two possible approaches to deal with this prob- lem. In Section 3 we impose conditions on the interpretations to specify those which do preserve the modules of synonymous theories. In Section 4, we take an alternative ap- proach in which we define a special class of modules that are preserved by logical syn- onymy. This new class of modules is based on the notion of reducible theories from [4]. 2. Modules and Logically Synonymous Theories A key objective of this paper focuses on the reuse of modularizations between theories. After reviewing the different metalogical relationships among theories that play a role in ontology verification, we find sets of theories for which none of these relationships preserve the sets of modules of the theories. We then consider properties of specific map- pings between theories that provide sufficient conditions for the preservation of modules. 2.1. Modules and Conservative Extensions In this paper, we consider a theory to be a set of first-order sentences closed under logi- cal consequence. We follow previous work in terminology and notation [4] treating on- tologies and their modules as logical theories. We do not distinguish between logically equivalent theories. For every theory T , Σ(T ) denotes its signature, which includes all the constant, function, and relation symbols used in T , and L (T ) denotes the language of T , which is the set of first-order formulae that only use the symbols in Σ(T ). We remind the reader of the notion of conservative extension [1]: Definition 1 Let T1 , T2 be two first-order theories such that Σ(T1 ) ⊆ Σ(T2 ). T2 is a proof-theoretic conservative extension of T1 iff for any sentence σ ∈ L (T1 ), T2 |= σ ⇔ T1 |= σ . T2 is a model-theoretic conservative extension of T1 iff every model of T1 can be expanded to a model of T2 . In this paper, we will focus on model-theoretic conservative extension. [5] estab- lishes the close relationship between the two notions – T2 is a proof-theoretic conserva- tive extension of T1 iff every model of T1 is elementarily equivalent to a structure that can be expanded to a model of T2 . Most work on modularity in ontologies considers a module to be a subset of axioms in a theory; In this paper, we adopt a more general notion for a module of a theory, by considering a module to be a subtheory of the theory: Definition 2 T1 is a module of T2 iff T2 is a conservative extension of T1 . 2.2. Relationships Among Theories There are a range of fundamental metalogical relationships among first-order theories. All of them consider mappings between the signatures of the theories which preserve entailment and satisfiability. In this section, we review the three different metalogical relationships that play key roles in ontology verification. 2.2.1. Interpretability The notion of interpretability between theories is widely used within mathematical logic and applications of ontologies for semantic integration. We adopt the following definition from [6]: Definition 3 An interpretation π of the theory T1 with signature Σ(T1 ) into a theory T2 with signature Σ(T2 ) is a function on the set of non-logical symbols of Σ(T1 ) and formulae in L (T1 ) such that 1. π assigns to ∀ a formula π∀ of Σ(T2 ) in which at most the variable v1 occurs free, such that T2 |= (∃v1 ) π∀ 2. π assigns to each n-place relation symbol P a formula πP of Σ(T2 ) in which at most the variables v1 , ..., vn occur free. 3. for any atomic sentence σ ∈ Σ(T1 ) with relation symbol P, π(σ ) = π(P); 4. for any sentence σ ∈ Σ(T1 ), π(¬σ ) = ¬π(σ ); 5. for any sentences σ , τ ∈ Σ(T1 ), π(σ ⊃ τ) = π(σ ) ⊃ π(τ); 6. for any sentence σ ∈ Σ(T1 ), π(∀x σ ) = ∀x π∀ ⊃ π(σ ); 7. For any sentence σ ∈ Σ(T1 ), T1 |= σ ⇒ T2 |= π(σ ) Thus, the mapping π is an interpretation of T1 if it preserves the theorems of T1 and we say T1 is interpretable in T2 . Definition 4 An interpretation π of a theory T1 into a theory T2 is faithful iff for any sentence σ ∈ Σ(T1 ), T1 6|= σ ⇒ T2 6|= π(σ ) Thus, the mapping π is a faithful interpretation of T1 if it preserves satisfiability with respect to T1 . We will also refer to this by saying that T1 is faithfully interpretable in T2 . Definition 5 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 ). Following [7], translation definitions can be considered to be an axiomatization of the interpretation of T0 into T1 . In [4], it was shown that T1 is interpretable in T2 iff there exist a set of translation definitions ∆ for T1 into T2 such that T2 ∪ ∆ |= T1 2.2.2. Logical Synonymy One notion of equivalence among theories is mutual faithful interpretability, that is, T1 faithfully interprets T2 and T2 faithfully interprets T1 . An even stronger equivalence rela- tion is that of logical synonymy: Definition 6 Two ontologies T1 and T2 are synonymous iff there exists an ontology T3 with the signature Σ(T1 ) ∪ Σ(T2 ) that is a definitional extension of T1 and T2 . It is easy to see that logical synonymy implies mutual faithful interpretability: Lemma 1 If T1 and T2 are synonymous, then T1 faithfully interprets T2 , and T2 faithfully interprets T1 . Logical synonymy is a powerful metalogical relationship that supports ontology ver- ification; [8] shows how this relationship preserves the models of a theory, allowing us to characterize the models of a theory up to isomorphism. 2.2.3. Isomorphism of Categories As powerful as logical synonymy is, it does not preserve the following model-theoretic properties of a theory – submodels/embedding, homomorphic images, direct products, existentially closed models, model completeness, and the amalgamation property. How- ever, these properties are preserved by isomorphism of categories [9]. For any first-order theory T , Mod(T ) forms a category in which the models of T are the objects and homomorphisms on the models are the morphisms. Definition 7 Two categories C1 ,C2 are isomorphic iff there exists functors F and G such that • F : C1 → C2 and G : C2 → C1 ; • FG = 1C2 and GF = 1C1 . In [10], this is referred to as definitional equivalence of algebraic theories. Isomorphism of categories of models of theories is stronger than logical synonymy. Lemma 2 If there is an isomorphism of categories between Mod(T1 ) and Mod(T2 ) then T1 is logically synonymous with T2 . In order to guarantee that we have an isomorphism of categories between the cate- gory of models of T1 and the category of models of T2 , [9] imposes the following condi- tions on the translation definitions ∆ for T1 into T2 and the Π for T2 into T1 : 1. ∆ is T1 -existential, T2 -universal, and T2 -equivalent to positive formulae; 2. Π is T2 -existential, T1 -universal, and T1 -equivalent to positive formulae; Thus, the translation definitions ∆ and Π must be quantifier-free formulae. 2.3. Modules Are Not Preserved by Synonymy The following examples show that modules are not preserved by logical synonymy (and hence they are not preserved by interpretation or faithful interpretation). In fact, not even isomorphism of categories is strong enough to preserve modules. In some cases, there exists a theory with no nontrivial modules, yet it is logically synonymous with a theory that does have nontrivial modules. In other cases, there exist modules of one theory which are not logically synonymous to modules of the other theory. 2.3.1. Boolean Lattices There is a variety of alternative axiomatizations for boolean lattices with different sig- natures. Within COLORE, there are axiomatizations of Boolean lattices in four different hierarchies: 1 • Tboolean lattice 2 in Hlattices , with signature {meet, join, zero, one}; • Tboolean lattice ordering 3 in Hordering , with signature {leq}; • Tboolean ring 4 in Hringoids , with signature {sum, prod, zero, one}; • Tboolean dis joint 5 in Hdis jointness , with signature {disjoint}; All of these theories are logically synonymous with each other. In addition, Mod(Tboolean ring ) and Mod(Tboolean lattice ) are category isomorphic. The theories Tboolean lattice ordering and Tboolean dis joint have no nontrivial modules. On the other hand, the theories Tboolean lattice and Tboolean ring do have nontrivial modules, but there is not a one-to-one correspondence between the sets of modules for these two theories. For example, the maximal module of Tboolean lattice {(∀x) ( join(x, x) = x), (∀x, y) ( join(x, y) = join(y, x))} is not synonymous with any maximal module Tboolean ring . The relevance of these theories to the broader ontology community lies in their rela- tionship to mereologies. The ontology Tcem c for first-order complete extensional mere- ology is closely related to boolean lattices, being logically synonymous with the theory of boolean semilattices (i.e. boolean lattices with the 0 element removed). 2.3.2. Ontologies for Time Intervals Within COLORE, there are three hierarchies of time interval ontologies: 1 The basic organizational principle in COLORE is the notion of a hierarchy [4], which is a set of ontologies with the same signature. In particular, a hierarchy H = hH , ≤i is a partially ordered, finite set of theories H = T1 , ..., Tn such that 1. Σ(Ti ) = Σ(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 . 2 http://colore.oor.net/lattices/boolean_lattice.clif 3 http://colore.oor.net/orderings/boolean_lattice_ordering.clif 4 http://colore.oor.net/ringoids/boolean_ring.clif 5 http://colore.oor.net/disjointness/boolean_disjoint.clif • the hierarchy HPeriods , whose theories were introduced in [11], • the hierarchy HApproximate−Point presented in [12], • the hierarchy HInterval−Meeting , which has been explored in [12]. [13] gives an overview of the metalogical relationships among theories in these three hierarchies. Tap root 6 and Tperiods root 7 are logically synonymous, and there is a one-to-one correspondence between the modules of these two theories. On the other hand, Tmeets root 8 and Tperiods root are logically synonymous, yet the former theory has no proper modules. 2.3.3. Summary We have shown that metalogical relationships as strong as logical synonymy and iso- morphism of categories fail to preserve the modules of the theories. This is particularly noteworthy because logical synonymy is typically considered to be a demonstration that the theories are merely notational variants of each other, essentially providing alternative axiomatizations of a theory using different signatures. 2.4. Preservation of Modules by Translation Definitions Although logical synonymy alone does not preserve modules of a theory, it is important to remember that all of the metalogical relationships such as interpretation, faithful in- terpretation, and synonymy are based on the existence of translation definitions. Further- more, we have seen that the even stronger notion of isomorphism of categories required additional conditions be imposed on the translation definitions. If we want to preserve the modules of a theory, we also need to look at properties of the translation definitions themselves. Theorem 1 Suppose that T1 and T2 are logically synonymous with translation definitions ∆ and Π such that T1 ∪ ∆ |= T2 T2 ∪ Π |= T1 If T1i ∪ ∆ ∪ Π is a definitional extension of T1i for each module T1i of T1 , then there is a one-to-one correspondence between the set of modules of T1 and the set of modules of T2 . Proof: Let π1 be the (faithful) interpretation of T1 into T2 and let π2 be the (faithful) interpretation of T2 into T1 . For any module T1i of T1 , suppose T2i = {σ : T1i ∪ ∆ |= σ } T1 j = {σ : σ ∈ L (T1i ), T1i ∪ ∆ ∪ Π |= σ } 6 http://colore.oor.net/approximate_point/ap_root.clif 7 http://colore.oor.net/periods/period_root.clif 8 http://colore.oor.net/interval_meeting/meets_root.clif Since T1i ∪ ∆ ∪ Π is a definitional extension of T1i , we can see that T1 j is logically equivalent to T1i , and hence π2 π1 (T1i ) = T1i for each module T1i of T1 . Therefore, the interpretation π1 is a bijection from the set of modules of T1 to subtheories of T2 . Now suppose that T2i is not a module of T2 , so that there exists a sentence σ with the same signature of T2i such that T2i 6|= σ , T2 |= σ By definition, T1 j 6|= π2 (σ ) and hence T1i 6|= π2 (σ ) However, since T1 and T2 are synonymous, we must also have T1 |= π2 (σ ) which contradicts the assumption that T1i is a module of T1 . A similar argument shows that the interpretation π2 is a bijection from the set of modules of T2 to subtheories of T1 , and that these subtheories are modules of T2 . Thus, we have a bijection between the set of modules of T1 and the set of modules of T2 . 2 We can revisit the examples from the preceding section to see which interpretations saisfy the sufficient conditions for preserving the modules of the theories. 2.4.1. Boolean Lattices Consider the translation definitions ∆: (∀x, y, z) (sum(x, y) = z) ≡ ( join(meet(x, comp(y)), meet(comp(x), y)) = z) (∀x, y, z) (prod(x, y) = z) ≡ (meet(x, y) = z) and the translation definitions Π (∀x, y, z) ( join(x, y) = z) ≡ (sum(x, sum(y, prod(x, y))) = z) (∀x, y, z) (meet(x, y) = z) ≡ (prod(x, y) = z) (∀x, y) (comp(x) = y) ≡ (sum(x, y) = one) Tboolean lattice ∪ ∆ ∪ Π is not a definitional extension of Tboolean lattice since it entails the sentence (∀x, y) join(x, y) = join(meet(x, y), join(meet(x, comp(y)), meet(comp(x), y))) 2.4.2. Time Interval Ontologies The translation definitions ∆ p ap for the interpretation of theories in HApproximate−Point to theories in HPeriods is the set of sentences (∀x, y) precedence(x, y) ≡ precedes(x, y) (∀x, y) inclusion(x, y) ≡ f iner(x, y) and the translation definitions Πap p for the interpretation of theories in HPeriods to the- ories in HApproximate−Point are logically equivalent to these sentences, from which it is easy to see that Tperiods ∪ ∆ p ap ∪ Πap p is a definitional extension of Tperiods . Note that there is a one-to-one correspondence between the set of modules of Tap root and the set of modules of Tperiods root . 3. Preservation of Modules in Reducible Theories So far we have seen that in general, modules are not preserved by faithful interpretation and logical synonymy. In this section we introduce a special class of modules, based on the notion of reducible theories, and show that such modules are preserved by synonymy. We start with the definition of reducible theories: Definition 8 A theory T is reducible to a set of theories S1 , ..., Sn (n > 1) iff 1. T faithfully interprets each theory Si ; 2. T is synonymous with S1 ∪ ... ∪ Sn . We will refer to the set S1 , ..., Sn as a reduction of T . The relevant property of reducible theories is that reductions are preserved, up to logical equivalence, by synonymy, because both faithful interpretation and synonymy are transitive relations: Theorem 2 If the theory T is synonymous with the theory T 0 , and T is reducible to S1 , ..., Sn , then T 0 is reducible to S1 , ..., Sn . Proof: Suppose T is reducible to S1 , ..., Sn . By definition, T faithfully interprets each Si . By Lemma 7 of [4], T 0 also faithfully interprets each Si . By definition, we also know that S1 ∪ ... ∪ Sn faithfully interprets T ; by Lemma 7 of [4], S1 ∪ ... ∪ Sn also faithfully interprets T 0 . T 0 is synonymous with T . By definition, T is synonymous with S1 ∪ ... ∪ Sn . By Theorem 2 in [8], synonymy is transitive. Therefore, T 0 is synonymous with S1 ∪ ... ∪ Sn . Together, these three conditions show that T 0 is reducible to S1 , ..., Sn . 2 Consider for example the theory Tend points 9 (which is a time ontology for timepoints and time intervals) and the theory Tpsl ob j (that axiomatizes object structures in the PSL ontology). Tend points relates the time points and time intervals by defining the functions begino f , endo f , and between. begino f (i) and 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. Tpsl ob j includes all function and predicate symbols in Tend points except between and the sort predicate timeinterval, but it includes another sort predicate ob ject. Moreover, begino f and endo f are defined over ob ject elements. Tend points and Tpsl ob j are synonymous, and both are reducible to the theory Tlinear ordering 10 of linear ordering and the theory Tstrict graphical 11 of strict graphical incidence structures. Faithful interpretation generalizes the notion of conservative extension, so each the- ory Si in a reduction of a theory T should be related to a module Ti of T . The following theorem shows that Si and Ti are related by synonymy. Theorem 3 Let S1 , ..., Sn be a reduction of a theory T . There exist theories T1 , ..., Tn such that 9 http://colore.oor.net/combined_time/endpoints.clif 10 http://colore.oor.net/orderings/linear_ordering.clif 11 http://colore.oor.net/bipartite_incidence/strict_graphical.clif 1. Ti is synonymous with Si . 2. Ti is a module of T , for 1 ≤ i ≤ n; Proof: Let S1 , ..., Sn be a reduction of a theory T ; by the definition of reducibility, T is synonymous with S1 ∪ ... ∪ Sn . There exists an interpretation π of S1 ∪ ... ∪ Sn into T , so that for any σ ∈ Σ(S1 ∪ ... ∪ Sn ), S1 ∪ ... ∪ Sn |= σ ⇔ T |= π(σ ) Similarly, there exists an interpretation πi of T into Si . Let Ti = {σ : Si |= πi (σ ), T |= σ } By the definition of reducibility, T faithfully interprets Si , so that we have Si |= σ ⇔ T |= π(σ ) so that Ti is synonymous with Si . Ti is not synonymous with T j , for any i 6= j, 1 ≤ i, j ≤ n, because otherwise Si is synonymous with S j . Suppose that T is a nonconservative extension of Ti . Then exists Φ ∈ L (Ti ) such that T |= Φ, Ti 6|= Φ. Si and Ti are synonymous, so that Si ∪ ∆i 6|= Φ. However, by the definition of reducibility, T is a conservative extension of Si ∪ ∆i . Since Φ ∈ L (Ti ), we have T 6|= Φ which contradicts the assumption that T is a nonconservative extension of Ti . 2 We will refer to the set of subtheories T1 , ..., Tn as the reductive modularization of the theory T that corresponds to the reduction S1 , ..., Sn ; the subtheories Ti will be referred to as reductive modules. It is easy to see that not all modules of a theory are reductive. For example, the theory Twog of weak ordered geometries contains two modules (one of which is synonymous with a betweenness relation and other which is synonymous with a bipartite incidence structure); however, since it is not reducible, Twog has no reductive modules. Even if we restrict our attention to reducible theories, not all modules are reductive modules. The reductive modules of a reducible theory are maximal modules in the following sense: Theorem 4 Each module of a reducible theory T is a module of a reductive module of T . Proof: If T is reducible, there exists a set of reductive modules of T by Theorem 3. Suppose there exists a module T 0 of T which is not a module of any reductive module of T . Case 1: T 0 is not a subtheory of any reductive module of T . Since T 0 cannot be synonymous with a subtheory of any theory in the reduction of T , we must have S1 ∪ ... ∪ Sm ∪ Π |= T 0 , m < n , in which case S1 ∪ ... ∪ Sm ∪ Π is a nonconservative extension of T 0 . However, T is a nonconservative extension of S1 ∪ ... ∪ Sm ∪ Π, making T a nonconservative extension of T 0 , which contradicts the assumption that T 0 is a module of T . Case 2: T 0 is a subtheory of a reductive module Ti of T , but T 0 is not a module of Ti . Ti must be a nonconservative extension of T 0 , so that there exists a sentence Φ ∈ L (T 0 ) such that T 0 6|= Φ and Ti |= Φ Since Ti is a module of T , we must have T |= Φ. which contradicts the assumption that T 0 is a module of T . 2 Note that if there exist multiple reductions that contain different, but synonymous, sets of theories, each reduction leads to the same modularization, since the different theories in the reductions are synonymous. On the other hand, since synonymy is transitive, reductive modules of different theo- ries that are related to the same reduction are synonymous. We showed that synonymous theories have same reductions; reductive modules of a theory T are therefore preserved by synonymy: Theorem 5 If T1 , T2 are synonymous reducible theories, then each reductive module of T1 is synonymous with a reductive module of T2 . Proof: Let T1 , T2 be synonymous reducible theories. Let S1 , ..., Sn be a reduction of T1 . By Theorem 3 there exists reductive modularization T11 , ..., T1n of T1 such that T1i is synonymous with Si . By Theorem 2, S1 , ..., Sn is also a reduction of T2 . By Theorem 3 there exists reductive modularization T21 , ..., T2n of T2 such that T2i is synonymous with Si . By Theorem 2 in [8], synonymy is transitive. Therefore, T1i is synonymous with T2i for all 1 ≤ i ≤ n. 2 4. Preservation by Extension To this point we have considered the preservation of the modules of a theory by logical synonymy, that is, whether there is a one-to-one correspondence between the modules of two theories. We can also consider whether the modules of a theory are preserved by different kinds of extensions, that is, what is the relationship between the modules of T and the modules of an extension of T ? In this case, we are considering extensions of a theory which also expand the signature of the theory. 4.1. Preservation by Conservative Extensions In general, the modules of a theory are preserved by conservative extension. Theorem 6 If T1 is a conservative extension of T2 , then each module of T2 is also a module of T1 . Proof: Suppose T3 is a module of T2 and T2 is a module of T1 . If every model of T3 can be expanded to a model of T2 , and every model of T2 can be expanded to a model of T1 , then every model of T3 can be expanded to a model of T1 . Thus, T1 is a conservative extension of T3 , and T3 is a module of T1 . 2 On the other hand, reductive modules of a theory are not preserved by conserva- tive extension – there exist theories which have nontrivial reductive modules, yet a con- servative extension of such a theory has no nontrivial reductive modules. For example, the theory12 Tbetweenness ∪ Tweak bipartite contains both Tbetweenness and Tweak bipartite as re- ductive modules. However, the theory Twog 13 is a conservative extension of Tbetweenness ∪ Tweak bipartite yet it has no reductive modules. 4.2. Preservation by Definitional Extensions Translation definitions are conservative definitions, so the failure of definitional exten- sions to preserve modules follows from the discussion of Section 2. Thus, there exists a theory T with definitional extension T ∪ ∆ such that T ∪ ∆ has modules which are not modules of T . For example, if ∆ is the set of translation definitions (∀x, y, j) join(x, y) = j ≡ (leq(x, j) ∧ leq(y, j) ∧((∀z) (leq(x, z) ∧ leq(y, z) ⊃ leq( j, z) (∀x, y, z) meet(x, y) = z ≡ (leq(z, x) ∧ leq(z, y) ∧((∀z) (leq(z, x) ∧ leq(z, y) ⊃ leq(z, m) then Tboolean lattice ordering ∪ ∆ is a definitional extension of Tboolean lattice ordering and a conservative extension of Tboolean lattice , even though Tboolean lattice ordering itself has no proper modules. Theorem 7 Let T ∪ Σ be a definitional extension of T . T has reductive modules T1 , ..., Tn iff T ∪ Σ has reductive modules T1 , ..., Tn . Proof: Let T ∪ Σ be a definitional extension of T . Then T ∪ Σ and T are synonymous. Since synonymy is transitive, T is synonymous with S1 ∪ ... ∪ Sn iff T ∪ Σ is syn- onymous with S1 ∪ ... ∪ Sn . Considering that Σ is a set of conservative definitions of T , it is straightforward to see that T faithfully interprets Si iff T ∪ Σ faithfully interprets Si . Hence T is reducible to S1 , ..., Sn iff T ∪ Σ is reducible to S1 , ..., sn . By Theorem 3, there exist T1 , ..., Tn such that T1 , ..., Tn are reductive modules of T iff T1 , ..., Tn are reductive modules of T ∪ Σ. 2 Thus, T and T ∪ Σ have the same reductive modules. Theorem 7 also implies that T is not a reductive module of T ∪ Σ whenever Σ is a set of conservative definitions, even though T is a module of T ∪ Σ. 12 http://colore.oor.net/between/betweenness.clif http://colore.oor.net/bipartite_incidence/weak_bipartite.clif 13 http://colore.oor.net/ordered_geometry/wog.clif 5. Summary In this paper, we have considered the problem of reusing the modularization of an ontol- ogy – use the decomposition of one ontology into modules to find the modules of another ontology. This problem is formulated as determining whether or not various metalogi- cal relationships among ontologies (such as faithful interpretability, logical synonymy, isomorphism of categories, and reducibility) preserve the modules of an ontology. In- terestingly, there are examples of theories whose modules are not preserved by logical synonymy or even by isomorphism of categories. One observation is that all of these relationships are based on the existence of trans- lation definitions, so one approach to characterizing the preservation of modules imposes additional conditions on these translation definitions. An alternative approach is to show that restricted classes of modules are preserved by various metalogical relationships. In particular, we showed that the modules of a reducible theory that correspond to the theories in the reduction are indeed preserved by logical synonymy. References [1] 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. [2] Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Extracting Modules from Ontologies: A Logic Based Approach. In Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, pages 159–186, 2009. [3] 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. [4] M. Grüninger, T. Hahmann, A. Hashemi, D. Ong, and A. Ozgovde. Modular First-order ontologies via repositories. Applied Ontology, 7(2):169–209, 2012. [5] P. Veloso and S. Veloso. On conservative and expansive extensions. O que no faz pensar: Cadernos de Filosofia, 4:87–1068, 1991. [6] H. Enderton. Mathematical Introduction to Logic. Academic Press, 1972. [7] L.W. Szczerba. Interpretability of Elementary Theories. In Logic, Foundations of Mathematics and Computability Theory, pages 129–145, 1977. [8] D. Pearce and A. Valverde. Synonymous theories and knowledge representations in answer set program- ming. Journal of Computer and System Sciences, 78:86–104, 2012. [9] Charles Pinter. Properties preserved under definitional equivalence and interpretations . Zeitschrift fur Mathematik Logick und Grundlagen der Mathematik, 24:481–488, 1978. [10] R. Padmanabhan and S. Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific, 2008. [11] J. van Benthem. The Logic of Time: A Model-Theoretic Investigation into the Varieties of Temporal Ontology and Temporal Discourse. Synthese Library. Springer, 1991. [12] Patrick Hayes. A Catalog of Temporal Theories. Technical Report UIUC-BI-AI-96-01, Beckman Insti- tute and Departments of Philosophy and Computer Science, University of Illinois, 1996. [13] Michael Grüninger and Darren Ong. Verification of Time Ontologies with Points and Intervals. In TIME, pages 31–38, 2011.