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 computational 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 ontology verification that is based on repositories. Verification is concerned with the relationship between the intended models of an ontology and the models of the axiomatization of the ontology. In particular, we want to characterize the models of an ontology up to isomorphism and determine whether or not these models are equivalent to the intended models of the ontology. 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 problem. 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 approach in which we define a special class of modules that are preserved by logical synonymy. This new class of modules is based on the notion of reducible theories from [4].

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 mappings between theories that provide sufficient conditions for the preservation of modules.

Modules and Conservative Extensions

In this paper, we consider a theory to be a set of first-order sentences closed under logical consequence. We follow previous work in terminology and notation [4] treating ontologies 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 T 1 , T 2 be two first-order theories such that Σ(T 1 ) ⊆ Σ(T 2 ).

T 2 is a proof-theoretic conservative extension of T 1 iff for any sentence σ ∈ L (T 1 ),

T 2 |= σ ⇔ T 1 |= σ .

T 2 is a model-theoretic conservative extension of T 1 iff every model of T 1 can be expanded to a model of T 2 .

In this paper, we will focus on model-theoretic conservative extension. [5] establishes the close relationship between the two notions -T 2 is a proof-theoretic conservative extension of T 1 iff every model of T 1 is elementarily equivalent to a structure that can be expanded to a model of T 2 .

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 T 1 is a module of T 2 iff T 2 is a conservative extension of T 1 .

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.

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 T 1 with signature Σ(T 1 ) into a theory T 2 with signature Σ(T 2 ) is a function on the set of non-logical symbols of Σ(T 1 ) and formulae in L (T 1 ) such that 1. π assigns to ∀ a formula π ∀ of Σ(T 2 ) in which at most the variable v 1 occurs free, such that T 2 |= (∃v 1 ) π ∀ 2. π assigns to each n-place relation symbol P a formula π P of Σ(T 2 ) in which at most the variables v 1 , ..., v n occur free. 3. for any atomic sentence σ ∈ Σ(T 1 ) with relation symbol P, π(σ ) = π(P); 4. for any sentence σ ∈ Σ(T 1 ), π(¬σ ) = ¬π(σ ); 5. for any sentences σ , τ ∈ Σ(T 1 ), π(σ ⊃ τ) = π(σ ) ⊃ π(τ); 6. for any sentence σ ∈ Σ(T 1 ), π(∀x σ ) = ∀x π ∀ ⊃ π(σ ); 7. For any sentence σ ∈ Σ(T 1 ),

T 1 |= σ ⇒ T 2 |= π(σ )

Thus, the mapping π is an interpretation of T 1 if it preserves the theorems of T 1 and we say T 1 is interpretable in T 2 .

Definition 4 An interpretation π of a theory T 1 into a theory T 2 is faithful iff for any sentence σ ∈ Σ(T 1 ),

T 1 |= σ ⇒ T 2 |= π(σ )

Thus, the mapping π is a faithful interpretation of T 1 if it preserves satisfiability with respect to T 1 . We will also refer to this by saying that T 1 is faithfully interpretable in T 2 .

Definition 5 Let T 0 be a theory with signature Σ(T 0 ) and let T 1 be a theory with signature Σ(T 1 ) such that Σ(T 0 ) ∩ Σ(T 1 ) = / 0. Translation definitions for T 0 into T 1 are conservative definitions in Σ(T 0 ) ∪ Σ(T 1 ) of the form

∀x p i (x) ≡ Φ(x)

where p i (x) is a relation symbol in Σ(T 0 ) and Φ(x) is a formula in Σ(T 1 ).

Following [7], translation definitions can be considered to be an axiomatization of the interpretation of T 0 into T 1 .

In [4], it was shown that T 1 is interpretable in T 2 iff there exist a set of translation definitions ∆ for T 1 into T 2 such that

T 2 ∪ ∆ |= T 1 2.2.

Logical Synonymy

One notion of equivalence among theories is mutual faithful interpretability, that is, T 1 faithfully interprets T 2 and T 2 faithfully interprets T 1 . An even stronger equivalence relation is that of logical synonymy: Definition 6 Two ontologies T 1 and T 2 are synonymous iff there exists an ontology T 3 with the signature Σ(T 1 ) ∪ Σ(T 2 ) that is a definitional extension of T 1 and T 2 .

It is easy to see that logical synonymy implies mutual faithful interpretability:

Lemma 1 If T 1 and T 2 are synonymous, then T 1 faithfully interprets T 2 , and T 2 faithfully interprets T 1 .

Logical synonymy is a powerful metalogical relationship that supports ontology verification; [8] shows how this relationship preserves the models of a theory, allowing us to characterize the models of a theory up to isomorphism.

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. However, 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 C 1 ,C 2 are isomorphic iff there exists functors F and G such that

• F : C 1 → C 2 and G : C 2 → C 1 ; • FG = 1 C 2 and GF = 1 C 1 .

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(T 1 ) and Mod(T 2 ) then T 1 is logically synonymous with T 2 .

In order to guarantee that we have an isomorphism of categories between the category of models of T 1 and the category of models of T 2 , [9] imposes the following conditions on the translation definitions ∆ for T 1 into T 2 and the Π for T 2 into T 1 :

1. ∆ is T 1 -existential, T 2 -universal, and T 2 -equivalent to positive formulae; 2. Π is T 2 -existential, T 1 -universal, and T 1 -equivalent to positive formulae; Thus, the translation definitions ∆ and Π must be quantifier-free formulae.

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.

Boolean Lattices

There is a variety of alternative axiomatizations for boolean lattices with different signatures. Within COLORE, there are axiomatizations of Boolean lattices in four different hierarchies: All of these theories are logically synonymous with each other. In addition, Mod(T boolean ring ) and Mod(T boolean lattice ) are category isomorphic.

The theories T boolean lattice ordering and T boolean dis joint have no nontrivial modules. On the other hand, the theories T boolean lattice and T boolean 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 T boolean lattice {(∀x) ( join(x, x) = x), (∀x, y) ( join(x, y) = join(y, x))} is not synonymous with any maximal module T boolean ring .

The relevance of these theories to the broader ontology community lies in their relationship to mereologies. The ontology T cem c for first-order complete extensional mereology is closely related to boolean lattices, being logically synonymous with the theory of boolean semilattices (i.e. boolean lattices with the 0 element removed).

Ontologies for Time Intervals

Within COLORE, there are three hierarchies of time interval ontologies:

• the hierarchy H Periods , whose theories were introduced in [11],

• the hierarchy H Approximate−Point presented in [12],

• the hierarchy H Interval−Meeting , which has been explored in [12]. [13] gives an overview of the metalogical relationships among theories in these three hierarchies. T ap root 6 and T periods root7 are logically synonymous, and there is a one-to-one correspondence between the modules of these two theories. On the other hand, T meets root 8 and T periods root are logically synonymous, yet the former theory has no proper modules.

Summary

We have shown that metalogical relationships as strong as logical synonymy and isomorphism 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.

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 interpretation, and synonymy are based on the existence of translation definitions. Furthermore, 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 T 1 and T 2 are logically synonymous with translation definitions ∆ and Π such that

T 1 ∪ ∆ |= T 2 T 2 ∪ Π |= T 1 If T 1i ∪ ∆ ∪ Π is a definitional extension of T 1i for each module T 1i of T 1 ,

then there is a one-to-one correspondence between the set of modules of T 1 and the set of modules of T 2 .

Proof: Let π 1 be the (faithful) interpretation of T 1 into T 2 and let π 2 be the (faithful) interpretation of T 2 into T 1 .

For any module T 1i of T 1 , suppose

T 2i = {σ : T 1i ∪ ∆ |= σ } T 1 j = {σ : σ ∈ L (T 1i ), T 1i ∪ ∆ ∪ Π |= σ } Since T 1i ∪ ∆ ∪ Π

is a definitional extension of T 1i , we can see that T 1 j is logically equivalent to T 1i , and hence π 2 π 1 (T 1i ) = T 1i for each module T 1i of T 1 . Therefore, the interpretation π 1 is a bijection from the set of modules of T 1 to subtheories of T 2 . Now suppose that T 2i is not a module of T 2 , so that there exists a sentence σ with the same signature of T 2i such that T 2i |= σ , T 2 |= σ By definition, T 1 j |= π 2 (σ ) and hence T 1i |= π 2 (σ ) However, since T 1 and T 2 are synonymous, we must also have T 1 |= π 2 (σ ) which contradicts the assumption that T 1i is a module of T 1 . A similar argument shows that the interpretation π 2 is a bijection from the set of modules of T 2 to subtheories of T 1 , and that these subtheories are modules of T 2 . Thus, we have a bijection between the set of modules of T 1 and the set of modules of T 2 . 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.

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)

T boolean lattice ∪ ∆ ∪ Π is not a definitional extension of T boolean lattice since it entails the sentence (∀x, y) join(x, y) = join(meet(x, y), join(meet(x, comp(y)), meet(comp(x), y)))

Time Interval Ontologies

The translation definitions ∆ p ap for the interpretation of theories in H Approximate−Point to theories in H Periods 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 H Periods to theories in H Approximate−Point are logically equivalent to these sentences, from which it is easy to see that T periods ∪ ∆ p ap ∪ Π ap p is a definitional extension of T periods . Note that there is a one-to-one correspondence between the set of modules of T ap root and the set of modules of T periods root .

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 S 1 , ..., S n (n > 1) iff 1. T faithfully interprets each theory S i ; 2. T is synonymous with S 1 ∪ ... ∪ S n .

We will refer to the set S 1 , ..., S n 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 , and T is reducible to S 1 , ..., S n , then T is reducible to S 1 , ..., S n .

Proof: Suppose T is reducible to S 1 , ..., S n . By definition, T faithfully interprets each S i . By Lemma 7 of [4], T also faithfully interprets each S i . By definition, we also know that S 1 ∪ ... ∪ S n faithfully interprets T ; by Lemma 7 of [4], S 1 ∪ ... ∪ S n also faithfully interprets T .

T is synonymous with T . By definition, T is synonymous with S 1 ∪ ... ∪ S n . By Theorem 2 in [8], synonymy is transitive. Therefore, T is synonymous with S 1 ∪ ... ∪ S n . Together, these three conditions show that T is reducible to S 1 , ..., S n . 2

Consider for example the theory T end points9 (which is a time ontology for timepoints and time intervals) and the theory T psl ob j (that axiomatizes object structures in the PSL ontology). T end 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. T psl ob j includes all function and predicate symbols in T end 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. T end points and T psl ob j are synonymous, and both are reducible to the theory T linear ordering10 of linear ordering and the theory T strict graphical11 of strict graphical incidence structures. Faithful interpretation generalizes the notion of conservative extension, so each theory S i in a reduction of a theory T should be related to a module T i of T . The following theorem shows that S i and T i are related by synonymy.

Theorem 3 Let S 1 , ..., S n be a reduction of a theory T .

There exist theories T 1 , ..., T n such that 1. T i is synonymous with S i .

2. T i is a module of T , for 1 ≤ i ≤ n;

Proof: Let S 1 , ..., S n be a reduction of a theory T ; by the definition of reducibility, T is synonymous with S 1 ∪ ... ∪ S n .

There exists an interpretation π of S 1 ∪ ... ∪ S n into T , so that for any σ ∈ Σ(S 1 ∪ ... ∪ S n ),

S 1 ∪ ... ∪ S n |= σ ⇔ T |= π(σ )

Similarly, there exists an interpretation π i of T into S i . Let

T i = {σ : S i |= π i (σ ), T |= σ }

By the definition of reducibility, T faithfully interprets S i , so that we have

S i |= σ ⇔ T |= π(σ )

so that T i is synonymous with S i . T i is not synonymous with T j , for any i = j, 1 ≤ i, j ≤ n, because otherwise S i is synonymous with S j . Suppose that T is a nonconservative extension of T i . Then exists Φ ∈ L (T i ) such that

T |= Φ, T i |= Φ.

S i and T i are synonymous, so that

S i ∪ ∆ i |= Φ.

However, by the definition of reducibility, T is a conservative extension of S i ∪ ∆ i . Since Φ ∈ L (T i ), we have

T |= Φ

which contradicts the assumption that T is a nonconservative extension of T i . 2

We will refer to the set of subtheories T 1 , ..., T n as the reductive modularization of the theory T that corresponds to the reduction S 1 , ..., S n ; the subtheories T i 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 T wog 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, T wog 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 of T which is not a module of any reductive module of T .

Case 1: T is not a subtheory of any reductive module of T . Since T cannot be synonymous with a subtheory of any theory in the reduction of T , we must have

S 1 ∪ ... ∪ S m ∪ Π |= T , m < n

, in which case S 1 ∪ ... ∪ S m ∪ Π is a nonconservative extension of T . However, T is a nonconservative extension of S 1 ∪ ... ∪ S m ∪ Π, making T a nonconservative extension of T , which contradicts the assumption that T is a module of T .

Case 2: T is a subtheory of a reductive module T i of T , but T is not a module of T i . T i must be a nonconservative extension of T , so that there exists a sentence Φ ∈ L (T ) such that T |= Φ and T i |= Φ Since T i is a module of T , we must have T |= Φ. which contradicts the assumption that T 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 theories 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 T 1 , T 2 are synonymous reducible theories, then each reductive module of T 1 is synonymous with a reductive module of T 2 .

Proof: Let T 1 , T 2 be synonymous reducible theories.

Let S 1 , ..., S n be a reduction of T 1 . By Theorem 3 there exists reductive modularization T 11 , ..., T 1n of T 1 such that T 1i is synonymous with S i . By Theorem 2, S 1 , ..., S n is also a reduction of T 2 . By Theorem 3 there exists reductive modularization T 21 , ..., T 2n of T 2 such that T 2i is synonymous with S i . By Theorem 2 in [8], synonymy is transitive. Therefore, T 1i is synonymous with T 2i for all 1 ≤ i ≤ n. 2

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.

Preservation by Conservative Extensions

In general, the modules of a theory are preserved by conservative extension.

Theorem 6 If T 1 is a conservative extension of T 2 , then each module of T 2 is also a module of T 1 .

Proof: Suppose T 3 is a module of T 2 and T 2 is a module of T 1 . If every model of T 3 can be expanded to a model of T 2 , and every model of T 2 can be expanded to a model of T 1 , then every model of T 3 can be expanded to a model of T 1 . Thus, T 1 is a conservative extension of T 3 , and T 3 is a module of T 1 . 2

On the other hand, reductive modules of a theory are not preserved by conservative extension -there exist theories which have nontrivial reductive modules, yet a conservative extension of such a theory has no nontrivial reductive modules. For example, the theory 12 T betweenness ∪ T weak bipartite contains both T betweenness and T weak bipartite as reductive modules. However, the theory T wog 13 is a conservative extension of T betweenness ∪ T weak bipartite yet it has no reductive modules.

Preservation by Definitional Extensions

Translation definitions are conservative definitions, so the failure of definitional extensions 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 T boolean lattice ordering ∪ ∆ is a definitional extension of T boolean lattice ordering and a conservative extension of T boolean lattice , even though T boolean lattice ordering itself has no proper modules.

Theorem 7 Let T ∪ Σ be a definitional extension of T .

T has reductive modules T 1 , ..., T n iff T ∪ Σ has reductive modules T 1 , ..., T n .

Proof: Let T ∪ Σ be a definitional extension of T . Then T ∪ Σ and T are synonymous. Since synonymy is transitive, T is synonymous with S 1 ∪ ... ∪ S n iff T ∪ Σ is synonymous with S 1 ∪ ... ∪ S n .

Considering that Σ is a set of conservative definitions of T , it is straightforward to see that T faithfully interprets S i iff T ∪ Σ faithfully interprets S i . Hence T is reducible to S 1 , ..., S n iff T ∪ Σ is reducible to S 1 , ..., s n . By Theorem 3, there exist T 1 , ..., T n such that T 1 , ..., T n are reductive modules of T iff T 1 , ..., T n 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 ∪ Σ.

Summary

In this paper, we have considered the problem of reusing the modularization of an ontology -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 metalogical relationships among ontologies (such as faithful interpretability, logical synonymy, isomorphism of categories, and reducibility) preserve the modules of an ontology. Interestingly, 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 translation 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 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.