In ontology development, modularity has received great attention in the past years; see, e.g., the LNCS monograph [27]. The non-standard reasoning tasks of extracting modules and of decomposing an ontology into modules have manifold applications in ontology reuse, versioning, debugging, and comprehension, as well as collaborative ontology development and automated reasoning optimization. When extracting a single module from a TBox T , that is, a subset M that can be used as a proxy for T , it is crucial for all these scenarios that M encapsulates the knowledge from T about a certain topic, which is usually taken to be a set of terms, the seed signature Σ . This encapsulation is typically captured via the notion of Σ -inseparability [17,2,3,15], which generalizes that of a conservative extension [4,20,13]. However, depending on the application, the widely adopted requirement that M be Σ -inseparable from T is not always suficient. For example, when importing M in place of T into an external TBox, M should even be Σ ′-inseparable from T , where Σ ′ is the union of Σ and the signature of M-this property, called self-containment [18], ensures that M encapsulates the knowledge about all of its own terms, making M a suitable proxy for T w.r.t. those terms rather than just Σ . On the other hand, in scenarios such as optimization of debugging and explanation [26,14] or of reasoning [7,30], M should even preserve all ways to derive the knowledge about Σ (or Σ ′), captured by the notions of M being weakly (strongly) depleting or justification-preserving [18,1,24]. Decomposition aims at computing the modular structure of a TBox-a representative subset of all modules together with their logical interactions. This structure can be used to better understand the TBox, aid its collaborative design, and optimize tool support [9,10]. Among the available techniques, atomic decomposition (AD) [11] stands out by its eficiency and genericness: the underlying algorithm is based on a linear number of module extractions, for a suitable module notion. Originally based on locality-based modules (LBMs) [8], the AD framework was recently shown to work with any module extraction function m that yields uniquely determined Σ -inseparable subsets of the input TBox which satisfy certain module properties, among them self-containment [10]. In recent years, AD has received increased attention [29,21,19] A wide range of module extraction functions and module properties are known [8,16,28,23,12,1,24,6,5,19]. The functions difer in the properties they ensure and, for a given module extraction function m and property P , it is not always obvious
whether m satisfies P . This is particularly so when m is based on some normal
form: e.g., there may be various ways to recover a module of an arbitrary TBox T
from a module of its normalization, thus violating uniqueness and suitability for
AD. Sometimes only weak properties are known, and their strong counterparts
have to be ensured via iteration [
The aim of this paper, which is an extended abstract of our KR 2021 paper
[
We briefly report on our main results. For this, let a module extraction function (MEF) be a (partial) function m(· , · ) that maps a signature Σ (a set of concept and role names) and a TBox T to a subset M of T that is Σ -inseparable from T . For a property P of a single module, we say that an MEF m satisfies P if m(Σ, T ) satisfies P for all Σ and T , e.g., an MEF is depleting if it only yields depleting modules.
First, we conduct a systematic study of the relationships between module properties and we find, amongst others, the following implications. Theorem 1. Let m be an MEF. The following implications hold. 1. If m is monotonic in T , m is justification-preserving; 2. If m is justification-preserving, m is depleting; 3. If m is strongly justification-preserving, m is strongly depleting and selfcontained.
These interrelations yield rigorous, short proofs of properties satisfied by
various module notions. For example, LBMs are obviously monotonic in T ,
substantiating the ‘folklore’ assumption of them being justification-preserving
[
Second, we generalize the iteration process underlying various MEFs, which
ensures self-containment—either inherent to the module extraction process itself
[
Theorem 2. For any MEF m, there is an iterative algorithm that computes a self-contained MEF m+ in linear time with access to an oracle of m. If m is justification-preserving (depleting), m+ is strongly justification-preserving (strongly depleting).
Third, various MEFs depend on the input TBox being normalized [
Title Suppressed Due to Excessive Length
Fortunately, as it is known that denormalization of justification-preserving
and depleting modules is possible [
Fourth, given a MEF that is monotonic in Σ , the above results enable us to construct a ‘repair’ of it that is suitable for computing the AD of a general TBox: Theorem 4. If an MEF m is monotonic in Σ , we can extend m to an MEF m′ that satisfies all properties required to compute the AD of any general TBox. In natural cases, this holds even if the domain of m is restricted to normalized TBoxes.
Finally, we conduct a case study with an existing family of module notions
based on normalization and Datalog reasoning [
Future work should address several theoretical questions and compare AD
based on repaired MEFs with AD based on LBMs [