=Paper=
{{Paper
|id=Vol-1248/paper2
|storemode=property
|title=Preservation of Modules
|pdfUrl=https://ceur-ws.org/Vol-1248/WoMO14-Paper3.pdf
|volume=Vol-1248
|dblpUrl=https://dblp.org/rec/conf/fois/GruningerA14
}}
==Preservation of Modules==
https://ceur-ws.org/Vol-1248/WoMO14-Paper3.pdf
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.