On Concept Forgetting in Description Logics with Qualified Number Restrictions

1 Introduction

Forgetting is a non-standard reasoning service that seeks to create restricted views of ontologies by eliminating concept and role names from ontologies in a way such that all logical consequences are preserved up to the remaining signature. It has proved to be a very useful technique in ontology-based knowledge processing, as it allows users to focus on specific parts of (usually very large) ontologies for easy reuse, or to zoom in on (usually very complex) ontologies for in-depth analysis. Other uses of forgetting are information hiding, explanation generation (abduction), ontology debugging and repair, as well as computing the logical difference between ontology versions [Bicarregui et al., 2001; Lang et al., 2003; Konev et al., 2009; Grau and Motik, 2012; Wernhard, 2013; Ludwig and Konev, 2014; Wang et al., 2014].

Forgetting can be defined in two ways that are closely related; it can be defined syntactically as the dual of uniform interpolation [Visser, 1996] (related notions include weak forgetting [Zhang and Zhou, 2010], consequence-based inseparability [Lutz and Wolter, 2010] and consequence-based conservative extensions [Ghilardi et al., 2006]) and it can be defined model-theoretically as semantic forgetting [Wang et al., 2014] (related notions include strong forgetting [Lin and Reiter, 1994], model inseparability [Konev et al., 2013], model conservative extensions [Lutz et al., 2007] and second-order quantifier elimination [Gabbay et al., 2008]). The two notions differ in the sense that uniform interpolation preserves all logical consequences up to certain names whereas semantic forgetting preserves equivalence up to certain names. In this sense, semantic solutions are in general stronger than the uniform interpolants; they often require more expressivity than is available in the source logic. For example, the semantic solution of forgetting the role name {r} from the ALC-ontology {A1 ⊑ ∃r.B, A2 ⊑ ∀r.¬B} is {A1 ⊑ ∃▽.B, A1 ⊓A2 ⊑ ⊥}, whereas the uniform interpolant is {A1 ⊓ A2 ⊑ ⊥}, which is weaker. Observe in this case that the target language must include the universal role ▽ to represent the semantic solution. If a semantic solution is expressible in the source logic, then it is equivalent to the uniform interpolant, which means, in this case, the two notions coincide [Zhang and Zhou, 2010].

Despite the notable usefulness in ontology engineering as described above, forgetting is an inherently difficult problem; it is much harder than standard reasoning (satisfiability testing) and very few logics are known to have the uniform interpolation property or are complete for semantic forgetting. It is known that: (i) uniform interpolants and semantic solutions of forgetting do not always exist for EL and ALC [Konev et al., 2008; Lutz and Wolter, 2011; Konev et al., 2013], (ii) deciding the existence of uniform interpolants is EXPTIME-complete for EL [Lutz et al., 2012] and 2EXPTIMEcomplete for ALC [Lutz and Wolter, 2011], (iii) the existence of semantic solutions of forgetting is undecidable for EL and ALC [Konev et al., 2013; Botoeva et al., 2016], and (iv) uniform interpolants can be triple exponential in size w.r.t. the input ontologies for EL and ALC [Lutz and Wolter, 2011; Nikitina and Rudolph, 2014].

These not very encouraging results have not prevented the community from developing practical methods for computing uniform interpolants and semantic forgetting solutions for various description logics. For example, [Ludwig and Konev, 2014] have developed a resolution-based method for computing uniform interpolants for ALC TBoxes. Since ALC does not have the uniform interpolation property, the method introduces a depth-bounded version of the core algorithm to guarantee finite representations of uniform interpolants. Another resolution-based method for uniform interpolation for ALC TBoxes is by [Koopmann and Schmidt, 2013b]. This method introduces fixpoint operators in the target language to ensure that uniform interpolants can always be finitely represented. The method has been extended to the languages of ALCH, ALCQ and SIF TBoxes [Koopmann and Schmidt, 2013a; 2014; 2015a], and ALC and SHI with ABoxes [Koopmann and Schmidt, 2015b; Koopmann, 2015]. Practical methods for computing semantic solutions of forgetting are developed, implemented and evaluated in [Zhao and Schmidt, 2015; 2016]. These methods are based on generalisations of Ackermann's Lemma [Ackermann, 1935], and attempt to eliminate concept and role names from ontologies expressible in the description logic ALCOIH(▽, ⊓). The methods are incomplete however; for example, they cannot handle the case of forgetting the concept name {B} from {A1 ⊑ ∃r.B,A2 ⊑ ∃r.¬B}, because the forgetting solution {A1 ⊑ ∃r.⊤,A2 ⊑ ∃r.⊤, A1 ⊓ A2 ⊑ ≥2r.⊤} requires more expressivity than is available in the source logic (number restrictions). The methods have been extended to description logics with number restrictions [Zhao and Schmidt, 2017], but the work is focused only on role forgetting.

This paper presents a practical method for computing solutions of concept forgetting in description logics with number restrictions and nominals. While allowing the given example to be solved, admitting number restrictions and nominals significantly increases the difficulty of the problem. Our method handles in particular ontologies expressed in ALCOQ and the extension with role negation, role conjunction and role disjunction, which means that it can handle expressive description logics that cannot be handled by other methods at present. The method follows an Ackermann-based approach, it is terminating, sound and nearly concept forgetting complete for ALCOQ(¬, ⊓, ⊔). When it succeeds, the method outputs either a semantic solution of concept forgetting, or a uniform interpolant in ALCOQ(¬, ⊓, ⊔). Results of an evaluation with a prototypical implementation have shown that the method is computationally feasible and is able to find solutions of concept forgetting in more than 90% of the test cases from a large corpus of biomedical ontologies. In only 13.2% of these cases the solutions were semantic solutions.

2 The Description Logic ALCOQ(¬, ⊓, ⊔)

Let NC, NR and NI be countably infinite and pairwise disjoint sets of concept names, role names and individual names (aka nominals), respectively. Roles in ALCOQ(¬, ⊓, ⊔) can be a role name r ∈ NR, or formed with negation ¬, conjunction ⊓ and disjunction ⊔. Concepts in ALCOQ(¬, ⊓, ⊔) have one of the following forms:

where a ∈ NI, A ∈ NC, C and D are any concepts, R is any role, and m ≥ 1 and n ≥ 0 are natural numbers. Additional concepts are represented as abbreviations: ∃R.C = ≥1R.C, ∀R.C = ≤0R.¬C, ¬≥mR.C = ≤nR.C and ¬≤nR.C = ≥mR.C, where n = m- 1. Concepts of the form ≥mR.C and ≤nR.C are called (qualified) number restrictions, which allow one to specify cardinality constraints on roles.

An ALCOQ(¬, ⊓, ⊔)-ontology comprises of a TBox and an ABox. A TBox is a finite set of axioms of the form C ⊑ D (concept inclusions), where C and D are concepts. An ABox is a finite set of axioms of the form C(a) (concept assertions), where a ∈ NI and C is a concept. As this paper is only concerned with concept forgetting, not including role assertions or role inclusions in the language is without loss of generality, because concept names do not occur in them. Concept assertions are superfluous in description logics with nominals, because they can be expressed equivalently as concept inclusions via nominals: C(a) as a ⊑ C. Hence, in this paper, an ALCOQ(¬, ⊓, ⊔)-ontology is assumed to contain only TBox axioms. The semantics of ALCOQ(¬, ⊓, ⊔) is as expected.

Theorem 1. Reasoning in ALCOQ(¬, ⊓, ⊔) is decidable.

Theorem 1 follows from the decidability of C2 [Gr¨adel et al., 1997], which subsumes the logic ALCOQ(¬, ⊓, ⊔).

Our forgetting method works with TBox axioms in clausal form. A TBox literal in ALCOQ(¬, ⊓, ⊔) is a concept of the form a, ¬a, A, ¬A, ≥mR.C or ≤nR.C. A TBox clause in ALCOQ(¬, ⊓, ⊔) is a disjunction of a finite number of TBox literals. TBox clauses are obtained from TBox axioms using the standard clausal form transformations.

Let A ∈ NC be a designated concept name. An occurrence of A is said to be positive (negative) in an axiom (clause) if it is under an even (odd) number of explicit and implicit negations, e.g., A is positive in ≥mr.A and ≤nr.¬A, and negative in ≥mr.¬A and ≤nr.A. An axiom or clause is called an A-axiom or A-clause if it contains an occurrence of A. An axiom or clause is called an A+-axiom or A+-clause (A-- axiom or A--clause) if it contains a positive (negative) occurrence of A. A set N of clauses is said to be positive (negative) w.r.t. A if every occurrence of A in N is positive (negative).

By sig C(X), sig R(X) and sig I (X), we denote respectively sets of the concept names, role names and individual names occurring in X, where X ranges over concepts, roles, axioms, clauses, sets of axioms and sets of clauses. Let A ∈ NC be any concept name, and let I and I ′ be two interpretations. We say that I and I ′ are equivalent up to A, or A-equivalent, if I and I ′ coincide but differ possibly in the interpretation of A. More generally, I and I ′ are equivalent up to a set F of concept names, or F-equivalent, if I and I ′ coincide but differ possibly in the interpretations of the names in F.

Definition 1 (Semantic Forgetting). Let O be an ontology and let F ⊆ sig C(O) be a forgetting signature. An ontology O′ is a semantic solution of forgetting F from O iff the following conditions hold: (i) sig C(O′ ) ⊆ sig C(O)\F, and (ii) for any interpretation I: I |= O′ iff I ′ |= O, for some interpretation I ′ F-equivalent to I.

Definition 2 (UniformInterpolation). Let O be an ontology and let F ⊆ sig C(O) be a forgetting signature. An ontology O′ is a uniform interpolant of O for the signature sig C(O)\F iff the following conditions hold: (i) sig C(O′ ) ⊆ sig C(O)\F, and (ii) for any axiom α with sig(α) ⊆ sig(O)\F, O′ |= α iff O |= α, i.e., O′ preserves all logical consequences up to the names in sig C(O)\F.

In this paper, we use the notation F to denote the forgetting signature, i.e., the set of concept names to be forgotten. The concept name in F under current consideration for forgetting is referred to as the pivot in our method.

3 Major Obstacles to Semantic Concept Forgetting in Description Logics with Qualified Number Restrictions

Solutions of forgetting the names in F are computed by successively eliminating single names in F. For most cases the elimination can be based on generalisations of Ackermann's Lemma [Ackermann, 1935], which allow one to eliminate a single concept or role name from an ontology in a way such that the original ontology and the resulting one are equivalent up to the interpretations of the eliminated name (i.e., Conditions (i) and (ii) of Definition 1 hold). The proof is an easy adaptation of the Ackermann's original result [Gabbay et al., 2008]. In Ackermann-based approaches, e.g. [Szałas, 2006; Schmidt, 2012; Zhao and Schmidt, 2015; 2016; 2017], the lemma is the basis for the following rules:

where S ∈ NC (S ∈ NR) is the pivot, the αi (1 ≤ i ≤ n) are concepts (roles) that do not contain S, O(S +) and O(S -) denote respectively the ontology O being positive and negative w.r.t. S, and OSα denotes the ontology obtained from O by substituting α for every occurrence of S in O. S is thus eliminated fromO (by substitution). In this case, α is referred to as the definition of S in O.

Observe that the Rules (1) and (2) are applicable to an ontology O to eliminate a name S, only if (i) every S +-axiom in O has the form α ⊑ S, where S ̸∈ sig(α), or (ii) every S --axiom in O has the form S ⊑ α, where S ̸∈ sig(α). On the other hand, since concept names may occur under a role restriction or a sequence of role restrictions (in this paper, a number restriction or a sequence of number restrictions), e.g., α ⊑ ∀r.S and α ⊑ ∃r.∃s.S, there are cases where O is not in a form suitable for application of either of the two rules. In these cases, O needs to be reformulated so that those syntactically unsatisfactory S-axioms in O are equivalently expressed in the form of α ⊑ S or S ⊑ α.

In the approach of [Zhao and Schmidt, 2015] to semantic concept forgetting in the description logic ALCOI, a concept name under a (or a sequence of) universal role restriction can be moved outwards using Galois connections between ∀r and ∀r-, e.g., α ⊑ ∀r.S is equivalently expressed as ∃r-.α ⊑ S, and in the case of concept assertions, Skolemisation allows a concept name under an (or a sequence of) existential role restriction to be moved outwards, e.g., a ⊑ ∃r.S is replaced by a ⊑ ∃r.b and b ⊑ S, where a is a nominal and b is a fresh nominal. However, this approach has three drawbacks: (i) Galois connections require inverse roles in the language and Skolemisation adds new nominals in the forgetting solutions, (ii) Skolemisation can be used only in the cases where the axiom is a concept assertion, but not when the axiom is a concept inclusion, and most importantly, (iii) Galois connections and Skolemisation are not sufficient in axioms with number restrictions. This means that these two methods cannot be used for the logic considered in this paper.

[Zhao and Schmidt, 2017] have developed an Ackermannbased approach to semantic role forgetting in description logics with number restrictions (but have left the problem of concept forgetting open). For concept forgetting in these logics, a seemingly feasible solution is the reduction of concept forgetting to role forgetting. The idea is to first replace in the given ontology every occurrence of the concept name one wants to forget by the concept ≥1r.⊤, where r is a fresh role name, and then forget {r} from the present ontology using the approach of [Zhao and Schmidt, 2017]. However, this approach has proved to be unfeasible in practice, because the solution of role forgetting (i.e., an ontology that does not contain r) computed by the method include newly introduced definer names, 1 which are supposed not to be present in the forgetting solutions (they are supposed to be eliminated from the intermediate solutions as regular concept names). Moreover, it can be observed that the axioms in resulting ontology often have the same syntactic patterns as those given in the original concept forgetting. This brings the problem back to the original concept forgetting. For example, forgetting the concept name {B} from the ontology {A1 ⊑ ≥2s.B, A2 ⊑ ≤1s.B} can be reduced to the problem of forgetting the role name {r} from {A1 ⊑ ≥2s.≥1r.⊤,A2 ⊑ ≤1s.≥1r.⊤}, where r is a fresh role name. The solution of the role forgetting computed by the method is {A1 ⊑ ≥2s.D, A2 ⊑ ≤1s.D}, where D ∈ ND is a fresh concept definer name. Observe that the axioms in the resulting set and those in the given one have the same syntactic patterns, and the problem then becomes forgetting the definer {D} from {A1 ⊑ ≥2s.D, A2 ⊑ ≤1s.D}, which is basically the same problem of forgetting {B} from {A1 ⊑ ≥2s.B, A2 ⊑ ≤1s.B}.

Inspired by the same work we consider solving the problem by working on translations of ontologies in first-order logic, where transforming a formula into a specific form seems to be much easier (because in first-order logic concept and role names are syntactically more 'easy-going'; concept names are not explicitly preceded by role restrictions). Then concept names can be eliminated using methods for semantic forgetting in first-order logic such as the SCAN algorithm (based on resolution) and the DLS algorithm (based on Ackermann's Lemma) [Gabbay and Ohlbach, 1992; Doherty et al., 1997; Gabbay et al., 2008]. The forgetting solution, which is a set of first-order formulas, is then translated into equivalent expressions in a description logic. However, this is unfeasible as well. The reasons can be illustrated with two examples.

Example 1. First, we consider the case of forgetting the role name {r} from the ontology {A1 ⊑ ≥2r.B, A2 ⊑ ≤1r.B}. The translation of this ontology in first-order logic is:

1 Definers names (or definers) are auxiliary concept names that do not occur in the present ontology [Koopmann and Schmidt, 2013b]; they are used to facilitate the normalisation of a given ontology.

where f1(x) and f2(x) are Skolem terms. The forgetting solution computed by both the SCAN or DLS method in existential quantifier-free first-order logic is:

This can be expressed equivalently in a description logic as follows (if the target logic includes the universal role):

Example 2. Next, we consider the case of forgetting the concept name {B} from the same ontology as given in Example 1. The solution computed by SCAN or DLS in existential quantifier-free first-order logic is:

Because of the two variables x and x′ not being unified in the last formula of the forgetting solution, it is not clear if this solution can be expressed equivalently in a description logic. It has been found that solutions of concept forgetting usually contain such ununified variables, which makes the translation to a description logic seem impossible, but this does not happen when forgetting role names. An important reason is that role names are binary relations and are guards, and resolving on these unifies variables in the premises. In contrast, concept names are unary relations, and resolving on these produces a resolvent with more than two variables. These are the cases in our approach (described in the next section) where the preservation of equivalence is open.

4 Our Ackermann-Based Approach to Eliminating One Concept Name

In this section, we present our approach to eliminating a concept name from a set of TBox clauses in ALCOQ(¬, ⊓, ⊔). It is a direct approach based on a non-trivial generalisation of Ackermann's Lemma. The approach has two ingredients: (i) transformation of the given clause set into reduced form, and (ii) an Ackermann rule. The reduced form is a specialised normal form that is suitable for application of the Ackermann rule. The Ackermann rule reflects the generalisation of Ackermann's Lemma and allows a concept name to be eliminated from a set of clauses in reduced form.

4.1 Transformation into Reduced Form

Definition 3 (Reduced Form). Suppose A ∈ NC is the pivot. A clause is in reduced form if it has the form C ⊔A, C ⊔¬A, C ⊔ ≥xR.A, C ⊔ ≥xR.¬A, C ⊔ ≤yR.A or C ⊔ ≤yR.¬A, where C is a clause that does not contain A, R is a role, and x ≥ 1 and y ≥ 0 are natural numbers. A set N of clauses is in reduced form if every A-clause in N is in reduced form.

The reduced forms include all elementary forms of clauses in which a concept name could occur (i.e., a concept name could occur at the top level, or under a ≥-restriction or ≤- restriction of a clause). Clauses not in reduced form have the form C ⊔≥xR.D or C ⊔≤yR.D, where (i) C is a clause that contains A, or (ii) D ̸= (¬)A is a concept that contains A.

Given a set N of TBox clauses (not in reduced form) with A ∈ sig C(N) being the pivot, the first step in our approach is to transform N into reduced form so that the Ackermann rule can be applied to N to eliminate A. This involves the introduction of definers. Let ND ⊂ NC be a set of definers disjoint from sig C(N). Definers are introduced, incrementally replacing 'C' and 'D' in every A-clause not in reduced form until (i) and (ii) above do not hold. A new clause ¬D1 ⊔ C is added to N for each replaced subconcept C, a new clause ¬D2 ⊔ D is added to N for each replaced subconcept D immediately under a ≥-restriction, and a new clause D3 ⊔ D is added to N for each replaced subconcept D immediately under a ≤-restriction, where D1,D2,D3 ∈ ND are fresh definers. In this way, N is transformed into reduced form.

Theorem 2. Using the definer introduction, any set of clauses in ALCOQ(¬, ⊓, ⊔) can be transformed into reduced form. The transformation is polynomial and preserves equivalence up to the interpretations of the introduced definers.

Proof (sketch). The definer introduction is basically the standard structural transformation (polynomial). It uses Ackermann's Lemma in the reverse direction to introduce definers.

4.2 Ackermann Rule

Let N be a set of TBox clauses in reduced form for the pivot A ∈ sigC(N). By P + ⋆(A) and P - ⋆ (A) we denote the sets of the clauses of the form C ⊔ A and C ⊔ ¬A, respectively. By P + ≥ (A) and P - ≥ (A) we denote the sets of the clauses of the formC⊔≥xR.A and C⊔≥xR.¬A, respectively. By P + ≤ (A) and P - ≤ (A) we denote the sets of the clauses of the form C ⊔ ≤yR.¬A and C ⊔ ≤yR.A, respectively. We use P +(A) to denote the union of the sets P + ⋆(A), P + ≥ (A) and P + ≤ (A) (the positive premises). We use P -(A) to denote the union of the sets P - ⋆ (A), P - ≥ (A) and P - ≤ (A) (the negative premises). We use N -A to denote the set of the non-A-clauses in N.

The second step in our approach is to apply the Ackermann rule, shown in Figure 1, to N to eliminate A. The Ackermann rule is a replacement rule which replaces the clauses above the line (the premises) by those under the line (the conclusion). The idea is to combine the set of the positive premises P +(A) with every negative premise α ∈ P -(A) (or to combine the set of the negative premises P -(A) with every positive premise α ∈ P +(A)). The result of each combination is a finite set of clauses that does not contain A, denoted by BLOCK(P +(A), α) (or BLOCK(P -(A), α)). The conclusion of the rule, which is the solution of forgetting A from N , is the union of the blocks obtained from these combinations. It is found that in some combination cases the result obtained from combining P +(-) (A) with α is identical to the union of the results obtained from combining respectively P +(-) ⋆ (A), P +(-) ≥ (A) and P +(-) ≤ (A) with α. Thus, for clarity's sake, we split such combinations into separate cases in the presentation of the Ackermann rule. For different premises, the combination is performed as nine different cases (see Fig. 1). Soundness of the rule follows from the following two lemmas.

Figure 1: The Ackermann rule for eliminating A ∈ sigC (N) from a set N of TBox clauses in reduced form

Lemma 1. Cases 1, 2, 3, 4 and 5 in Figure 1 preserve equivalence up to the interpretation of the pivot.

Proof. For Cases 1, 2, 3, 4 and 5, the idea of the combination is analogous to that of Ackermann's Lemma, where the pivot is eliminated by computing the definition of the pivot from the negative (positive) premises and substituting this definition for the pivot in every positive (negative) premise.

The preservation of equivalence in Cases 6, 7, 8 and 9 is open (because of the cases discussed in Section 3). We show that the results in these cases are at least uniform interpolants.

Lemma 2. Cases 6, 7, 8 and 9 in Figure 1 preserve all logical consequences up to the names in sig C(N)\F.

Proof (sketch). For space reasons, we only prove Case 8. The other cases can be proved similarly. {Dj ⊔ ≥wjQj.⊤} follows directly from the premises. Assume a domain element has minimally x R-successors satisfying A and maximally y S-successors satisfying A, then, if x > y, it has minimally x - y R- and ¬S-successors satisfying A or ¬A (⊤). Thus, {Dj ⊔ Hk′ ⊔ ≥(wj - zk′ )(Qj ⊓ ¬Tk′ ).⊤} holds.

Two special cases are that: A occurs (i) only positively, or (ii) only negatively, in N. Then A is said to be pure in N (impure, otherwise). In Case (i), the solution of forgetting A from N is computed by substituting ⊤ for every occurrence of A in N, and in Case (ii), the solution is computed by substituting ⊥ for every occurrence of A in N. This is referred to as the purification, which preserves equivalence up to the interpretations of the pivot [Zhao and Schmidt, 2016].

5 The ForgettingMethod

The input to the method are a set cls set of TBox clauses and a set f sig of concept names to be forgotten. Our method performs purification first (on the entire clause set), because purification often results in numerous redundancies, tautologies and contradictions inside the clauses, which are immediately simplified or eliminated thereby leading to a much reduced clause set. This makes subsequent forgetting less difficult. A notable feature of the method is that impure names are eliminated in a local manner, that is, a concept name A ∈ f sig is eliminated from only the A-clauses, rather than the entire clause set. This significantly reduces the search space. In this way, the method eliminates the concept names in f sig one by one. Once all these concept names have been eliminated, the method attempts to eliminate the introduced definers to compute the forgetting solution. Yet the definer elimination is not always successful; it may fail when the original concept forgetting involves cyclic dependencies. For example, forgetting the concept name {A} from {¬A⊔∃r.A} yields {¬D⊔∃r.D}, where D ∈ ND is a fresh definer. Observe that the clause in the resulting set has the same pattern with the one in the given set. Thus, eliminating the definer {D} from {¬D ⊔ ∃r.D} would, as one can expect, yield another 'same pattern' clause. This problem can be solved using fixpoints [Koopmann and Schmidt, 2013b], with which in the target language we may even make our method complete. However, since at present mainstream tools do not support fixpoints, we do not include them for practicality of the method. What the method returns as output are a finite set cls set of TBox clauses. If cls set does not contain any names in f sig or any introduced definers, then the method was successful. The following theorem states termination and soundness of the method.

Theorem 3. For any ALCOQ(¬, ⊓, ⊔)-ontology O and any forgetting signature F ⊆ sigC(O), our method always terminates and returns a finite set O′ of TBox clauses. If O′ does not contain any names in F or any introduced definers, then O′ is either a semantic solution of forgetting F from O, or a uniform interpolant of O for the signature sig C(N)\F.

Theorem 4. Given an ALCOQ(¬, ⊓, ⊔)-ontology O and a forgetting signature F ⊆ sigC(O), our method is guaranteed to compute a semantic solution of forgetting F from O if the following conditions hold for each A ∈ F: (i) O is an acyclic TBox w.r.t. the names in F (including internalised ABox axioms), and (ii) A does not occur positively (negatively) under a ≥-restriction and a ≤-restriction.

Proof (sketch). Condition (i) ensures all definers can be eliminated from O. Condition (ii) means in the reduced form of O for any A ∈ F, P + ≥ (A) = ∅ and P + ≤ (A) = ∅, or P - ≥ (A) = ∅ and P - ≤ (A) = ∅. This avoids Cases 6, 7, 8 and 9.

6 Evaluation and Empirical Results

In order to gain insight into the practicality of our forgetting method, we implemented a prototype in Java using the OWL API 2 and evaluated it on a corpus of biomedical ontologies. The corpus was based on a snapshot of the BioPortal repository taken in March 2017 [Matentzoglu and Parsia, 2017], containing 396 OWL API compatible ontologies.

Because the ontologies in the snapshot can be as expressive as SHOIN(D) and SROIQ(D), we adjusted the selected ontologies to the language of ALCOQ(¬, ⊓, ⊔) using simple simulations and replacements, e.g., an exact number restriction =1r.C was simulated by≥1r.C ⊓ ≤1r.C and concepts not expressible in ALCOQ(¬, ⊓, ⊔) were replaced by ⊤. Table 1 shows statistical information about the adjusted ontologies, where #(O) denotes the numbers of axioms in the ontologies, and #sig C(O), #sig R(O) and #sig I (O) denote respectively the numbers of the concept names, role names and

2 https://github.com/owlcs/owlapi

T.O.: Timeout, S. Rate: Success Rate, S. Sol.: Semantic Solution

Table 2: Results of forgetting 10%, 30% and 50% of concept names

individual names in the ontologies. It was found that 38.9% of the test ontologies included ABoxes (154 out of 396).

To fit in with different real-world application scenarios, we evaluated the performance of the prototype for forgetting different numbers of concept names from each test ontology. In particular, we considered respectively the cases of forgetting 10%, 30% and 50% of concept names in the signature of each ontology. The names to be forgotten were randomly selected. The experiments were conducted on a desktop computer with an Intel® Core TM i7-4790 processor, four cores running at up to 3.60 GHz, and 8 GB of DDR3-1600 MHz RAM. The experiments were run 100 times on each ontology and we averaged the results in order to verify the accuracy of our findings. A timeout of 1000 seconds was imposed on each run.

The results are shown in Table 2. The most encouraging results are that on average: (i) the prototype was successful (i.e., eliminated all specified concept names and the introduced definers) in more than 90% of the test cases, and (ii) in most of these cases forgetting solutions were computed within 10 seconds. The column headed T.O. shows the percentages of the test cases where the solutions could not be computed within the timeout. The column headed ND shows the percentages of the test cases where the definers could not be all eliminated from the results. The column headed S. Sol. shows the percentages of the test cases where the solution was a semantic solution; in 13.2% of the successful cases, the solution was a semantic solution and it was a uniform interpolant in the other cases. An important finding, which is not shown in the table, is that role constructs (¬, ⊓ and ⊔) occurred in the forgetting solutions in 32% of the test cases.

7 Conclusions

In this paper, we developed an Ackermann-based method for computing solutions of concept forgetting in the description logic ALCOQ(¬, ⊓, ⊔). When it succeeds, the method outputs either a semantic solution of concept forgetting or a uniform interpolant in ALCOQ(¬, ⊓, ⊔). An evaluation with a prototype has shown that the method is practical and semantic solutions of concept forgetting are rare for ALCOQ(¬, ⊓, ⊔).