Modules of a logical theory are subtheories that are conservatively extended by the theory. There are, on the other hand, subtheories that are not contained 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 combinations of models of modules of the theory. In that sense, ontological commitments that are captured by residues basically determine how arbitrary models of modules must be combined.
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 sentences 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.
1In 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.
,
T2 |= F .
We first provide a short review of the relationships between ontologies that will be necessary for introducing the notion of the residue of a theory.2
Non-conservative and conservative extensions are generalized to theories with
different signatures through the notions of non-faithful and faithful interpretations. We
adopt the definitions of these notions from [
free, and T2 |= (9 v1) p 8
most n variables occur free.
most the variables v1, ..., vn, vn+1 occur free, and
T2 |= (8 v1, ..., vn) p 8 (v1) ^ ... ^ p 8 (vn) (9 x)(p 8 (x) ^ ((8 vn+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 , F 1, F 2 2 L (T1), • if F is an atomic sentence with predicate symbol P, then p (F ) = p P; • p (¬F ) = ¬p (F ); • p (F 1 ^ F 2) = p (F 1) ^ p (F 2); • p (F 1 _ F 2) = p (F 1) _ p (F 2); • p (F 1 F 2) = p (F 1) p (F 2); • p (9 x F ) = (9 x) p 8 (x) ^ p (F ); • p (8 x F ) = (8 x) p 8 (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),
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:
(8 x) P(x) ⌘ F (x), where F is a formula in L (T );
Interpretations between theories can be axiomatized in terms of translation definitions between the theories:
definitional extension of T2 and
T2 [ D |= T1.
More formally, the results in [
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.
and only if there exists an ontology T3 with the signature S (T1) [ S (T2) that is a definitional extension of T1 and T2.
If T1 and T2 are logically synonymous, then there exists a set of translation definitions 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 .
We consider a module of a theory T to be a subtheory of T , and adopt the following
definition from [
Note that this is more general than the notion of module used in work such as [
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.
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:
T \ (T1 [ ... [ Tn).
Thus, a theory has a nontrivial residue iff it is not perfectly modularized. Example: Let T be the theory3 with axioms {(9 x) A(x), (9 x) B(x), (8 x) A(x) _ B(x)}.
T has two modules {(9 x) A(x)}, {(9 x) B(x)}.
The residue of T is {(8 x) A(x) _ B(x)}. ⇤ Example: Consider the ontology Tdolce present 4 which is a subtheory of the DOLCE Ontology that captures intuitions about how objects can be present at different points in time. One module is equivalent to Tdolce time mereology5 (which axiomatizes the mereology on temporal regions); the other module consists of the axioms: (8 x) (ED(x) _ PD(x) _ Q(x))
(9 t) PRE(x, t), (8 x, t) PRE(x, t)
T (t). 3Thank you to one of the reviewers, who suggested this example. 4colore.oor.net/dolce_present/dolce_present.clif 5colore.oor.net/dolce_time_mereology/dolce_time_mereology.clif
In addition, there are two axioms which are not contained in any module of
(8 x, t, t1) PRE(x, t) ^ P(t1, t)
PRE(x, t1),
(8 x, t, t1, t2) PRE(x, t1) ^ PRE(x, t2) ^ SU M(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 Twog6 that plays a role in the verification of OWL-Time
[
One module is equivalent to the theory Tpartial bipartite7 and the other module is equivalent to the theory Tbetweenness8. The two sentences
(8 x, 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), (8 x, 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. 6colore.oor.net/ordered_geometry/wog.clif 7colore.oor.net/bipartite_incidence/partial_bipartite 8colore.oor.net/betweenness/betweenness.clif
The notion of reducibility presented in [
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 points9 of time endpoints which relates the notion of linear time points with the notion of time intervals by defining the functions beginof, 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 ordering10 of linear ordering and the theory Tstrict graphical 11 of strict graphical incidence structures.
A strict graphical incidence structure [
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 synonymous with Tlinear ordering and Tstrict graphical . ⇤
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: (8 i) timeinterval(i) be f ore(begino f (i), endo f (i)). (1) 9colore.oor.net/combined_time/endpoints.clif 10colore.oor.net/orderings/linear_ordering.clif 11colore.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.
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:
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 P i and D i such that Ti [ P i and Si [ D i are logically equivalent, and P i ⇢ P and D i ⇢ D . Then we have (⌘ denotes logical equivalence)
T1 [ P 1 [ ... [ Tn [ P n ⌘ S1 [ D 1 [ ... [ Sn [ D n.
Since R is disjoint from T1, ..., Tn, we can say that
S1 [ D 1 [ ... [ Sn [ D n 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 [ D : (8 x) timepoint(x) ⌘ point(x). (8 x) timeinterval(x) ⌘ line(x).
(8 x, y) (begino f (y) = x) ⌘ (8 x, y) (endo f (y) = x) ⌘ (in(x, y) ^ point(x) ^ (x 6= y) ^ (8 z) point(z) ^ in(z, y)) leq(x, z). (in(x, y) ^ point(x) ^ (x 6= y) ^ (8 z) point(z) ^ in(z, y)) leq(z, x).
(8 x, y) be f ore(x, y) ⌘ leq(x, y).
(8 x, 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 .
Reducibility places strong conditions on the relationship between a theory and its modules. 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:
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 [
As we saw with reducibility, the notion of weak reducibility also leads to the identification of a class of modules for a theory:
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 .
T with S (T 0) = S (T ) which is synonymous with S1 [ ... [ Sn. 12
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 nonconservative 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 models 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.
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 [
12Note that by Definition 10, if T is weakly reducible, which is the case in this theorem, then T 0 exists. 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-PNhPysEicDal(Ex)ndurant ideal cem wmg
EEndDu(rxan)ts
PhysPicEalDE(nxd)urant [ ideal cem wmg PePrdDu(rxa)nts [ ideal cem wmg ⌘ dolce present
Qualities Q(x)
Looking more closely at these reductive modules, we can see that they are themselves 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. upper_set
ideal lower_set subposet subposet_root lower_reverse lower_preserve chain_antichain upper_preserve upper_reverse mereology partial_ordering
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 modules 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 ontologies in the subposet hierarchy. 13 The subposet hierarchy is a collection of mathematical ontologies which are developed for verification of spacial an temporal ontologies. The weakest ontology in this hierarchy is constructed by taking the weakest mereology 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.
13A hierarchy is a set of ontologies with the same signature [
For example, the work in [
and Tupper preserve is constructed by adding the following residue axiom to Tmereology [ (8 x, y, z) part(z, x) ^ leq(x, y) leq(z, y).
Notice that both of these two axioms specify the relationship between the parthood relation 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 (8 x, 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
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 reductive modules T1, ..., Tn and residue R. Other ontologies in the hierarchy are obtained by strengthening at least one of T1, ..., Tn, or strengthening R.
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.