Efficient Computation of General Modules for ALC Ontologies

1 Introduction

Ontologies are used to formalize terminological knowledge in many domains such as biology, medicine and the Semantic Web. Usually, they contain a set of statements (axioms) about concept and role names (unary and binary predicates). Using a formalization based on description logics (DLs) allows DL reasoners to infer implicit information from an ontology. Modern ontologies are often large and complex, which can make ontology engineering challenging. For example, as of 3 January 2023, the medical ontology SNOMED CT [Donnelly and others, 2006], used in the health-case systems of many countries, formalizes over 360,000 concepts, and the BioPortal repository of ontologies from the bio-medical domain [Noy et al., 2009] currently hosts 1,043 ontologies that use over 14 million concepts. Often, one is not interested in the entire content of an ontology, but only in a fragment, for instance if one wants to reuse content from a larger ontology for a more specialized application, or to analyse what the ontology states about a given set of names. In particular, this set of names would form a signature Σ, got which we want to compute an ontology M that captures all the logical entailments of the original ontology O expressed using only the names in Σ. Our aim is to compute such an M that is as simple as possible, in terms of number and size of axioms. This problem has received a lot of attention in the past years, and for anMsatisfying those requirements, the common approaches are modules and uniform interpolants.

Modules are syntactical subsets of the ontology O that preserve entailments within a given signature. There is a variety of notions of modules and properties they can satisfy that have been investigated in the literature [Grau et al., 2008; Konev et al., 2009]. Semantic modules preserve all models of the ontology modulo the given signature Σ. This makes them undecidable already for light-weight DLs such as EL [Konev et al., 2013], which is why existing methods often compute approximations of minimal modules [Gatens et al., 2014; Romero et al., 2016]. A popular example are locality-based modules, which can be computed in a very short time [Grau et al., 2008]. However, locality-based modules can be comparatively large, even if the provided signature is small [Chen et al., 2014]. In contrast to semantic modules, deductive modules are decidable, and focus only on entailments in Σ that can be expressed in the DL under consideration. Practical methods to compute them are presented in [Koopmann and Chen, 2020; Yang et al., 2023b]. However, while those modules is often half the size of the locality-based modules, for the more expressive DL ALC, those methods are timeconsuming, and can also not always guarantee minimality. An approximation of modules are excerpts, whose size is bounded by the user, but which may not preserve all entailments in the given signature [Chen et al., 2017].

Since modules are always subsets of the original ontology, they may use names outside of the given signature. Uniform interpolants (UIs), on the other hand, only use names from the provided signature Σ, and are thus usually not syntactical subsets of the input ontology. This makes them useful also for applications other than ontology reuse, such as for logical difference [Ludwig and Konev, 2014], abduction [DelPinto and Schmidt, 2019], information hiding [Grau, 2010], and proof generation [Alrabbaa et al., 2020]. The strict requirement on the signature means that UIs may not always exist, and, in case of ALC, can be of a size that is triple exponential in the size of the input [Lutz and Wolter, 2011]. Despite this high complexity, practical implementations for computing UIs exist [Zhao and Schmidt, 2018; Koopmann, 2020]. However, their computation times are much higher than for module extraction and can produce very complex axioms.

Both modules and UIs can be more complex than necessary. By dropping the syntactical requirements of those notions-being subsets of O and being within Σ respectively-we may obtain ontologies that are both smaller and simpler, and yet still preserve all relevant entailments, which would make them better suited for ontology reuse and analysis. In this paper, we present a method to compute such general modules, which are indeed often smaller and nicer than the corresponding classical modules and UIs. Our method can indeed also compute deductive modules and UIs, and does so in significantly shorter time than the state-of-theart. While general modules have been investigated for the lightweight DLs EL and ELH [Nikitina and Glimm, 2012; Alghamdi et al., 2021], to our knowledge, this is the first time they are investigated for ALC.

The main steps of our approach are shown in Figure 1. Our method essentially works by performing uniform interpolation on a normalized version of the input ontology (Section 3). During normalization, so-called definer names are introduced, which are eliminated in the final step.This idea is inspired by the method for uniform interpolation in [Koopmann, 2020]. However, different from this approach, we put fewer constraints on the normal form and do not allow the introduction of definers after normalization, which changes the mechanism of uniform interpolation. As a result, our definer elimination step may reintroduce names eliminated during uniform interpolation, which is not a problem for the computation of general modules. In contrast, eliminating definers as done in [Koopmann, 2020] can cause an exponential blowup, and introduce concepts with the non-standard greatest fixpoint constructor [Calvanese and De Giacomo, 2003].

A particular challenge in uniform interpolation is the elimination of role names, for which existing approaches either rely on expensive calls to an external reasoner [Zhao et al., 2019; Koopmann, 2020] or avoid the problem partially by introducing universal roles [Zhao and Schmidt, 2017; Koopmann and Chen, 2020], leading to results outside ALC. A major contribution of this paper is a technique called role isolation, which allows to eliminate roles more efficiently, and explains our short computation times (Section 4).

Our evaluation shows that all our methods, including the one for uniform interpolation, can compete with the run times of locality-based module extraction, while at the same time resulting in subtantially smaller ontologies (Section 7).

Our main contributions are: 1) the first method dedicated to general modules in ALC, 2) a formal analysis of some properties of the general modules we compute, 3) new methods for module extraction and uniform interpolation that significantly improve the state-of-the-art, 4) an evaluation on realworld ontologies indicating the efficiency of our technique.

For detailed proofs of the results, please refer to the extended version of the paper [Yang et al., 2023a]. A prototype of our method can be found at https://hub.docker.com/r/ yh1997/demo gemo.

2 Preliminaries

We recall the DL ALC [Baader et al., 2017]. Let NC={A,B, . . .} and NR = {r, s, . . .} be pair-wise disjoint, countably infinite sets of concept and role names, respectively. A signature Σ ⊆ NC ∪ NR is a set of concept and role names. Concepts C are built according to the following grammar rules.

For simplicity, we identify concepts of the form ¬¬C with C. In this paper, an ontology O is a finite set of axioms of the form C ⊑ D, C and D being concepts. We denote by sig(O)/sig(C) the set of concept and role names occurring in O/C, and we use sig C (∗)/sig R (∗) to refer to the concept/role names in sig(∗). For a signature Σ, a Σ-axiom is an axiom α s.t. sig(α) ⊆ Σ.

An interpretation I=(∆I , ·I ) consists of a non-empty set ∆I and a function ·I mapping each A ∈ NC to AI ⊆ ∆I and each r ∈ NR to rI ⊆ ∆I ×∆I . The interpretation function ·I is extended to concepts as follows:

An axiom C ⊑ D is satisfied by an interpretation I (I |= C ⊑ D) if C I ⊆ DI . I is a model of an ontology O (I |= O) if I satisfies every axiom in O. O entails an axiom α if I |= α for every model I of O. If α holds in every interpretation, we write |= α and call α an tautology.

The length |∗| of concepts and axioms is defined inductively by |⊤| = |A| = 1, where A ∈ NC, |C⊔D| = |C⊓D| = |C ⊑D| = |C| + |D|, |∀r.C| = |∃r.C| = |C| +1, and |¬C| = |C|. Then, the length of an ontology, denoted ∥O∥, is defined by ∥O∥= ∑α∈O |α|.

A central notion for us is (deductive) inseparability [Konev et al., 2009; Koopmann and Chen, 2020]. Given two ontologies O1 and O2 and a signature Σ, O1 and O2 are Σinseparable, in symbols O1 ≡Σ O2, if for every Σ-axiom α, O1 |= α iff O2 |= α. In this paper, we are concerned with the computation of general modules, defined in the following.

Definition 1 (General module). Given an ontology O and a signature Σ, an ontology M is a general module for O and Σ iff (i) O ≡Σ M and (ii) O |= M.

Every ontology is always a general module of itself, but we are interested in computing ones that are small in length and low in complexity. Two extreme cases of general modules are uniform interpolants and deductive modules.

Definition 2 (Uniform interpolant & deductive module). Let O be an ontology, Σ a signature, and M a general module for O and Σ. Then, (i) M is a uniform interpolant for O and Σ if sig(M) ⊆ Σ, and (ii) M is a deductive module for O and Σ if M ⊆ O.

3 Ontology Normalization

Our method performs forgetting on a normalized view of the ontology, which is obtained via the introduction of fresh names as in [Koopmann, 2015]. An ontology O is in normal form if every axiom is of the following form:

where A ∈ NC, and Q ∈ {∀, ∃}. We call the disjuncts Li literals. For simplicity, we omit the "⊤ ⊑" on the left-hand side of normalized axioms, which are regarded as sets, in order to avoid dealing with duplicated literals and order. As an example, the axiom A2 ⊑ A3 ⊔ ∀s.B3 is equivalent to ¬A2 ⊔ A3 ⊔ ∀s.B3 in normal form.

We assume a function cl that normalizes O usind standard transformations (see for example [Koopmann, 2015]). In particular, cl replaces concepts C occurring under role restrictions Qr.C by fresh names D taken from a set ND ⊆ NC \ sig C (O) of definers. We use D, D′ , D1, D2, . . . to denote definers. For each introduced definer D, we remember the concept CD that was replaced by it. We assume that distinct occurrences of the same concept are replaced by distinct definers. Thus, in the resulting normalization of O denoted cl(O), every literal Qr.D satisfies D ∈ ND, and for every D ∈ ND, cl(O) contains at most one literal of the form Qr.D. Every definer D has to occur only in literals of the form ¬D or Qr.D, that is, positive literals of the form D are not allowed. Obviously, we require cl(O) ≡sig(O) O.

Example 1. Let O be the ontology defined in the first row of Table 1. By normalizing O, we obtain the set cl(O) shown in the second row of Table 1. The definers D1, D2 and D3 in cl(O) replace the concepts CD1 = ∃s.B1, CD2 = B1 and CD3 = B2, respectively.

For a fixed normalization, we define a partial order ⪯d over all introduced definers, which is defined as the smallest reflexive-transitive relation over ND s.t.

Intuitively, D′ ⪯d D whenever CD′ is contained in CD. In Example 1, we have D2 ⪯d D1, since ¬D1⊔∃s.D2 ∈ cl(O). Our normalization ensures that ⪯d is acyclic.

In the following, we assume that the ontology O and the signature Σ do not contain definers, unless stated otherwise.

4 Role Forgetting

An ontology M is called a role forgetting for O and Σ iff M is a uniform interpolant for O and Σ′ = Σ ∪ sig C (O). Existing methods to compute role forgetting either rely on an external reasoner [Zhao et al., 2019; Koopmann, 2020] or use the universal role ∇ [Zhao and Schmidt, 2017; Koopmann and Chen, 2020]. The former approach can be expensive, while the latter produces axioms outside of ALC. The normalization allows us to implement a more efficient solution within ALC, which relies on an integrated reasoning procedure and an additional transformation step that produces so-called role isolated ontologies.

4.1 Role Isolated Ontologies

The main idea is to separate names A ∈ NC that occur with roles outside of the signature, using the following notations.

Definition 3 (Role-isolated ontology). An ontology O is role isolated for Σ if (i) O is in normal form, and (ii) every axiom α ∈ O is of one of the following forms:

Thus, an axiom in a role isolated ontology falls into two disjoint categories: either (c1) it contains literals built only over concepts in OutΣ(O) or (c2) it contains role restrictions or literals built over concepts outside OutΣ(O).

Figure 2: Inference rules for computing DΣ(O)

Example 2 (Example 1 cont'd). For Σ = {r, A1, A2, A3, A4}, we have OutΣ(cl(O)) = {D2,D4}. cl(O) is not role isolated for Σ because of ¬D2 ⊔ B1.

Given an ontology, we compute its role isolated form using the following definition.

Definition 4. The role isolated form RIΣ(O) of O is defined as RIΣ(O) := clΣ(O) ∪ DΣ(O), where

• clΣ(O) ⊆ cl(O) contains all α ∈ cl(O) s.t. if ¬D is a literal of α, then Rol(D′ , cl(O)) ⊆ Σ for all D′ ∈ ND s.t. D ⪯d D′ .
• DΣ(O) is the set of axioms ¬D1 ⊔ . . . ⊔ ¬Dn s.t. (i) clΣ(O) contains axioms of the form C1 ⊔ Q1r.D1, C2 ⊔ ∀r.D2, . . ., Cn ⊔ ∀r.Dn, where r ∈ NR \ Σ, Q1 ∈ {∀, ∃}, and (ii) {D1. . . . ,Dn} is a minimal set of definers s.t. cl(O) |= D1 ⊓ . . . ⊓Dn ⊑⊥.

Intuitively, if a definer D appears in clΣ(O), then it should not depend on definers in OutΣ(O).

Example 3 (Example 2 cont'd). We have:

• clΣ(O) = cl(O) \ {¬D2 ⊔ B1, ¬D4 ⊔ B3} because Rol(D2, cl(O)) = Rol(D4, cl(O)) = {s} ̸⊆ Σ and,
• DΣ(O) = {¬D2 ⊔ ¬D4}.

Theorem 1. RIΣ(O) is role isolated for Σ and we have O ≡Σ∪sig C (O) RIΣ(O).

To compute DΣ(O), we saturate cl(O) using the inference rules shown in Fig. 2, which is sufficient due to the following lemma.

Lemma 1. Let S be the set of axioms ¬D1 ⊔ . . . ⊔ ¬Dn, obtained by applying the rules in Fig. 2 exhaustively on cl(O). Then, for all D1, . . ., Dn ∈ ND, we have cl(O) |= D1⊓. . .⊓Dn ⊑⊥ iff ¬Di1 ⊔. . .⊔¬Dik ∈ S for some subset {i1, . . . , ik} ⊆ {1, . . . , n}.

Example 4 (Example 3 cont'd). The axiom ¬D2 ⊔ ¬D4 in DΣ(O) is obtained by applying two A-Rule inferences:

4.2 Role Forgetting for Role Isolated Ontologies

If O is role isolated for Σ, a role forgetting for O and Σ can be obtained using the r-Rule in Figure 2. Our method applies to any ontology in normal form, not necessarily normalized using cl, which is why now the concept names D1, . . . , Dn in the r-Rule can include also concept names outside ND.

Definition 5. rolEΣ(O) is the ontology obtained as follows:

1. apply the r-Rule exhaustively for each r ∈ sig R (O) \ Σ,
2. remove all axioms containing some r ∈ sig R (O) \ Σ.

The second step ensures that all role names in the resulting ontology rolEΣ(O) are in Σ and therefore, we have sig(rolEΣ(O)) ⊆ Σ ∪ sig C (O).

Example 5 (Example 4 cont'd). For the ontology RIΣ(O), Table 1 (fourth row) shows rolEΣ(RIΣ(O)) which is obtained through the following two steps:

1. The new axiom ¬D1 ⊔ ¬A2 ⊔ A3 is generated by the r-Rule inference:

1. The two axioms ¬D1 ⊔ ∃s.D2, ¬A2 ⊔ A3 ⊔ ∀s.D4 are removed because they contain s ∈ sig(RIΣ(O)) \ Σ.

Theorem 2. If O is role isolated for Σ, then rolEΣ(O) is a role-forgetting for O and Σ.

5 Computing General Modules via rolEΣ

We compute a general module from rolEΣ(O) by forgetting also the concept names and eliminating all definers. The latter is necessary to obtain an ontology entailed by O. Forgetting concept names is done to further simplify the ontology.

5.1 Concept Forgetting

We say that an ontology M is a concept forgetting for O and Σ iff M is a uniform interpolant for O and the signature Σ′ = Σ ∪ sig R (O) ∪ ND. A concept forgetting can be computed through the A-Rule in Figure 2.

Definition 6. conEΣ(O) is the ontology obtained as follows:

1. apply theA-Rule exhaustively for eachA ∈ sig C (O)\Σ,
2. delete every axiom α that contains A or ¬A, where A ∈ NC \ Σ and no axiom contains Qr.A for Q ∈ {∀, ∃} and r ∈ NR.

Example 6 (Example 5 cont'd). Table 1 (the 5th row) shows the axioms in conEΣ(rolEΣ(RIΣ(O))) obtained as follows.

1. ¬D3 ⊔B4, ¬B2 ⊔A4, and ¬D3 ⊔A4 are first generated by applying the A-Rule on B2 and B4.
2. Axioms containing Bi or ¬Bi, i ∈ {1, . . . , 4}, are removed since Bi ̸∈ Σ. ¬D2 ⊔ ¬D4 is also removed because there are no literals of the form Qr.D2 or Qr.D4.

The following is a consequence of [Zhao and Schmidt, 2017, Theorem 1].

Theorem 3. If O is in normal form, then conEΣ(O) is a concept forgetting for O and Σ.

Theorems 1, 2 and 3, give us the following corollary.

Corollary 1. conEΣ(rolEΣ(RIΣ(O))) ≡Σ O.

5.2 Constructing the General Module

Now, in order to obtain our general modules, we have to eliminate the definers from conEΣ(rolEΣ(RIΣ(O))). To improve the results, we delete subsumed axioms (i.e., axioms ⊤ ⊑ C ⊔ D for which we also derived ⊤ ⊑ C) and also simplify the axioms.

Theorem 4. Let gmΣ(O) be the ontology obtained from conEΣ(rolEΣ(RIΣ(O))) by

• deleting subsumed axioms,
• replacing each definer D by CD, and
• exhaustively applying C1 ⊑ ¬C2⊔C3 ⇒C1⊓C2 ⊑ C3 and C1 ⊑ Qr.¬C2 ⊓ C3 ⇒ C1 ⊓ Qr.C2 ⊑ C3, where ∃ = ∀ and ∀ = ∃.

Then, gmΣ(O) is a general module for O and Σ.

Example 7 (Example 6 cont'd). Table 1 (the 8th row) shows the general module gmΣ(O), which has been obtained using CD1 =∃s.B1 and CD3 =B2.

Eliminating definers in this way may reintroduce previously forgotten names, which is why our general modules are in general not uniform interpolants. This has the advantage of avoiding the triple exponential blow-up caused by uniform interpolation (see Section 1). In contrast, the size of our result is at most single exponential in the size of the input.

Proposition 1. For any ontologyO and signature Σ, we have ∥gmΣ(O)∥ ≤ 2O(∥cl(O)∥) . On the other hand, there exists a family of ontologies On and signatures Σn s.t. ∥On∥ is polynomial in n ≥ 1 and ∥gmΣn (On)∥ = n · 2O(∥cl(On)∥) .

We will see in Section 7 that this theoretical bound is usually not reached in practice, and usually general modules are much smaller than the input ontology.

For some module extraction methods, such as for localitybased modules [Grau et al., 2008], iterating the computation can lead to smaller modules. The following result shows that this is never the case for our method.

Proposition 2. Let (Mi)i≥1 be the sequence of ontologies defined by (i) M1 = gmΣ(O) and (ii) Mi+1 = gmΣ(Mi) for i ≥ 1. Then, we haveMi ⊆Mi+1 for i ≥ 1. Moreover, there exists i0 ≥ 0 s.t. Mk =Mi0 for all k ≥ i0.

This property holds thanks to the substitution step of Theorem 4. This step may reintroduce in gmΣ(O) concept and role names outside of Σ. As a result, the repeated application of rolEΣ and conEΣ on gmΣ(O) can produce additional but unnecessary axioms. However, for ontologies in normal form, our method is stable in the sense that repeated applications produce the same ontology.

Proposition 3. Let O be an ontology in normal form and M= gmΣ(O). Then, gmΣ(M) =M.

5.3 Optimizing the Result

The general module gmΣ(O) may contain complex axioms since definers D can stand for complex concepts CD. To make the result more concise, we eliminate some definers before substituting them. In particular, we use the following operations on conEΣ(rolEΣ(RIΣ(O))), inspired by [Sakr and Schmidt, 2022].

conD-Elim:

where ⋃nj=2 {¬D⊔Cj} (n ≥ 1) are all the axioms of the form ¬D ⊔ C. This rule is applicable only if no Cj contains definers.

Figure 3: Rules to eliminate definers

• Op1. Eliminating conjunctions of definers aims to eliminate disjunctions of negative definers (¬D1 ⊔ . . . ⊔ ¬Dn). This is done in two steps: (i) Applying the conD-Elim rule in Figure 3 on conEΣ(rolEΣ(RIΣ(O))), and then (ii) deleting all axioms of the form ¬D1 ⊔ . . . ⊔ ¬Dn.
• Op2. Eliminating single definers aims to get rid of definers D that do not occur in axioms of the form ¬D⊔¬D1⊔C. This is done in two steps: (i) applying the D-Prop rule of Figure 3 exhaustively and then (ii) deleting all axioms containing definers for which D-Prop has been applied.

Theorem 5. Let gm∗Σ(O) be the ontology obtained by:

• successive application of Op1 and Op2 over conEΣ(rolEΣ(RIΣ(O))), followed by
• application of the steps described in Theorem 4.

Then, gm∗Σ(O) is a general module for O and Σ.

Example 8. Assume Σ = {r,A,A1} and

Then, conEΣ(rolEΣ(RIΣ(O))) is:

where CD1 = ∃s.B1, CD2 = ∀s.B2. And thus, by replacing Di by CDi , we obtain gmΣ(O) =

which is actually more intricate than O. We can avoid this by applying the two optimizations described above.

The elimination of definer conjunctions (Op1) produces

(i) The first step of Op1 applies the conD-Elim inference:

• (ii) The second step of Op1 removes the axiom ¬D1 ⊔ ¬D2. Then, the elimination of definers (Op2) produces

by replacing D1, D2 by ⊤ as there is no axioms with negative Di, i = 1, 2 in Equation (2). Note that the first two axioms in Equation (3) are tautologies and thus can be ignored. Finally, we have gm∗Σ(O) = {A ⊓ A1 ⊑ ∀r.⊥}.

6 Deductive Modules and Uniform Interpolants

Deductive modules Depending on the situation, users might prefer the axioms in the original ontology O rather than newly introduced axioms (e.g., axioms in gmΣ(O) or gm∗Σ(O)). For such situations, we can compute a deductive module for O and Σ by tracing back the inferences performed when computing the general module gm∗Σ(O).

Let ResΣ(O) be the set of all axioms generated by the computation progress of gm∗Σ(O). Clearly, gm∗Σ(O) ⊆ ResΣ(O). We iteratively construct a relation R on ResΣ(O) during the computation gm∗Σ(O) as follows: we start with R = ∅, and each time a new axiom β is generated from a premise set {α1, . . . , αn} (e.g., if β is obtained by applying r-Rule on {α1, . . . , αn}), we add to R the relations α1Rβ, . . . , αnRβ. Let R∗ be the smallest transitive closure of R. Then the deductive module is defined as follows.

Theorem 6. Let us define dmΣ(O) by

Then, dmΣ(O) is a deductive module for O and Σ.

Uniform interpolants While general modules can be a good alternative to uniform interpolants for ontology reuse, uniform interpolation has applications that require the ontology to be fully in the selected signature, as stated in the introduction. If instead of substituting definers D by CD, we eliminate them using existing uniform interpolation tools, we can compute a uniform interpolant for the input.

When computing gm∗Σ(O) for an ontology O and signature Σ, if all definers have been eliminated by Op1 and Op2 from Section 5.3 (as in Example 8), then gm∗Σ(O) is indeed a uniform interpolant for O and Σ. Otherwise, we compute a uniform interpolant by forgetting the remaining definers using an existing uniform interpolation tool such as LETHE or FAME [Koopmann, 2020; Zhao and Schmidt, 2018]. As we see in Section 7, this allows us to compute uniform interpolants much faster than using the tool alone.

7 Evaluation

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 ALC. We were also interested in the impact of our optimization, and the performance of our technique for computing deductive modules and uniform interpolants. We implemented a prototype called GEMO in Python 3.7.4. As evaluation metrics, we looked at run time, length of computed ontologies, and length of largest axiom in the result. All the experiments were performed on a machine with an Intel Xeon Silver 4112 2.6GHz, 64 GiB of RAM, Ubuntu 18.04, and OpenJDK 11.

Corpus The ontologies used in our experiment are generated from the OWL Reasoner Evaluation (ORE) 2015 classification track [Parsia et al., 2017] by the two following steps. First, we removed axioms outside of ALC from each ontology in ORE 2015. Then, we kept the ontologies O for which cl(O) contained between 100 and 100,000 names. This resulted in 222 ontologies.

Signatures For each ontology, we generated 50 signatures consisting of 100 concept and role names. As in [Koopmann and Chen, 2020], we selected each concept/role name with a probability proportional to their occurrence frequency in the ontology. In the following, a request is a pair consisting of an ontology and a signature.

Methods For each request (O,Σ), GEMO produced three different (general) modules gmΣ(O), gm∗Σ(O) and dmΣ(O), respectively denoted by gm, gm∗ , and dm. gmLethe denotes the uniform interpolation method described in Section 6, where we used GEMO for computing gm∗ and then LETHE for definer forgetting. In the implementation, for each request, we first extracted a locality based ⊤⊥∗ -module [Grau et al., 2008] to accelerate the computation. This is a common practice also followed by the uniform interpolation and deductive module extraction tools used in our evaluation. Since removing subsumed axioms as mentioned in Theorems 4 and 5 can be challenging, we set a time limit of 10s for this task.

We compared our methods with four different alternatives: (i) ⊤⊥∗ -modules [Grau et al., 2008] as implemented in the OWL API [Horridge and Bechhofer, 2011]; (ii) minM [Koopmann and Chen, 2020] that computes minimal deductive modules under ALCH∇-semantics; (iii) LETHE 0.6 1 [Koopmann, 2020] and FAME 1.0 2 [Zhao and Schmidt, 2018] that compute uniform interpolants.

Success rate We say a method succeeds on a request if it outputs the expected results within 600s. Table 2 summarizes the success rate for the methods considered. After the ⊤⊥∗ - modules, our method GEMO had the highest success rate.

Module length and run time Because some of the methods can change the shape of axioms, the number of axioms is not a good metric for understanding the quality of general modules. We thus chose to use ontology length as defined in Section 2, rather than size, for our evaluation. Table 3 shows the length and run time for the requests on which all methods were successful (78.45% of all requests).

We observe that dm and gmLethe have the best overall performance: their results had a substantially smaller average length and were computed significantly faster than others. Note that the average size of results for dm was even smaller than that for minM. The reason is that minM preserves entailments over ALCH∇, while we preserve only entailments over ALC. Therefore, the minM results may contain additional axioms compared to the ALC deductive modules.

Comparing gm and gm∗ regarding length lets us conclude that the optimization in Section 5.3 is effective. On the other hand, minM produced results of small length but at the cost of long computation times. FAME and ⊤⊥∗ -module were quite time-efficient but less satisfactory in size, especially for FAME, whose results are often considerably larger than for the other methods. LETHE took more time than FAME, but produced more concise uniform interpolants on average.

1 https://lat.inf.tu-dresden.de/∼koopmann/LETHE/

2 http://www.cs.man.ac.uk/∼schmidt/sf-fame/

For 87.87% of the requests reported in Table 3, gm∗ already computed a uniform interpolant, so that gmLethe did not need to perform any additional computations.

Figure 4 provides a detailed comparison of minM, gm∗ and gmLethe. gm∗ was often faster but produced larger results. In contrast, gmLethe produced more concise results at the cost of longer computation time. While minM avoided large modules, it was generally much slower than our methods.

Table 4 summarizes the results concerning all requests for which GEMO (resp. gmLethe) was successful. We see that the results of dm had a small average size. However, as for gm∗ and gmLethe, the median size of results was much smaller, which suggests that gm∗ and gmLethe perform better over relatively simple cases.

Uniform interpolants For 80.23% of requests where GEMO was successful, gm∗Σ(O) was already a uniform interpolants. In the other cases, the success rate for gmLethe was 93.96%. In the cases where LETHE failed, the success rate for gmLethe was 36.23%.

The comparison of LETHE with gmLethe in Figure 5 shows that gmLethe was significantly faster than LETHE in most of the cases.

Axiom size A potential shortcoming of general modules compared to classical modules is that they could contain axioms that are more complex than those of the input, and thus be harder to handle by human end-users. For the requests reported in Table 3, the largest axiom in the output of minM had length 352, while for gm∗ , it had length 5,815, and for gm, even only 56. In contrast, for the uniform interpolants computed by LETHE and FAME, the situation was much worse: here, the largest axiom had a length of 26,840 and 130,700, respectively, which is clearly beyond what can be understood by a human end-user. Besides these extreme cases, we can also observe differences wrt. the median values: for gm∗ the longest axiom had a median length of 3, which is even lower than the corresponding value for minM (5), and, as expected, lower than for LETHE (4) and FAME (6). This indicates that, in most cases, general modules computed by gm∗ are simple than for the other tools.

8 Conclusion

We presented new methods for computing general modules for ALC ontologies, which can also be used for computing deductive modules and uniform interpolants. Due to its higher syntactical flexibility, our general modules are often smaller and less complex than both classical modules and uniform interpolants computed with the state-of-the-art, which makes them particularly useful for applications such as ontology reuse and ontology analysis. Our method is based on a new role isolation process that enables efficient role forgetting and an easy definer elimination. The experiments on realworld ontologies validate the efficiency 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 DLs.

Acknowledgements

Hui Yang, Yue Ma and Nicole Bidoit are funded by the BPIFrance (PSPC AIDA: 2019-PSPC-09) and ANR (EXPIDA: ANR-22-CE23-0017). Patrick Koopmann is partially funded by DFG Grant 389792660 as part of TRR 248-CPEC (see https://perspicuous-computing.science)