Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach

1 Introduction

The origins of interest in forgetting can be traced back to the work of Boole on propositional variable elimination and the seminal work of Ackermann [Ackermann, 1935] who recognized that the problem amounts to the elimination of existential second-order quantifiers. In logic the problem has been studied as the (dual) uniform interpolation problem [Visser, 1996; D'Agostino and Hollenberg, 2000; Herzig and Mengin, 2008], a notion related to the Craig interpolation problem, but stronger. In computer science the importance of forgetting can be found in the knowledge representation literature [Lin and Reiter, 1994; Lang et al., 2003; Delgrande and Wang, 2015], specification refinement literature [Bicarregui et al., 2001] and the area of description logic-based ontology engineering [Botoeva et al., 2016; Wang et al., 2008; 2010; 2014; Konev et al., 2009a; 2009b; 2013; Lutz and Wolter, 2011; Lutz et al., 2012; Grau and Motik, 2012; Ludwig and Konev,

2014; Nikitina and Rudolph, 2014]. In ontology-based information processing, forgetting allows users to focus on specific parts of ontologies in order to create decompositions and restricted views for in depth analysis or sharing with other users. Forgetting is also useful for information hiding, explanation generation, and ontology debugging and repair.

Because forgetting is an inherently difficult problem- it is much harder than standard reasoning (satisfiability testing) - and very few logics are known to be complete for forgetting (or have the uniform interpolation property), 1 there has been insufficient research on the topic (in particular on the topic of role forgetting), and few forgetting tools are available. Recent work has developed practical methods for computing uniform interpolants for ontologies defined in expressive OWL language dialects [Koopmann and Schmidt, 2013a; 2013b; 2015b]. These methods, which are saturation approaches based on resolution, can eliminate both concept and role symbols and can handle ontologies specified in description logics from ALC to ALCH and SIF. The methods have been extended to SHQ for concept forgetting in [Koopmann and Schmidt, 2014]. While most of this work is focused on TBox and RBox uniform interpolation, practical methods for uniform interpolation for description logics ALC and SHI with ABoxes are described in [Koopmann and Schmidt, 2015a; Koopmann, 2015].

An alternative approach that can perform both concept and role forgetting is described, automated and evaluated in [Zhao and Schmidt, 2016]. This approach is a semantic approach which accommodates ontologies expressible in description logics with nominals, role inverse, role inclusions, role conjunction and the universal role. The foundation for this approach is an adaptation of Ackermann's Lemma [Ackermann, 1935], which also provides the foundation for approaches to second-order quantifier elimination [Doherty et al., 1997; Nonnengart and Szałas, 1999; Gabbay et al., 2008] and modal correspondence theory [Szałas, 1993; Conradie et al., 2006; Schmidt, 2012].

In this paper, we follow an Ackermann approach to forgetting and present a practical method for semantic role forgetting in expressive description logics not considered so far. In particular, the method accommodates ontologies expressible in the description logic ALCOQH and the extension with the universal role ▽. The extended expressivity enriches the target language, making it expressive enough to represent the forgetting solution which otherwise would have been lost. For example, the solution of forgetting the role symbol {r} from the ontology {A1 ⊑ ≥2r.B1,A2 ⊑ ≤1r.B2} is the set {A1 ⊑ ≥2▽.B1, A1 ⊓ A2 ⊑ ≥1▽.(B1 ⊓ ¬B2)}, whereas in a description logic without the universal role, the uniform interpolant is {⊤}, which is weaker. Being based on non-trivial generalizations of Ackermann's Lemma, the method is the only approach so far for forgetting role symbols in description logics with qualified number restrictions. The method is goal-oriented and incremental. It always terminates and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols, possibly with new concept definer symbols. Our method is nearly role forgetting complete for ALCOQH(▽)-ontologies, and we characterize cases where the method is complete. Only problematic are cases where forgetting a role symbol would require the combinations of certain cardinality constraints and role inclusions. Despite the inherent difficulty of forgetting for this level of expressivity, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies.

1 [Konev et al., 2013] have shown that the solution of forgetting does not always exist for ALC and EL, and the existence of a solution for forgetting a concept (role) symbol is undecidable for ALC.

2 ALCOQH(▽) and Other Basic Notions

Let NC, NR and NO be countably infinite and pairwise disjoint sets of concept symbols, role symbols and individual symbols (aka nominals), respectively. Roles in ALCOQH(▽) can be any role symbol r ∈ NR or the universal role ▽. Concepts in ALCOQH(▽) have one of the following forms:

where a ∈ NO, A ∈ NC, C and D are any concepts, R is any role, and m ≥ 1 and n ≥ 0 are natural numbers. Additional concepts and roles are defined as abbreviations: ⊥ = ¬⊤, △= ¬▽, ∃R.C = ≥1R.C, ∀R.C = ≤0R.¬C, ¬≥mR.C = ≤nR.C and ¬≤nR.C = ≥mR.C with n = m-1. Concepts of the form ≥mR.C and ≤nR.C are referred to as qualified number restrictions (or number restrictions for short), which allow one to specify cardinality constraints on roles. We assume w.l.o.g. that concepts and roles are equivalent relative to associativity and commutativity of ⊓ and ⊔, ⊤ and ▽ are units w.r.t. ⊓, and ¬ is an involution.

An ALCOQH(▽)-ontology is mostly assumed to be composed of a TBox, an RBox and an ABox. A TBox T is a finite set of concept axioms of the form C ⊑ D (concept inclusion), where C and D are concepts. An RBox R is a finite set of role axioms of the form r ⊑ s (role inclusion), where r, s ∈ NR. We define C ≡ D and r ≡ s as abbreviations for the pair of C ⊑ D and D ⊑ C and the pair of r ⊑ s and s ⊑ r, respectively. An ABox A is a finite set of concept assertions of the form C(a) and role assertions of the form R(a, b), where a, b ∈ NO, C is a concept, and R is a role. In a description logic with nominals, ABox assertions can be equivalently expressed as TBox axioms, namely, C(a) as a ⊑ C and R(a, b) as a ⊑ ∃R.b. Hence, in this paper, we assume w.l.o.g. that an ontology contains only TBox and RBox axioms.

The semantics of ALCOQH(▽) is defined in terms of an interpretation I = 〈∆I , ·I 〉, where ∆I is a non-empty set (the domain of the interpretation), and ·I is the interpretation function, which assigns to every nominal a ∈ NO a singleton aI ⊆ ∆I , to every concept symbol A ∈ NC a set AI ⊆ ∆I , and to every role symbol r ∈ NR a relation rI ⊆ ∆I ×∆I . The interpretation function ·I is inductively extended to concepts and roles as follows:

where #{·} denotes the cardinality of the set {·}.

Our method works with TBox and RBox axioms in clausal normal form. We assume w.l.o.g. that a TBox literal is a concept of the form a, ¬a, A, ¬A, ≥mR.C or ≤nR.C, where a ∈ NO, A ∈ NC, m ≥ 1 and n ≥ 0 are natural numbers, C is any concept, and R is any role. A TBox clause is a disjunction of a finite number of TBox literals. An RBox clause is a disjunction of a role symbol and a negated role symbol. TBox and RBox clauses are obtained by clausification of TBox and RBox axioms, where in the latter case role negation is introduced. This is done for consistency in presentation, replacing role inclusion by disjunction as the main operator. Nominals are treated as regular concept symbols in our method, because we are only concerned with role forgetting in this paper.

A concept axiom C ⊑ D is true in an interpretation I, and we write I |= C ⊑D, iff C I ⊆ DI . A role axiom r ⊑ s is true in an interpretation I, and we write I |= r ⊑ s, iff rI ⊆ sI . I is a model of an ontology O iff every axiom in O is true in I. In this case we write I |= O.

An axiom (clause) that contains a designated (concept or role) symbol S is called an S-axiom (S-clause). An occurrence of S is assumed to be positive (negative) in an S-axiom (S-clause) if it is under an even (odd) number of explicit and implicit negations. For instance, r is assumed to be positive in ≥mr.A and s ⊑ r, and negative in ≤nr.A and r ⊑ s. A set N of axioms (clauses) is assumed to be positive (negative) w.r.t. S if every occurrence of S in N is positive (negative).

3 Definition of Forgetting, Ackermann's Lemma and Obstacles to Role Forgetting

Forgetting can be defined in two ways that are closely related: one is analogous to model inseparability (i.e., a semantic notion based on model-conservative extensions; see e.g. [Konev et al., 2013]), which preserves equivalence up to certain signatures, and the other is via uniform interpolation (i.e., a syntactic notion based on deductive-conservative extensions; see e.g. [Visser, 1996]), which preserves logical consequences; see [Botoeva et al., 2016] a survey for their interrelation.

Our notion of forgetting is a semantic notion. By sigC(X) and sigR(X) we denote the sets of respectively the concept and role symbols occurring in X (excluding nominals), where X ranges over axioms, clauses, sets of axioms, and sets of clauses. Let r ∈ NR be any role symbol, and let I and I ′ be any interpretations. We say I and I ′ are equivalent up to r, or r-equivalent, if I and I ′ coincide but differ possibly in the interpretations of r. More generally, I and I ′ are equivalent up to a set Σ of role symbols, or Σ-equivalent, if I and I ′ coincide but differ possibly in the interpretations of the symbols in Σ. This can be understood as follows: (i) I and I ′ have the same domain, i.e., ∆I = ∆I ′ , and interpret every concept symbol and every individual symbol identically, i.e., AI = AI ′ for every A ∈ NC and aI = aI ′ for every a ∈ NO; (ii) for every role symbol r ∈ NR not in Σ, rI = rI ′ .

It follows from this that: (i) the original ontology O and the forgetting solution O′ are equivalent up to (the interpretations of) the symbols in Σ. Also (ii) forgetting solutions are unique up to equivalence, that is, if both O′ and O′′ are solutions of forgetting Σ from O, then they are logically equivalent.

Definition 1 (Role Forgetting for ALCOQH(▽)) Let O be an ALCOQH(▽)-ontology and let Σ be a subset of sigR(O). An ontology O′ is a solution of forgetting Σ from O, iff the following conditions hold: (i) sigR(O′ ) ⊆ sigR(O)\Σ, and (ii) for any interpretation I: I |= O′ iff I ′ |= O, for some interpretation I ′ Σ-equivalent to I.

In this paper, Σ is always assumed to be a set of symbols to be forgotten. The symbol in Σ under current consideration for forgetting is referred to as the pivot in our method. An axiom (clause) that contains an occurrence of the pivot is referred to as a pivot-axiom (pivot-clause).

Given an ontology O and a set Σ of concept and role symbols, computing a solution of forgetting Σ from O can be reduced to the problem of eliminating single symbols in Σ. This can be based on the use of a monotonicity property found in [Ackermann, 1935], referred to as Ackermann's Lemma. For ontologies, Ackermann's Lemma can be formulated as the following theorem. The proof is an easy adaptation of Ackermann's original result [Gabbay et al., 2008].

Theorem 1 (Ackermann's Lemma) Let O be an ontology that contains axioms α1 ⊑ S, ..., αn ⊑ S, where S ∈ NC (or S ∈ NR), and the αi (1 ≤ i ≤ n) are concepts (or roles) that do not contain S. If O\{α1 ⊑ S, ..., αn ⊑ S} is negative w.r.t. S, then OSα1⊔...⊔αn is a solution of forgetting {S} from O (i.e., Conditions (i) and (ii) of Definition 1 hold), where OSα1⊔...⊔αn denotes the ontology obtained from O by substituting α1 ⊔ ... ⊔ αn for every occurrence of S in O.

In Ackermann-based approaches, e.g., [Szałas, 2006; Conradie et al., 2006; Schmidt, 2012; Zhao and Schmidt, 2015; 2016], the lemma is often used as the following rule:

The idea of Ackermann's Lemma is based on a notion of 'substitution', which can informally yet intuitively be understood as follows: given an ontology O with S ∈ sigC(O) (or S ∈ sigR(O)) being the pivot, if there exists a concept (or a role) α such that S ̸∈ sig(α) and α defines S w.r.t. O, then we can substitute this definition for every occurrence of S in O (S is thus eliminated from O). This lemma also holds, when the inclusions are reversed, i.e., S ⊑ α1, ..., S ⊑ αn, and the polarity of S in the rest part of O is switched, i.e., O\{S ⊑ α1, ..., S ⊑ αn} is positive w.r.t. S .

A crucial task in Ackermann-based approaches, therefore, is to find a definition of the pivot w.r.t. the present ontology, that is, to reformulate all pivot-axioms with positive occurrences of the pivot being in the form α ⊑ S (or dually, with negative occurrences of the pivot being in the form S ⊑ α), where S ̸∈ sig(α). In the context of this paper where axioms are represented in clausal form, this means reformulating all pivot-clauses with positive occurrences of the pivot being in the form ¬α ⊔ S (or dually, with negative occurrences of the pivot being in the form ¬S ⊔ α), where S ̸∈ sig(α).

In the case of concept forgetting, a concept symbol (or a negated concept symbol) deep inside a clause could be moved outward by using Galois connections between ∀r and ∀r(e.g., a TBox clause ¬A ⊔ ∀r.S can be equivalently rewritten as (∀r-.¬A) ⊔ S, where r- denotes the inverse of r), or by exploiting the idea of Skolemization (e.g., an ABox clause ¬a ⊔ ∃r.¬S can be equivalently rewritten as ¬a ⊔ ∃r.b and ¬b ⊔¬S, where b is a fresh nominal). This is explained in detail in the work of [Conradie et al., 2006; Schmidt, 2012; Zhao and Schmidt, 2015; 2016].

In the case of role forgetting, since every role symbol that occurs in a TBox clause is always preceded by a role restriction operator (i.e., a number restriction in this work), it is not obvious how to reformulate the TBox pivot-clauses. Thus a direct approach based on Ackermann's Lemma does not seem feasible for role forgetting in ontologies with TBoxes.

How then to do role forgetting? For the translation of ontologies in first-order logic, there are no such obstacles. We could apply Ackermann's Lemma for first-order logic (e.g., as in the DLS algorithm of [Doherty et al., 1997]) to eliminate a single role symbol. Such an indirect approach requires suitable back-translation however, which is absent at present for expressive description logics. Translating first-order formulas into equivalent description logic expressions is not straightforward, in particular when number restrictions are present in the target language. For example, the solution of forgetting the role symbol {r} from {A1 ⊔≥2r.B1, A2 ⊔≤1r.B2} in quantifier-free first-order logic is the set:

where f1(x) and f2(x) are Skolem terms, and f1(x) ̸≈ f2(x) is an inequality. Because of the presence of the Skolem terms and the inequality, it is not clear whether this solution can be expressed equivalently in a description logic.

4 Our Ackermann-Based Approach to Eliminating A Single Role Symbol

In this section we present our approach to eliminating a single role symbol from a set of TBox and RBox clauses expressible in ALCOQH(▽). It is a direct approach based on non-trivial generalizations of Ackermann's Lemma. The approach has two key ingredients: (i) transformation of the present clause set into reduced form, and (ii) a set of Ackermann rules. The Ackermann rules reflect the generalizations of Ackermann's Lemma and allow a single role symbol to be eliminated from a set of clauses in reduced form.

Ackermann I

Ackermann II

Ackermann III

N , BLOCK(P + T (r), E1 ⊔ ≤y1r.F1), ..., BLOCK(P + T (r), En ⊔ ≤ynr.Fn), BLOCK(P + T (r), t1 ⊔ ¬r), ..., BLOCK(P + T (r), tw ⊔ ¬r)

Ackermann IV

N , BLOCK(P +R(r), E1 ⊔ ≤y1r.F1), ..., BLOCK(P +R(r), En ⊔ ≤ynr.Fn), BLOCK(P +R(r), t1 ⊔ ¬r), ..., BLOCK(P +R(r), tw ⊔ ¬r)

Ackermann V

Notation in Ackermann rules (1 ≤ i ≤ m, 1 ≤ j ≤ n, 1 ≤ k ≤ v, 1 ≤ l ≤ w):

1. BLOCK(P - T (r), ∅) denotes the set {E1 ⊔ ≤y1¬▽.F1, . . . , En ⊔ ≤yn¬▽.Fn}. 4. BLOCK(P - R (r), ∅) denotes ∅.
2. BLOCK(P + T (r), ∅) denotes the set {C1 ⊔ ≥x1▽.D1, . . . , Cm ⊔ ≥xm▽.Dm}. 2. BLOCK(P +R(r), ∅) denotes ∅.
3. BLOCK(P + T (r), Ej ⊔ ≤yjr.Fj) denotes the union of following sets, where m = |P + T (r)|:

Ground BLOCK: {C1 ⊔ ≥x1▽.D1, . . . , Cm ⊔ ≥xm▽.Dm}

. . .

mth-tier BLOCK: {Ej ⊔ C1 ⊔ . . . ⊔ Cm ⊔ ≥x▽.(D1 ⊓ . . . ⊓ Dm) ⊔ ≥(x1 + . . . + xm - yj - (x - 1))▽.((D1 ⊔ . . . ⊔ Dm) ⊓ ¬Fj ) ⊔ . . . ⊔ ≥1▽.((D1 ⊔ . . . ⊔ Dm) ⊓ ¬Fj) | x ∈ {1, . . . , xmin}} if x1 + . . . + xm ≥ yj , where xmin denotes the minimum of x1, . . . , xm and x1 + ... + xm - yj .

1. BLOCK(P + T (r), tl ⊔ ¬r) denotes the set: {C1 ⊔ ≥x1tl.D1, . . . , Cm ⊔ ≥xmtl.Dm}.

8. BLOCK(P +R(r), tl ⊔ ¬r) denotes the set: {¬s1 ⊔ tl, . . . , ¬sv ⊔ tl}.

9. BLOCK(P -,0 T (r),Ci ⊔≥xir.Di) denotes the union of following sets, where n = |P -,0 T (r)|:

Ground BLOCK: {Ci ⊔≥xi▽.Di}

nth-tier BLOCK: {Ci ⊔ E1 ⊔ . . . ⊔ En ⊔ ≥xi▽.(Di ⊓ ¬F1 ⊓ . . . ⊓ ¬Fn)}

10. BLOCK(P -,0 T (r), ¬sk ⊔ r) denotes the set: {E1 ⊔≤0sk.F1, . . . ,En ⊔≤0sk.Fn}.

1. BLOCK(P - R (r), ¬sk ⊔ r) denotes the set: {t1 ⊔ ¬sk, . . . , tw ⊔ ¬sk}.
2. BLOCK(P - R (r),Ci ⊔≥xir.Di) denotes the set: {Ci ⊔≥xit1.Di, . . . ,Ci ⊔≥xitw.Di}.

Figure 1: Ackermann rules for eliminating r ∈ NR from a set of clauses in reduced form. In the rules we assume that r ̸∈ sigR (N).

4.1 Transformation into Reduced Form

Definition 2 (Reduced Form) For r ∈ NR the pivot, a TBox pivot-clause is in reduced form if it has the form E ⊔≥mr.F or E ⊔ ≤nr.F , where E and F are concepts that do not contain r, and m ≥ 1 and n ≥ 0 are natural numbers. An RBox pivot-clause is in reduced form if it has the form ¬S ⊔ r or S ⊔¬r, where S ∈ NR and S ̸= r. A set N of clauses is in reduced form if all pivot-clauses in N are in reduced form.

The reduced forms incorporate all basic forms of TBox and RBox clauses in which a role symbol could occur. While an RBox pivot-clause is always in reduced form, this is not true for a TBox pivot-clause. A TBox pivot-clause not in reduced form has the form E ⊔ ≥mS.F or E ⊔ ≤nS.F , where S can be any role (including the pivot role symbol), and E and F are concepts with at least one of them containing the pivot; (≤1r.A) ⊔ (≤3s.≥2r.B) is such an example. Transforming a TBox pivot-clause into reduced form is not always possible unless definer symbols are introduced. Definer symbols are auxiliary concept symbols that do not occur in the present ontology [Koopmann and Schmidt, 2013b], and are introduced as follows: let N be a set of clauses not in reduced form, and let ND ⊂ NC be a set of definer symbols disjoint from sigC(N). Definer symbols are used as substitutes, incrementally replacing 'E' and 'F' for every TBox pivot-clause not in reduced form until neither 'E' nor 'F ' contain the pivot. A new clause ¬D1 ⊔E is added to N for each replaced subconcept E, a new clause ¬D2⊔F is added to N for each replaced subconcept F immediately under a ≥-restriction, and a new clause D3 ⊔ F is added to N for each replaced subconcept F immediately under a ≤-restriction, where D1,D2,D3 ∈ ND are fresh definer symbols. N is thus transformed into a set of clauses in reduced form. For the example mentioned above, this means that D1 and D2 are introduced to replace ≤1r.A and ≥2r.B, respectively, which yields D1 ⊔≤3s.D2 and two additional clauses ¬D1⊔≤1r.A and D2⊔≥2r.B. The original clause is thus represented by these three clauses in reduced form (to which an Ackermann rule can be applied).

Theorem 2 Using definer introduction as described above, any ALCOQH(▽)-ontology can be transformed into a set of clauses in reduced form. The transformation preserves equivalence up to the introduced definer symbols.

4.2 Ackermann Rules

Let N be a set of TBox and RBox clauses exhibiting all different reduced forms, for r ∈ sigR(N) the pivot. We refer to the clauses of the form C ⊔≥mr.D and the form C ⊔≤nr.D as positive TBox premises and negative TBox premises of the Ackermann rules, respectively. We refer to the clauses of the form ¬S ⊔ r and the form S ⊔ ¬r as positive RBox premises and negative RBox premises of the Ackermann rules, respectively. By P + T (r) and P - T (r) we denote respectively the sets of positive TBox premises and negative TBox premises. By P +R(r) and P - R (r) we denote respectively the sets of positive RBox premises and negative RBox premises. By P +(r) and P -(r) we denote respectively the union of P + T (r) and P +R(r), and the union of P - T (r) and P - R (r).

The Ackermann rules, shown in Figure 1, are based on an idea of 'combination'. Specifically, the idea is to combine all positive premises P +(r) with every negative premise α(r) in P -(r) (or dually, to combine all negative premises P -(r) with every positive premise α(r) in P +(r)). The result is a finite set of clauses, denoted by BLOCK(P +(-) (r), α(r)). It is observed that the result obtained from combining P +(r) with a negative premise is always identical to the union of the results obtained from combining respectively P + T (r) and P +R(r) with that premise (and the dual also holds). We therefore treat every combination of P +(r) with a negative premise as two separate combinations in our Ackermann rules (same for the dual), so that it can be understood better from which premises a resulting BLOCK of clauses is obtained.

For different P + T (r), P +R(r), P - T (r), P - R (r), and α(r), the combination is performed as 12 distinct cases (see Figure 1). For most cases, the idea is analogous to that of Ackermann's Lemma (and its dual), where the pivot is eliminated by substituting its definition found w.r.t. the present premises for every occurrence of the pivot in these premises. Only for Cases 5 and 9, the combination has a different flavor; their idea is illustrated with two concrete examples.

Case 5: Combining P + T (r) with a negative TBox premise in P - T (r), e.g., Ej ⊔≤yjr.Fj (1 ≤ j ≤ n), yields a set of TBox clauses, denoted by BLOCK(P + T (r),Ej ⊔≤yjr.Fj).

Example 1 Combining P + T (r) = {A1 ⊔≥2r.B1, A2 ⊔≥1r.B2} with {A ⊔ ≤1r.B} yields a set BLOCK(P + T (r),A ⊔ ≤1r.B) that contains the following subsets of clauses:

Ground BLOCK: {A1 ⊔≥2▽.B1,A2 ⊔≥1▽.B2}

1st-tier BLOCK: {A⊔A1 ⊔≥1▽.(B1 ⊓¬B)}

2nd-tier BLOCK: {A⊔A1 ⊔A2 ⊔≥1▽.(B1 ⊓B2) ⊔≥2▽.((B1 ⊔

B2) ⊓ ¬B) ⊔ ≥1▽.((B1 ⊔ B2) ⊓ ¬B)

Case 9: Combining P -,0 T (r) with a positive TBox premise in P + T (r), e.g., Ci ⊔≥xir.Di (1 ≤ i ≤ m), yields a set of TBox clauses, denoted by BLOCK(P -,0 T (r),Ci ⊔ ≥xir.Di). In this case, P -,0 T (r) denotes the set of negative TBox premises of the form E ⊔ ≤0r.F (i.e., cardinality constraints are 0).

Example 2 CombiningP -,0 T (r) = {A1⊔≤0r.B1,A2⊔≤0r.B2} with {A⊔≥2r.B} yields a set BLOCK(P -,0 T (r),A⊔≥2r.B) that contains the following subsets of clauses:

Ground BLOCK: {A⊔≥2▽.B}

1st-tier BLOCK: {A ⊔ A1 ⊔ ≥2▽.(B ⊓ ¬B1)}

2nd-tier BLOCK: {A ⊔ A1 ⊔ A2 ⊔ ≥2▽.(B ⊓ ¬B1 ⊓ ¬B2)}

How are the Ackermann rules used? For a set N of clauses in reduced form, depending on which kinds of premises the set N contains, we apply different Ackermann rules (to the premises in N to eliminate the pivot). Specifically, if N contains only positive premises, we apply the Ackermann I rule. If N contains only negative premises, we apply the Ackermann II rule. If N contains only positive TBox premises, as well as negative premises, we apply the Ackermann III rule. If N contains only positive RBox premises, as well as negative premises, we apply the Ackermann IV rule. If N contains both positive TBox and RBox premises, as well as negative premises, we apply the Ackermann V rule. Note that there is a gap in the scope of the rules in the Ackermann V rule; it is applicable only to the cases where all negative TBox premises (if they are present in N) are of the form E ⊔≤0r.F.

Theorem 3 Let I be any ALCOQH(▽)-interpretation. For r ∈ NR the pivot, when an Ackermann rule is applicable, the conclusion of the rule is true in I iff for some interpretation I ′ r-equivalent to I, the premises are true in I ′ .

This implies that the conclusion of an Ackermann rule is a solution of forgetting the pivot from the premises of the rule.

5 Description of the ForgettingMethod

Given an ontology O of axioms and a set Σ of role symbols to be forgotten, the forgetting process in our method comprises three main phases (see Figure 2): the conversion of O into a set N of clauses (the first phase), the Σ-symbol elimination phase (the central phase), and the definer elimination phase (the final phase). It is assumed that as soon as a forgetting solution is computed, the remaining phases are skipped.

Input: Given as input to the method are an ALCOQH(▽)- ontology O of axioms and a set Σ ⊆ sigR(O) of role symbols to be forgotten. An important feature of the method is that Σsymbols can be flexibly specified.

The first phase: The first phase of the forgetting process internalizes all ABox assertions in O (if they are present) into TBox axioms, and then transforms O into a set N of clauses using standard clausal form transformations.

The central phase: Central to the forgetting process is the Σ-symbol elimination phase, which is an iteration of several rounds in which the elimination of Σ-symbols is attempted. Specifically, the method attempts to eliminate the Σ-symbols one by one using the approach as described in the previous section. In each elimination round, the method performs two steps. The first step transforms every TBox pivot-clause (not in reduced form) into reduced form, so that one of the Ackermann rules can be applied. The second step then applies the Ackermann rule to the pivot-clauses to eliminate the pivot. Upon the intermediate result being returned at the end of each round, the method repeats the same steps in the next round for the elimination of the remaining symbols in Σ (if necessary). If a Σ-symbol has been found ineliminable from the present ontology (i.e., none of the Ackermann rules is applicable to the current reduced form), the method skips the current round and attempts to eliminate another symbol in Σ.

The final phase: To facilitate the transformation of TBox pivot-clauses (not in reduced form) into reduced form, definer symbols might have been introduced during the elimination rounds. The final phase of the forgetting process attempts to eliminate these definer symbols by using Ackermann-based rules for concept forgetting, which are very similar to the rule in (1) (and its dual); for details see [Koopmann and Schmidt,

2014; Zhao and Schmidt, 2015; 2016]. This allows definer symbols in many cases to be eliminated, because occurrences of one polarity of any definer symbol will be top-level occurrences. There is no guarantee however that all definer symbols can be eliminated, even if we use the generalization of Ackermann's Lemma involving the use of fixpoint operators. In practice, most real-world ontologies are normalized and therefore in reduced form, which means that for such ontologies definer introduction and elimination are obsolete.

Output: What the method returns as output at the end of the forgetting process is a finite set O′ of clauses. If O′ does not contain any symbols in Σ, then the method was successful (in computing a solution of forgetting Σ from O). The following theorem states termination and soundness of the method.

Theorem 4 For any ALCOQH(▽)-ontology O and any set Σ ⊆ sigR(O) of role symbols to be forgotten, the method always terminates and returns a finite set O′ of clauses. (i) If O′ does not contain any symbols in Σ or any newly-introduced definer symbols, then O′ is a solution of forgetting Σ fromO (i.e., O′ is equivalent to the original ontology O up to the symbols in Σ). (ii) If O′ does not contain any symbols in Σ but it contains newly-introduced definer symbols, then O′ is a solution of forgetting Σ from O in an extended language (and O′ and O are equivalent up to the symbols in Σ, as well as the newly-introduced definer symbols present in O′ ).

The method may return an 'O′ ' that still contains some Σsymbols. In this case, the method was not successful. This is because there is a gap in the scope of the rules in the Ackermann V rule, as mentioned before Theorem 3.

Theorem 5 Given an ALCOQH(▽)-ontology O in clausal form and a subset Σ of sigR(O), our method is guaranteed to compute a solution of forgetting Σ from O, possibly with concept definer symbols, iff any one of the following conditions holds for each r ∈ Σ: (i) O does not contain any RBox axioms of the form ¬S ⊔ r for S ̸= r; (ii) O does not contain any TBox axioms with number restrictions of the form ≥mr.D for m ≥ 1; or (iii) O does not contain any TBox axioms with number restrictions of the form ≤nr.D for n ≥ 1.

An explanation of Case (ii) is the following: let O be an ALCOQH(▽)-ontology in clausal form, and let Σ be a subset of sigR(O). For r ∈ Σ the pivot, if O does not contain any TBox axioms with number restrictions of the form ≥mr.D for m ≥ 1, then there will be no positive TBox premises occurring in O (when O is transformed into reduced form). O is thus in the form suitable for application of the Ackermann IV rule. Explanations of Cases (i) and (iii) are similar, i.e., O of Cases (i) and (iii) in reduced form are suitable for application of the Ackermann III and Ackermann V rules, respectively.

6 Evaluation and Empirical Results

To gain insight into the practical applicability of the method, we implemented a prototype in Java using the OWL-API, 2 and evaluated it on two corpora of slightly adjusted real-world ontologies from the NCBO BioPortal repository. 3 The experiments were run on a desktop computer with an Intel® Core TM

2 http://owlapi.sourceforge.net/

3 http://bioportal.bioontology.org/

i7-4790 processor, four cores running at up to 3.60 GHz and 8 GB of DDR3-1600 MHz RAM.

SDO 2738 114 1382 77 59 1305 14 SHOIQ(D)

TA = TBox and ABox Axioms, RA = RBox Axioms, CS = Concept Symbols,

RS = Role Symbols, IS = Individual Symbols, ≥ = ≥-restrictions, ≤ = ≤-restrictions

Figure 3: Ontologies selected from NCBO BioPortal

The corpora used for our experiments were constructed as follows. First, we selected from the NCBO BioPortal repository ontologies containing both number restrictions and role inclusions. Then, we filtered out those containing less than 40 role symbols (since they were less challenging). As a result, 5 ontologies stood out from the repository (see Figure 3 for their profiles). We further adjusted these 5 ontologies to the language of ALCOQH (i.e., none of them included the universal role ▽). This was done by removing those axioms not expressible in ALCOQH and using simple simulations. For example, an exact number restriction =1r.D was simulated by (≥1r.D) ⊓ (≤1r.D), and a functional role func(r) was simulated by ≤1r.⊤. In this way we obtained a corpus (Corpus I) of 5 ALCOQH-ontologies. By removing all role inclusions in each of the ontologies in Corpus I, we obtained another corpus (Corpus II) that contained 5 ALCOQ-ontologies. Using Corpora I and II as test data sets for our experiments, we considered how the presence of role inclusions affected the results of role forgetting, in particular, the success rates.

To fit in with real-world use, we evaluated the performance of forgetting different numbers of role symbols from each test ontology. In particular, we forgot 30% (i.e., a relatively small number) and 70% (i.e., a relatively large number) of role symbols in the signature of each test ontology. The symbols to be forgotten were randomly chosen. We ran the experiments 50 times on each ontology and averaged the results to verify the accuracy of our findings. A timeout of 100 seconds was imposed on each run of the experiment (unit of time: sec.).

• DI = Definers Introduced, SR = Success Rate, GC = Growth of Clauses

Figure 4: Results of forgetting 30% and 70% of role symbols

The results are shown in Figure 4, which is rather revealing in several ways. The most encouraging result was that our implementation was successful (i.e., forgot all symbols in Σ) in all test ontologies (within a short period of time) except in the case of SDO, despite role inclusions being present in them. This was unexpected, but there are obvious explanations (for the 100% success rate cases): inspection revealed that these ontologies did not contain axioms with number restrictions of the form ≤nS.D for n ≥ 1, and the likelihood of Σ-symbols occurring positively in the RBox axioms was very low. What was as expected was that definer symbols were not introduced in the test ontologies (as most real-world ontologies were by design flat and therefore already in reduced form). This gave us best benefits of using our Ackermann approach. Because of the nature of the Ackermann III and V rules, forgetting a role symbol could lead to growth of clauses in the forgetting solution, which was however modest (see the GC column in Figure 4) compared to the theoretical worst case (i.e., 2n - 1 for n the cardinality of P + T ). In the case of SDO the 'hasPart' role occurred positively in more than 50 different TBox clauses in reduced form. This means that if 'hasPart' was chosen as one of the Σ-symbols to be forgotten, then there were more than 50 positive TBox premises in the ontology SDO in reduced form (i.e., n ≥ 50), which led to a blow-up of clauses in the forgetting solution (i.e., ≥250 -1 clauses). Indeed, the failures on SDO were due to space explosion caused by the high frequency of the 'hasPart' role. We found that without this role in Σ, the success rate was 100%.

7 Conclusion and FutureWork

In this paper, we have presented a practical method of semantic role forgetting for ontologies expressible in the description logic ALCOQH(▽). The method is the only approach so far for forgetting role symbols in description logics with number restrictions. This is very useful from the perspective of ontology engineering as it increases the arsenal of tools available to create decompositions and restricted views of ontologies. We have shown that the method is terminating and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols, sometimes with new concept definer symbols. Although our method is not complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on two corpora of real-world biomedical ontologies.

Though the focus of this paper has been the problem of role forgetting, (non-nominal) concept forgetting can be reduced to role forgetting by substituting ≥1r.⊤ for every occurrence of the concept symbol one wants to forget, where r is a fresh role symbol, and then forgetting {r}. For example, forgetting the concept symbol {B} from {¬A⊔≥1s.B} can be reduced to forgetting the role symbol {r} from {¬A⊔≥1s.≥1r.⊤}. Thus our method also provides an incomplete approach to concept forgetting for ALCOQH(▽)-ontologies.

A natural next step for future work is to extend the method to accommodate transitive properties on roles, though it is realized when forgetting role symbols, the interaction between transitivity and role inclusions can lead to results where it is not clear how to represent them finitely [Koopmann, 2015].

Acknowledgments

We thank the anonymous referees for very useful comments.