We present a method for extracting general modules for ontologies formulated in the description logic ℒ. Given an ontology and a signature Σ of concept and role names, a general module is an ideally substantially smaller ontology that preserves all ℒ axioms that are entailed by and can be expressed using only the names in Σ. As such, it has applications such as ontology reuse and ontology analysis. In particular, if we want to reuse only a part of an ontology in a new application, rather than using the entire ontology, we may first want to extract a general module for the set of terms that are actually relevant for the application. General modules may also serve as a restricted view of the ontology, focused on a small set of terms of interest, which may make hidden relations between the terms visible. While classical modules have the additional requirement that they are a subset of the original ontology, general modules can also reformulate axioms from the input ontology, which can lead to smaller results that are more focused on the provided signature, and thus potentially better suited for the aforementioned applications. Another special case of general modules are uniform interpolants, which are general modules that are complete formulated using only names from the provided ontology. We believe that for application such as ontology reuse, this requirement is in fact too strict and can even be counter-productive. However, so far, general modules have only been investigated for lightweight description logics [1, 2]. Our main contributions are: 1) we present the first method dedicated to computing general modules in ℒ, 2) we provide a formal analysis of some properties of the general modules we compute, 3) based on our methods, we also obtain new methods for computing classical modules and uniform interpolants, and 4) using an evaluation on real-world ontologies we demonstrate the eficiency of our technique. This work has been accepted by IJCAI 2023. For detailed results and proofs, please refer to the extended version of the paper [3]. The main steps of our approach are shown in Figure 1. Essentially, our method works by performing uniform interpolation on a normalized version of the input ontology, inspired by the uniform interpolation method presented in [4]. Our normalization introduces fresh concept names, called definers , which are eliminated in the final step. However, diferent from [4], we put fewer constraints on the normal form and do not allow the introduction of
Role Isolation
RIΣ
Role Forgetting rolEΣ
Concept Forgetting conEΣ
Definer Substitution/ Forgetting
General Module: gmΣ, gm*Σ Deductive Module: dmΣ
Uniform Interpolant
definers after normalization. As a result, our definer elimination step may reintroduce names
eliminated during uniform interpolation. This is not a problem, since our aim is not to compute
uniform interpolants of the input ontology. In contrast, eliminating definers as done in [
Ontology Normalization form:
An ontology is in normal form if every axiom is of the following ⊤ ⊑ 1 ⊔ . . . ⊔
::= | ¬ | Q., Q ∈ {∀, ∃}.
For simplicity, we omit the “⊤ ⊑” on the left-hand side of normalized axioms. As an example, the axiom 2 ⊑ 3 ⊔ ∀.3 is equivalent to ¬2 ⊔ 3 ⊔ ∀.3 in normal form.
As the first step, we normalize the input ontology using standard transformations. In
particular, we replace every concept occurring under role restrictions by a so-called definer
name . For each definer , we remember the concept that was replaced by it.
Role Forgetting Next, we apply role forgetting to eliminate role names outside the given
signature Σ. Existing methods to compute role forgetting either rely on an external reasoner
[
Theorem 1. Let rolEΣ() be the ontology obtained as follows: 1. apply the r-Rule in Figure 2 exhaustively for each ∈ sigR() ∖ Σ, 2. remove all axioms containing some ∈ sigR() ∖ Σ.
If is role isolated for Σ, then rolEΣ() is a role-forgetting for and Σ.
Concept Forgetting Inspired by [7, Theorem 1], we define a concept forgetting operator conEΣ using A-Rule in Figure 2 in a similar way as defining rolEΣ. Applying the aforementioned procedure yields conEΣ(rolEΣ(RIΣ())), which contains only of names in the signature Σ or definers.
r-Rule : A-Rule : 1 ⊔ ∃.1, ⋃︀
=2{ ⊔ ∀.}, 1 ⊔ . . . ⊔ 1 ⊔ 1 ¬1 ⊔ 2 1 ⊔ 2 , = ⊔1≤ ≤ ¬ or ⊔2≤ ≤ ¬ Constructing the General Module To obtain our general modules gmΣ() for and Σ, we eliminate the introduced definers from conEΣ(rolEΣ(RIΣ())). For this, we replace each definer by , the concept replaced by in the normalization step.
Eliminating definers in this way may reintroduce previously forgotten names, which is why
our general modules are in general not uniform interpolants. This way, we avoid the triple
exponential blow-up caused by uniform interpolation in the worst case [
Proposition 1. For any ontology and signature Σ, we have ‖gmΣ()‖ ≤ 2(‖cl()‖). On the other hand, there exists a family of ontologies and signatures Σ s.t. ‖‖ is polynomial in ≥ 1 and ‖gmΣ ()‖ = · 2(‖cl()‖).
Optimized General Modules To obtain smaller general modules, we eliminate some definers
before substituting them, using an operation inspired by [
Deductive Modules and Uniform Interpolants Our method can also be used to compute
classical modules, which we do by tracing the inferences performed when computing the general
module gm*Σ(). For applications that instead require uniform interpolants, such as logical
diference [
Evaluation We evaluated our methods on 222 ontologies from the OWL Reasoner Evaluation
(ORE) 2015 classification track [ 13], from which we removed axioms not expressible in ℒ.
For each ontology, we randomly generated 50 signatures consisting of 100 concept and role
names as in [
We implemented a prototype called GeMo1 in Python 3.7.4. For each request (, Σ), GeMo
produced two types of general modules (gm and the optimized gm* ), a classical module (dm), as
well as a uniform interpolant (gmLethe). To show that our general modules can serve as a better
alternative for ontology reuse and analysis, we compared them with the state-of-the-art tools
implementing module extraction and uniform interpolation for ℒ: (i) ⊤⊥* -modules [14] as
implemented in the OWL API [15]; (ii) minM [
• Success rate: We say a method succeeds on a request if it outputs the expected results within 600s. Table 1 summarizes the success rate for the methods considered. After the ⊤⊥* -modules, GeMo had the highest success rate. • Resulting ontology length and run time: We used ontology length, which is the sum of the sizes of the axioms in the ontology, as metric. Table 2 shows the length and run time for the requests on which all methods were successful (78.45% of all requests). We observe that our optimization gm* was efective, and lead to almost the best length in median, only being improved by gmLethe, which however had longer run times. While our modules were generally smaller than what was computed by the state-of-the-art, run-times could almost compete with that of ⊤⊥* -module-modules.
Conclusion The experiments validate the eficiency of our proposal and the quality of the computed general modules. In the future, we want to optimize the concept elimination step to obtain more concise general modules. Also, we would like to investigate how to generalize our ideas to more expressive description logics. 2https://lat.inf.tu-dresden.de/~koopmann/LETHE/ 3http://www.cs.man.ac.uk/~schmidt/sf-fame/ Conference, KR 2014, AAAI Press, 2014. URL: http://www.aaai.org/ocs/index.php/KR/ KR14/paper/view/7985. [12] Y. Zhao, R. A. Schmidt, FAME: an automated tool for semantic forgetting in expressive description logics, in: International Joint Conference on Automated Reasoning, Springer, 2018, pp. 19–27. [13] B. Parsia, N. Matentzoglu, R. S. Gonçalves, B. Glimm, A. Steigmiller, The OWL reasoner evaluation (ORE) 2015 competition report, J. Autom. Reason. 59 (2017) 455–482. URL: https://doi.org/10.1007/s10817-017-9406-8. doi:10.1007/s10817-017-9406-8. [14] B. C. Grau, I. Horrocks, Y. Kazakov, U. Sattler, Modular reuse of ontologies: Theory and practice, Journal of Artificial Intelligence Research 31 (2008) 273–318. [15] M. Horridge, S. Bechhofer, The OWL API: a java API for OWL ontologies, Semantic Web 2 (2011) 11–21. URL: https://doi.org/10.3233/SW-2011-0025. doi:10.3233/SW-2011-0025.