Modularization for ontologies and thus for logical theories is receiving increasing interest, but a clear presentation of requirements for solutions is still missing. This paper presents a collection of such requirements. Some of these are derived as desiderata in the context of applying modularization to the axiomatization of a top-level ontology, whereas others are determined by analyzing the notion of module in software engineering. Given these requirements, their relationship to current proposals for modularizing ontologies is briefly discussed, with a focus on our application. In a wider context, the paper represents an initial step towards a notion of module for logical languages, which is applicable to the creation and maintenance of large axiomatizations.
Expedited by the Semantic Web in general, and the Web Ontology Language
(OWL) [
Concerning modularization in the context of OWL, the lack of a sophisticated notion of module has already been criticized with its advent, because of the simplicity of means which it provides for combining OWL ontologies. The owl:imports statement is the only available element of OWL to achieve a 1 In all cases of referring to OWL, we actually refer to OWL-DL which corresponds closely to the description logic SHOIN (D) (see [9, p. 27–32] for a clear presentation of minor differences between these two, which are irrelevant for this paper). syntax-level splitting of ontologies. The semantics of this statement corresponds to a simple union of the axioms of the importing ontology and the imported ones, which is insufficient for supporting modularized ontologies.
The specific background for our interest in logical modularization is given
by the development of the top-level ontology General Formal Ontology (GFO)
[
Among other purposes, this can support the evaluation of existing approaches.
Indeed, some extensions for OWL and other logical languages have been
proposed which offer ways for modularizing theories (for example, [
The overall structure of the paper is as follows. Firstly, we collect our desiderata for modules, which arise directly from working with logical formalisms, in section 2, preceded by a short introduction to the application setting. In section 3, further requirements are obtained by considering the notion of module in software engineering. Section 4 presents a brief analysis of the properties of current proposals in relation to our requirements, before the paper concludes with the fifth section.
A note on the formal setting is due. Much of what follows is independent of a particular logic, like first order logic (FOL) or any specific description logic (DL). We refer to a logic L as a triple L = (L, M, |=) of a language L, understood as a set of sentences2, a set of model structures M , and a satisfiability relation |= ⊆ M × L between model structures and sentences. By standard definitions, the latter generalizes to model and consequence relations between models, model classes, and theories, all of which are likewise denoted by |=. Cn(T ) denotes the deductive closure of T . Grammatical definitions of a language L usually distinguish sentence constructions and a vocabulary/signature V . We sometimes speak of the same language even for different vocabularies, and L(V ) denotes all sentences which can be built from V in a given grammatical framework. Any subset T ⊆ L(V ) is called a theory. The vocabulary of T is denoted by V (T ), the corresponding language is L(T ) =df L(V (T )). 2 We are not interested in formulas with free variables in the case of a language with variables.
The current axiomatization of the General Formal Ontology (GFO) comprises about three hundred sentences in FOL, circa one hundred of which are explicit definitions. These are roughly organized into axiomatic fragments with respect to several topics in GFO, like Time, Space, Part-of Relations, etc. This organization is useful for analyzing the resulting theories with respect to their logical properties, most prominently consistency and completeness. However, statements about the system of these fragments, seen as a single theory, are hard to make in the case of FOL, because the vocabularies of these fragments overlap.
In the current situation, one may view these fragments as modules, which
should be combined in a sensible manner. Note that in general, given some
notion of module, two kinds of usage become available, namely composition and
decomposition. Composition refers to studying the relation between a module
and a system built from several modules, whereas decomposition starts with a
theory or system and tries to determine an “appropriate” collection of modules.
The latter is often called “partitioning” in recent approaches [
Another view on GFO is as a ready-made component for the development of domain ontologies, so that GFO as a whole appears as a module of domain ontologies. Under this perspective, GFO should behave like a logical theory in order to fit formalizations of domain ontologies.
According to these views one can distinguish two kinds of modules (or even logics). Modules in the first sense are called basic modules, and their core component is some theory T ⊆ L, usually provided as a finite axiomatization in a language L. Given a number of basic modules (Ti)i∈I (where I is an arbitrary index set), these can be combined into a system S. Such a system may serve itself as a complex module for a larger system. If the applied combination operation departs from set-theoretical union, this yields potentially different logics for basic and complex modules. Let us assume that all basic modules Ti adhere to a common logic L = (L, M, |=bas ), where L = L Si∈I V (Ti) . Even then the composition operation for creating S out of the Ti may form a new kind of entailment and hence a different logic for S, L0 = (L0, M 0, |=comp ), with respect to which S represents a theory S ⊆ L0 ⊇ L. 2.2
With this general setting in mind, we formulate and discuss the following requirements for logical modules. At this stage, we do not impose any pre-established constraints on ourselves with respect to feasibility, computability, or the question of whether a single, formal notion of module can satisfy all of them. In this sense, the following is to be seen as a collection of desiderata, rather than a set of requirements which must be met necessarily.
a system S composed of modules should provide the information contained
explicitly in its modules. If S is composed of basic modules (Ti)i∈I , this requires
S |=comp φ for every φ ∈ Ti, for all i ∈ I. A strengthening of this requirement
would also include implicit information, replacing φ ∈ Ti above by Ti |=bas φ.
This is called local correctness in [
For instance, S should satisfy the deduction theorem (in case of a classical logic being used for its basic modules; or an equivalent for other kinds of logics). If it does not, assume that S |=comp φ and S |=comp φ → ψ, but S 6|=comp ψ. A classical system querying S and receiving φ and φ → ψ could then derive ψ, which is in conflict with S. The requirement means to avoid such situations for arbitrary classical deductions.
Directionality Composition should allow for a directed information flow among
modules, such that a module may use another without having an impact on it.
This requirement is motivated by the second use case from above, where a domain
ontology is based on a top-level ontology. Of course, one would not want effects
from the domain ontology to be transferred to the top-level ontology (in the
worst case, causing inconsistency where there was none). Formally, if T1 and T2
are components of S and composition assures a directed information flow from
T1 to T2 within S, then T2 may take sentences from T1 into account, but not
vice versa. A very similar requirement is stated in [
Comprehensibility A module should remain “comprehensible”, with the purpose of supporting maintainability. Two options in order to achieve this for basic modules are (a) to have a rather small vocabulary and small set of axioms of arbitrary form, or (b) to have a possibly large, structured vocabulary equipped with only simple axioms, which furthermore follow one or a few common schemes. For complex modules, comprehensibility should derive from the way they are composed of basic modules.
Stability A system composed of modules should remain stable if a single module
evolves, or loosely related modules are added. Especially, the system structure
should remain stable, i.e., the addition of a module does not change the
previously established structure among other modules. Furthermore, side effects of
evolution should be reduced to a minimum. This criterion has also been proposed
in [
These requirements arise naturally in our application setting. We are aware of
the fact that most of them have been mentioned in different circumstances, as
indicated according to our knowledge. Distributed First Order Logic (DFOL)
[
Concerning the interrelations among these requirements, one can already notice that there are some which are likely to prevent attempts to satisfy all of them. For example, directionality is a requirement which interferes with local correctness and completeness as well as classically closed composition. For example, let S answer queries in L(T1) only by means of its module T1, but queries in L(T2) ⊃ L(T1) by means of T1 ∪ T2. This can easily create a situation where S loses classically closed composition, e.g., by no longer satisfying the deduction theorem. Local correctness and completeness are problematic even without other requirements. Both conditions are very restrictive, and the question arises whether a non-trivial composition operation can be found, which is different from set-theoretical union but satisfies local correctness and completeness.
Based on these requirements, one could now start to develop a notion of module. However, so far this is rather an ad hoc collection of requirements. In order to put the overall approach onto firmer ground, we will next consider the notion of module in software engineering. 3
The reason for considering software engineering as an appropriate source relies on the assumption that the development of large axiomatizations in some aspects resembles software engineering, where we have come to this view based on our current experiences. Moreover, modules and modularization have proved as concepts of much success in software engineering. Note that a broad reading of module applies here, because several specialized fields have created their own basic notions which contain the general idea of modularization, e.g., “object” in object-oriented approaches, or “component” in component-based software development. 3.1
Starting with some general definitions, Siedersleben defines a module as “a closed
software unit with a well-defined interface”, which forms “the smallest unit of
software design” [28, p. 97, own translation]. He refers to [
Given this general characterization, interface and service form two central elements of modules in software engineering, which should be migrated to a logical understanding. The immediate services a logical module could provide are reasoning services. For example, [4, primarily ch. 1] mentions some reasoning types for description logics, like concept inclusion, concept satisfiability, or consistency checking. However, in this generality, it seems hard to fix an analogue for the notion of interface. In the sequel we therefore focus on answering entailment queries, i.e., queries of the form T |= φ. This is the most relevant kind of query for our application purpose, and several other query types can be reduced to it (in many logics).
For the entailment service, a number of options for defining an interface of a theory T ⊆ L appear. Two general approaches would be to view an interface either as a query language Q ⊆ L, or, considering the set of answers, again as a theory. The query language approach allows for restrictions of both, the language grammar as well as the vocabulary. A special case of this is to just restrict the language by means of the vocabulary, i.e., to use a subset V 0 ⊆ V (T ) of the given vocabulary as interface specification. The theory-based understanding of interface is even more general. It can integrate the query language approach by defining T 0 =df Cn(T ) ∩ Q, but it may also allow for transformations of the formulas of T . Currently, for reasons of comprehensibility and for simplicity of specification, we advocate the query language view of what a logical interface should be. Independent of this choice, a theory may provide several such interfaces, like in software engineering.
The notion of a body degenerates to some extent in the declarative setting, where a dynamics like program execution is missing or at least not more informative than the semantics. In the query language view, the overall theory appears as the body, which at least allows for information hiding (see below). 3.2
There are some key features of modules in software engineering (cf., for instance,
[
faces over which they communicate and the interface is the only way to communicate. Apart from that the module comprises a body which is accessed only internally by a module.
This feature has already been covered by the above discussion of
interpretations of “interface”. In the query language approach to interfaces, communication
between modules means that one module queries another in a query language
provided by the latter. This is very similar to the message passing metaphor
between theories employed in [
information handling is hidden for other modules. Therefore, a module provides encapsulated functionality and / or data.
It depends on the relation between the language L(T ) of a module T and the query language Q, serving as interface, to what extent information hiding and visibility are realized. A problem with this feature is that it is not clear, in a declarative setting, why some aspects of a theory should be generally hidden. That is, why should certain vocabulary elements appear in no interface for T ? With respect to a single interface, it is useful to think of information hiding and encapsulation. For example, given a top-level ontology TT LO, one may be interested to use just the theory of time built into it, so let TT LO |= TT ime. For this purpose, TT LO may provide L(TT ime) as a time interface. With our stability criterion in mind, changes to the top-level ontology must be transferred to some domain ontology which uses TT ime only then if they affect the service accessible via the time interface.
Let us now consider the case of multiple interfaces. In general, a theory T with a number of logical interfaces defined by means of query languages Q1, . . . , Qn yields a family of theories, namely (Cn(T ) ∩ Qi)1≤i≤n. Note that these theories cannot by default be seen as modules of T themselves, because two such theories may be related in arbitrary ways with respect to entailment, in dependence of the relations among the Qi. In software engineering, this freedom is constrained for modules by means of the next criterion.
Independence The tasks a module has in the overall architecture are (to an appropriate degree) independent from those of other modules.
With respect to the entailment service, which means to answer queries in a specific language, we interpret this in such a way that different modules answer questions with respect to different “topics”, which is naturally reflected by the use of different languages. Starting with the grammar level, it is not obvious to us how differences among the grammar would capture this criterion well. In contrast, different vocabularies can reasonably be seen to refer to different topics. A clear but strong notion of independence would require different vocabularies to be disjoint. However, less restrictive interpretations will be needed to achieve communication among modules.
It is important to note two axes of vocabulary differences, regarding the ontological relations of the intended meaning of the vocabulary elements. Horizontally (the term borrows from a hierarchical image of taxonomies), two vocabularies may be concerned with distinct concepts in the sense that those concepts do not share any instances. Trees, walks, and numbers are distinct in this reading. In contrast, the vertical axis relates to the generality of notions. For instance, vocabularies of top-level and domain ontologies are usually disjoint, but top-level concepts classify the same entities referred to by domain entities. For predicate logics and description logics, these types of differences interact with the corresponding model structures, if these languages are used in a way which allows for an ontological interpretation of relations between entities in model structures. For example, predication may reflect instantiation. OWL, in particular, is exposed to this problem because of its very nature as an ontology language. Accordingly, modularization approaches based on or with specific effects on model structures should be examined for implications on the contents expressed ontologically (see also section 4.1). In general, a solution for modularization which handles both types of differences appears to be preferable over another dealing with only one of them.
Due to interfaces as query languages, we have provided a language-oriented interpretation of independence for modules. Another approach could consider reasoning inside modules to be independent, rather than the languages used. However, complete independence would then mean to not exchange any formulas. Otherwise, the communication of formulas from one module to another creates interdependences of reasoning. Hence, we claim that a better analogue for this is interaction among modules rather than independence. Of course, interaction is likewise observed in software engineering, and constrained for modules by the subsequent characteristic.
Cohesion vs. coupling Modules should behave differently regarding cohesion and coupling. Cohesion refers to interconnections within a module, whereas coupling names interconnection among modules. Cohesion should be maximized in modules, coupling minimized.
Sentences in a logical theory may have an impact concerning entailments on each other, without any structural restrictions. This can be understood as cohesion. Combining theories by set-theoretical union yields a theory whose sentences are in the same way closely interconnected. Thus, this form of composition does not adopt the distinction between cohesion and coupling. Compared to our requirements above, directionality can be seen as a means to achieve a notion of coupling.
a module of equal character (i.e. which supports the same functionality) without unexpected side-effects concerning coupled modules and the overall system. In practice, usually some restrictions apply to the ideal case.
Given the query-language view of interface, “equal character” would literally mean that a substitute module T 0 provides the same answers to queries in Q as the original module T . Accordingly, this criterion can be met perfectly even by standard theories, yet for a seemingly uninteresting special case. Logically equivalent axiomatizations, i.e., given Cn(T 0) ∩ Q = Cn(T ) ∩ Q, would form distinct modules which are perfectly interchangeable without any side-effects. However, due to the fact that composition may yield a different form of entailment, this depends on the inclusion requirements. For example, the above equation may fail for a system comprising T , and later T 0, if only the inclusion of explicit information is provided.
Another relevant case regards multiple interfaces: one may refer “equal character” to a single interface. Returning to the time-example, TT ime may remain constant while TT LO is changed in some other respects. Again, this connects to our stability requirement.
There are further features, like readability, reuse status, or separate editability, which do not contribute as much to an understanding of “module” as those we have discussed so far. What can be observed is that there is hardly any overlap between our ad hoc requirements and those transferred from software engineering. By no means should this be interpreted negatively for the latter. Instead, implicit assumptions could be explicated by this approach. With a more profound set of requirements available, we can now start to evaluate the adequacy of related work for our purposes. 4
Modularization of logical theories is a rather young research interest, but it is
related to a number of fields which seem to provide good starting points. The
most direct approaches to modularization we are aware of and which moreover fit
the context of logic-based ontologies are that of Bernardo Cuenca Grau and
colleagues [
This approach was initially based on ε-connections [
The semantic encapsulation approach started as an application of
ε-connections to combining ontologies based on description logics [
Nevertheless, it still shares a central feature with the ε-connections method,
for a certain class of SHOIQ theories: [
This property has an effect which we find problematic, all the more against
our background of developing a top-level ontology: given a domain ontology
which can be modularized according to [
Nevertheless, [
The goals of this approach are to support reasoning over multiple theories with
overlapping content and vocabularies, as well as the improvement of the efficiency
of reasoning by means of partitions. [
Neglecting the algorithmic details of [
Moreover, a decomposition algorithm is presented in [
Taking partitions as modules and set-theoretical union as the composition operation, this approach satisfies inclusion of explicit information and classically closed composition. The intersection languages for message passing correspond properly to a specific type of interface specification. Moreover, the decomposition approach minimizes coupling, module size, and the number of modules, which is adequate also according to our setting. However, having union as composition is rather weak and prevents directionality. Therefore, utility for our purposes is primarily seen in the decomposition algorithm, similarly to semantic encapsulation. 4.3
This branch comprises works of Luciano Serafini et al. on developing Distributed
First Order Logic (DFOL) [
The major idea of LMS/ MCS, which conveys to the more recent approaches, is to have a collection of theories (possibly in different logical systems) each of which is first of all interpreted locally, i.e., with respect to the semantics of its associated logic. On top of this, bridge rules specify interconnections among these theories, i.e., given T1 and T2, a bridge rule is a pair (φ, ψ) with φ ∈ L(T1), ψ ∈ L(T2), which states that T1 |= φ allows one to assume ψ in T2.
The distributed logic approach is compositional rather than decompositional,
and it is equipped with a non-trivial composition operation, because bridge rules
provide directionality. Therefore, it appears to match some of our needs better
than the previous approaches, which are oriented towards decomposition. This
impression is further augmented by considering the list of properties required
for DFOL in [
Certainly the most prominent approach aiming at reasoning and structuring
theories, which has not been discussed here, is the solution provided for structuring
the CYC knowledge base [
Another line of research provides less logic-oriented approaches for
decomposing ontologies, among them [
Modularization is about to attract focused research interests, in particular with respect to formal logical approaches. However, requirements, i.e., clearly defined properties which a solution should satisfy are rarely provided. In this paper, we introduce and discuss a collection of requirements for modules/ modularization in logical settings, on a fairly language-independent level. On the one hand, these requirements are motivated directly from an application perspective, which involves the manual construction and maintenance of large axiomatizations. On the other hand, we hold that these tasks bear analogy to software engineering, and therefore we study a logical interpretation of requirements for modules in that field. The overall set of requirements is best understood as a catalog of properties – nevertheless, not meant to be complete – which can be used to analyze existing proposals, as briefly exemplified for three approaches, or to guide the design of new work on modularization.
There are three major conclusions which we draw from the discussion of the requirements. Firstly, the theory of modules in software engineering has turned out to be useful for our purposes. By means of this analysis we have identified a number of requirements which are applicable and desirable in the logical case, and which have not had much overlap with those requirements specified on an ad hoc basis. So these form a useful extension of our initial list.
Secondly, in the course of the discussion it has become clear that some of the requirements will hardly be implemented by a single approach to modularization. In particular, the requirements of local correctness and completeness, classically closed composition, independence, and directionality form an area of conflict. Note that this applies independently from the actual logical framework. Accordingly, we feel that a unique solution to modularization will remain insufficient, but specialized methods should be applied in dependence on the intended application.
Thirdly, it seems that the requirement of compositionality has not been taken into account thus far. Admittedly, of those properties presented, this one is certainly the one which is closest to be termed “wishful thinking”, especially if local correctness and completeness should be maintained. However, compositionality would be very beneficial, and there may be ways to achieve it if certain other requirements must be abandoned anyway, as part of some trade-off.
The presented requirements analysis is just an initial step for further work on, ultimately, implementing the top-level ontology GFO in a modular way. A direct continuation of this paper would be a more formal analysis of the interrelations of those requirements that can be captured formally, as well as relating them to properties of the logical system used. Moreover, the paper is a starting point for work on modularization which provides compositionality. In a longer term, one may consider extensions to different logics used for the modules (similar to the general LMS/ MCS approach), hence moving to hybrid logics. In this direction, the lack of a natural “reference logic”, with which the resulting systems could be compared, forms another interesting topic, which we further consider to relate back to ontology, here as a source of justification.