Forgetting Concept and Role Symbols in ALCOIHµ+(∇, ⊓)-Ontologies

1 Introduction

This paper presents a practical forgetting method for creating restricted views of ontologies expressed in the language of the description logic ALCOIHθ+(O↪ u). The work is motivated by the high demand for advanced techniques for ontology-based knowledge processing. Research of forgetting, often referred to as uniform interpolation (also known as variable elimination, projection or second-order quantifier elimination) has gained significant momentum since the work of various groups developing forgetting methods for the description logic ALC and logics weaker than ALC, e.g., [Konev et al., 2009b; Lutz et al., 2012; Ludwig and Konev, 2014; Nikitina and Rudolph, 2014; Wang et al., 2009; 2014], and the foundational studies of the properties of forgetting for description logics by, e.g., [Wang et al., 2008; Konev et al., 2009a; Lutz and Wolter, 2011; Lutz et al., 2012; Konev et al., 2013]. These works give arguments for the important role of forgetting in realizing various tasks crucial for effective processing and management of ontologies. For example, forgetting can be used for ontology analysis, for creating ontology summaries, for ontology reuse, for information hiding, for computing the logical difference between ontologies, for ontology debugging and repair, and for query answering.

Early work in the area primarily focused on forgetting concept symbols, as role forgetting was realized to be significantly harder than forgetting of concept symbols [Wang et al., 2008], because the result of forgetting role symbols often requires more expressivity than is available in the target logic. Although the earliest work did study concept and role forgetting, e.g. [Wang et al., 2009], most subsequent work considered only concept forgetting with the exception of [Koopmann and Schmidt, 2013a; 2013b; 2014; 2015]. Their method can perform both concept and role forgetting for description logics extending ALC up to and including description logics with the expressiveness of SH, SIF and SHQ. In addition they have extended their method to forgetting for description logics with ABoxes for logics between ALC and SHI.

The work on forgetting for description logics is predated by work on second-order quantifier elimination [Gabbay and Ohlbach, 1992; Szałas, 1993; Nonnengart and Szałas, 1999; Doherty et al., 1997; Gabbay et al., 2008], which can be traced to questions posed by Boole and seminal work of [Ackermann, 1935]. These works triggered and influenced work in knowledge representation [Lin and Reiter, 1994; Wernhard, 2011], but also led to striking results in the automation of correspondence theory of modal logics [Gabbay and Ohlbach, 1992; Conradie et al., 2006; Schmidt, 2012]. Because of the close relationship between description logics and modal logics, besides the work on modal correspondence theory, investigations of uniform interpolation for modal logics and the θ-calculus [Visser, 1996; Herzig and Mengin, 2008; D'Agostino and Hollenberg, 2000] are relevant. These are related to concept forgetting, but not to role forgetting.

The contribution of this paper is an approach for forgetting of concept and role symbols in expressive description logics not considered so far. The method accommodates ontologies expressible in the description logic ALCOIH and the extension allowing positive occurrences of the least fixpoint operator θ, the top role O and role conjunction u. This means the method is one of only few approaches that can eliminate role symbols, while also handling role inverse, ABox statements, and the only approach so far providing support for forgetting in description logics with nominals. The added expressivity has the advantage that it reduces information loss; for instance, the solution of forgetting the role symbol r in the ontology ¶A v 9r▷B↪ 9r▷B v B♦ is ¶A v 9O▷B↪ A v B♦, whereas in a description logic without the top role (or ABox axioms or nominals) the uniform interpolant is ¶A v B♦, which is weaker.

Being based on the Ackermann approach to second-order quantifier elimination [Doherty et al., 1997; Szałas, 2006; Schmidt, 2012; Zhao and Schmidt, 2015] the method terminates always. We have shown that the method is correct, i.e., the forgetting solution computed is equivalent to the original ontology up to the symbols that have been forgotten. A general problem of forgetting is marking out a language expressive enough to allow for solutions to be given by finitely many formulas, while being not too expressive so that the forgetting solutions returned can be further processed by available tools. For example, including second-order quantifiers of concept and role symbols in the language solves the forgetting problem trivially, but tool support would be absent. Even though concept forgetting becomes possible with fixpoint operators, at present mainstream tools do not support fixpoints. We avoid this problem by restricting occurrences of fixpoints in our logic to cases that can be simulated without them. Despite our method not being complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies.

2 The Description Logic ALCOIHθ+(O↪ u)

We assume that a TBox T is a set of concept axioms of the form C v D, where C and D are closed concepts, i.e., contain no concept variable not in the scope of a θ operator. An RBox R is a set of role axioms of the form R v S, where R and S are role symbols or inverted role symbols. An ABox is a set of concept assertions of the form C(a) and role assertions of the form R(a↪ b). In description logics with nominals ABox assertions are superfluous, since they can be equivalently expressed as TBox axioms, namely, C(a) as a v C and R(a↪ b) as a v 9R▷b. Hence, we assume an ontology is the union of a TBox and an RBox.

Let NC, NR and NO be mutually disjoint sets of concept symbols (names), role symbols (names) and individuals, respectively, and let Nθ be a set of concept variables disjoint with NC, NR and NO. Roles in ALCOIH(O↪ u) can be the top role O, a role symbol r 2 NR, the inverse r- of a role symbol r (an inverted role symbol), or can be formed with conjunction. Concepts in ALCOIH(O↪ u) have one of the following forms: a ♣ > ♣ A ♣ ≻C ♣ C t D ♣ 8R▷C, where a 2 NO, A 2 NC, C and D are any concepts, and R is any role in ALCOIH(O↪ u). We assume w.l.o.g. that concept and role expressions are equivalent relative to associativity and commutativity of u and t, ≻ and - are involutions, and > and O are units w.r.t. u.

The language of ALCOIHθ+(O↪ u) extends that of ALCOIH(O↪ u) with atomic least fixpoint expressions of the form θX▷C[X], where X 2 Nθ and C[X] is a concept expression in which X occurs only positively (under an even number of explicit and implicit negations) in place of a regular concept symbol. Moreover, θ-expressions may occur only positively. Because of this restriction, θ-expressions can be simulated in ALCOIH(O↪ u) with auxiliary concept symbols as in [Koopmann and Schmidt, 2013b].

The semantics of ALCOIHθ+(O↪ u) is defined in terms of an interpretation I = h∆I ↪ ·I i, where ∆I is any nonempty set, and ·I assigns to every nominal a 2 NO a singleton set aI ✓ ∆I , to every concept symbol A 2 NC a subset AI of ∆I , and to every role symbol r 2 NR a subset rI of ∆I ⇥∆I . The interpretation function ·I is inductively extended to concept and role expressions as follows:

The semantics of least fixpoint expressions takes additionally an assignment function ·V , mapping concept variables to subsets of ∆I , which is defined by: (θX▷C)I↪V = T¶E ✓ ∆I ♣ C I↪V[X◁E] ✓ E♦, where V[X◁E] denotes an assignment function identical to ·V except that XV = E. C I↪V is the interpretation C I of C that adopts the assignment function ·V , and C I↪V = C I when ·V is defined for all variables in C.

Theorem 1 Reasoning in ALCOIHθ+(O↪ u) is decidable.

A concept axiom C v D is true in an interpretation I iff C I ✓ DI , and a role axiom R v S is true in I iff RI ✓ SI . I is a model of an ontology O iff every axiom in O is true. In this case we write I ♣= O.

This follows, e.g., from the decidability of guarded fixpoint logic [Gr¨adel and Walukiewicz, 1999] or the description logic ALBOid [Schmidt and Tishkovsky, 2014] (because positive occurrences of θ-expressions can be encoded). Reasoning in ALCOIHθ+(O↪ u) can be performed with MetTeL, which decides ALBOid [Tishkovsky et al., 2012].

The normal form of our method are axioms in clausal normal form. A TBox clause is a disjunction of a finite number of ALCOIHθ+(O↪ u)-concepts. A role literal is a role symbol, an inverted role symbol, or formed with negation. An RBox clause is a disjunction of exactly two role literals of complementary polarity. TBox and RBox clauses are obtained by clausification of the TBox and RBox axioms, where in the case of role axioms role negation is introduced. Nominals are treated like regular concept symbols in our method, except that they cannot be specified as symbols to be forgotten.

A clause that contains a designated concept (role) symbol S is called an S-clause. Given an S-clause C, an occurrence of S is positive in C if it is under an even number of explicit and implicit negations, otherwise it is negative. For instance, an occurrence of r is assumed to be negative in 8r▷A and r v s, and positive in ≻8r▷A and s v r. C is positive (negative) w.r.t. S if every occurrence of S in C is positive (negative). A set N of clauses is positive (negative) w.r.t. S if every occurrence of S in N is positive (negative).

We now formalize our notion of forgetting. By sig(E) we denote the concept and role symbols occurring in E excluding nominals, where E ranges over all concepts, axioms, clauses, a set of clauses and ontologies. Let S be any concept or role symbol and let I and I 0 be interpretations. We say I and I 0 are equivalent up to S, or S-equivalent, if I and I 0 coincide but differ possibly in the interpretations of S. More generally, I and I 0 are equivalent up to a set ⌃, or ⌃-equivalent, if I and I 0 are the same but differ possibly in the interpretations of the symbols in ⌃. In this paper, ⌃ is assumed to be the set of the concept and role symbols to be forgotten.

Definition 1 (Forgetting for ALCOIHθ+(O↪ u)) Let O and O0 be ALCOIHθ+(O↪ u)-ontologies and let ⌃ be any subset of sig(O). O0 is the solution of forgetting the ⌃-symbols in O, if the following conditions hold: (i) sig(O0 ) ✓ sig(O) and sig(O0 ) \ ⌃ = ;, and (ii) for any interpretation I: I ♣= O0 iff I 0 ♣= O, for some interpretation I 0 ⌃-equivalent to I.

This states that the given ontology O and the forgetting solution O0 are equivalent up to the interpretations of the symbols in ⌃. Forgetting solutions are unique up to equivalence.

3 Overview of the ForgettingMethod

The forgetting process in our method consists of three main phases: the reduction to a set of ALCOIHθ+(O↪ u)-clauses, the forgetting phase and the definer elimination phase (see Figure 1). In the forgetting phase, an analyzer may be used to generate forgetting orderings, ≻C and ≻R, of the concept symbols and role symbols in ⌃.

The input to the method is an ontology O of TBox and RBox axioms expressible in ALCOIHθ+(O↪ u), and a set ⌃ with the concept and role symbols to be forgotten. The ⌃- symbols are entirely determined by the user and their application demands; ⌃ can thus be any subset of the signature of the initial ontology as the user wishes. The first phase transforms the input ontology O into a set N of clauses.

The forgetting phase is an iteration of several rounds in which individual concept and role symbols are eliminated. An important feature of the method is that concept symbols and role symbols are forgotten in a focused way, i.e., the rules for concept forgetting and the rules for role forgetting are mutually independent; concept and role symbols can therefore be forgotten in any order. In the forgetting phase, if S 2 ⌃ is a symbol to be forgotten, the idea is to transform the S-clauses into S-reduced form, so that the forgetting rules, specifically the Ackermann rules, can be applied to eliminate S. Thus, whether the ⌃-symbols are eliminable depends entirely upon whether the current set of clauses can be transformed into corresponding reduced forms. For A a concept symbol, the conversion to A-reduced form is performed using the rewrite rules in the calculus for concept forgetting, while for r a role symbol, the conversion to r-reduced form is realized using the rewrite rules in the calculus for role forgetting. The calculi are described in the next sections. To provide crucial control and flexibility in how the steps are performed, auxiliary concept symbols, called definer symbols, are introduced in the role forgetting rounds. The final phase in the method attempts to eliminate these using concept forgetting.

Previous research has shown that the success rates of forgetting depend very much upon the order in which the ⌃-symbols are forgotten [Gabbay and Ohlbach, 1992; Doherty et al., 1997; Conradie et al., 2006; Schmidt, 2012; Koopmann and Schmidt, 2014], even when forgetting only concept symbols, e.g., [Ludwig and Konev, 2014; Zhao and Schmidt, 2015]. An important challenge therefore is to find appropriate orderings for eliminating ⌃-symbols. Our method either follows the user-specified ordering, or it uses a heuristic analysis based on frequency counts of the ⌃- symbols, where concept symbols and role symbols are analyzed separately.

We refer to the maximal symbol of ⌃ w.r.t. the forgetting ordering ≻ as the pivot in our method. Following ≻ (and starting with the pivot), the method forgets the ⌃-symbols one by one. If the pivot is successfully eliminated from N, we attempt to forget the next symbol in the ordering ≻, which has become the new pivot. Otherwise the pivot is flagged as a currently non-forgettable symbol and remains in ⌃. The next symbol in ≻ then becomes the pivot. When the end of the ordering ≻ has been reached, the calculus is applied to the flagged symbols, attempting again to eliminate them. Success will always be pursued until a forgetting solution is found. Though the ordering ≻ provides useful guidance during the forgetting process, it does not generally guarantee success of forgetting. On the symbols not eliminated, a different ordering not attempted before, will be used. When all possible orderings have been attempted and there are still ⌃-symbols remaining, our method has been unable to find a forgetting solution (because it is unable to find a suitable reduced-form for the non-forgettable symbols).

Inexpensive equivalence-preserving simplification rules are applied throughout the forgetting process, ensuring that the current clauses are always simple representations for efficiency. Our experimental results suggest that the simplification rules are also crucial to the success of concept forgetting, as they can help conversion of clauses to reduced form, when the pivot is a concept symbol. What the method returns, if forgetting is successful, is an ontology O0 that does not contain the symbols in ⌃.

Theorem 2 For any ALCOIHθ+(O↪ u)-ontology O and any set ⌃ ✓ sig(O) of symbols to be forgotten, the method always terminates and returns a set O0 of clauses. If O0 does not contain any ⌃-symbols, the method was successful. O0 is then a solution of forgetting the symbols in ⌃ from O.

If neither O nor O0 uses fixpoints, O0 is ⌃-equivalent to O in ALCOIH(O↪ u). Otherwise, it is ⌃-equivalent to O in ALCOIHθ+(O↪ u).

4 Calculus for Concept Forgetting

This section presents the calculus for forgetting concept symbols from ontologies expressible in ALCOIHθ+(O↪ u). The calculus extends the calculus of [Zhao and Schmidt, 2015] for concept forgetting in ALCOI-ontologies by accommodating the top role in the calculus and allowing the least fixpoint operator to occur in the forgetting solutions for problems that contain cyclic dependencies. Since concept symbols occur only in TBox axioms, only the TBox needs to be processed for concept forgetting. The RBox remains unchanged.

Definition 2 (A-Reduced Form) Suppose A is a concept symbol. A clause is in A-reduced form if it is negative w.r.t. A, or it has the form AtC, where C is an ALCOIHθ+(O↪ u)- concept that (i) does not have any occurrences of A, or (ii) is negative w.r.t. A. A set N of clauses is in A-reduced form if every A-clause in N is in A-reduced form.

The AckermannC rules and the PurifyC rule, given in Figure 2, are the forgetting rules that lead to the elimination of concept symbols in a set of clauses. For A 2 NC the pivot and C a concept expression, N A C denotes the set obtained from N by replacing every occurrence of A by C. We refer to the clauses of the form Ci t A and Ci[A] t A (1  i  n) as positive premises of the Non-Cyclic AckermannC rule and the Cyclic AckermannC rule, respectively. The AckermannC rules are applicable to forget A in N only if N is in Areduced form.

Theorem 3 (Ackermann Lemma, Concept Forgetting)

Let I be any ALCOIHθ+(O↪ u)-interpretation. For A the pivot, when the Non-Cyclic AckermannC rule is applicable, the conclusion of the rule is true in I iff for some interpretation I 0 A-equivalent to I, the premises are true in I 0 . The

provided: (i) A does not occur positively in C, and (ii) A occurs positively in 8R▷D.

provided: (i) A occurs positively in ≻8R▷C, and (ii) b is a fresh nominal.

provided: (i) A occurs positively in ≻8O▷D, and (ii) b is a fresh nominal.

Sign Switching N

provided: A occurs positively in C1 t ▷ ▷ ▷ t Cn.

N A

≻A provided: (i) N is closed w.r.t. the other rewrite rules, and (ii) Sign Switching has not been performed on A.

Figure 3: The rewrite rules for finding A-reduced form

same is true for the Cyclic AckermannC and the PurifyC rules.

This states that eliminating the pivot symbol with the AckermannC and PurifyC rules preserves equivalence up to the pivot. Given a pivot A 2 NC and a set N of clauses in A-reduced form, the AckermannC and PurifyC rules are applied in different situations. Specifically, the Non-Cyclic AckermannC rule is applied when A does not occur in the concepts Ci of the positive premises (1  i  n). The Cyclic AckermannC rule is applied when A occurs in the Ci but only negatively (e.g., A in the cyclic clause At≻8r▷A). Fixpoints are introduced in this case in order to facilitate finite representation of the forgetting solution, where every occurrence of A in ≻C1 t ▷ ▷ ▷ t ≻Cn is replaced by X, a fresh concept variable, and every occurrence of A in N is replaced by θX▷(≻C1 t ▷ ▷ ▷ t ≻Cn)[X]. The PurifyC rule can be applied any time provided that A is pure in N, i.e., N is positive (or negative) w.r.t. A.

Figure 3 lists a set of rewrite rules for finding the pivotreduced form of a clause for the pivot a concept symbol. New compared to [Zhao and Schmidt, 2015], besides the Cyclic AckermannC rule, is the SkolemizationO rule that rewrites existential restrictions over the top role by the introduction of fresh nominals. The Case Splitting rule splits the derivation into several branches. The intermediate result returned at the end of a symbol elimination round is the disjunction of the solutions of each branch in the derivation. Crucial to the practicality of our method are a number of equivalencepreserving simplification rules, not described here.

It follows from [Schmidt, 2012; Zhao and Schmidt, 2015], which this work extends, that our method for concept forgetting succeeds on problems corresponding to the modal classes of C and C≻ [Schmidt, 2012], which subsume the class of Sahlqvist formulas [Sahlqvist, 1975] and the class of monadic inductive formulas [Goranko and Vakarelov, 2006].

5 Calculus for Role Forgetting

The main contribution of this paper is a calculus for goaloriented forgetting of role symbols in ontologies expressible in ALCOIHθ+(O↪ u). Since role symbols also occur in the RBox, both the TBox and the RBox need to be processed when role symbols are to be forgotten.

Definition 3 (r-Reduced Form) Suppose r is a role symbol. A clause is in r-reduced form if it has the form C t 8r▷D or C t ≻8r u Q▷D, where C and D are ALCOIHθ+(O↪ u)- concepts that do not contain any occurrence of r and Q is a role that does not contain any occurrence of r; or it has the form ≻S t r or S t ≻r, where S 2 ¶s↪ s-♦ and s (6= r) is a role symbol. A set N of clauses is in r-reduced form if every r-clause in N is in r-reduced form.

As in concept forgetting, the pivot-clauses are first transformed into pivot-reduced form, so that the Ackermann rule for role forgetting becomes applicable (to eliminate the pivot). Finding the pivot-reduced form of a clause is however not always possible unless definer symbols are introduced. Definer symbols are specialized concept symbols that do not occur in the present ontology [Koopmann and Schmidt, 2013b], and are introduced as follows: given a clause of the form C t 8r(-) ▷D or C t ≻8r(-) ▷D, with r being the pivot and occurring in Q 2 ¶C↪D♦, the definer symbols are used as substitutes, incrementally replacing C and D until neither contains any occurrences of r. A new clause ≻D t Q is added to the clause set for each replaced subconcept Q, where D is a fresh definer symbol. For example, introducing a definer symbol D1 leads to At ≻8r▷8r▷B being rewritten with A t ≻8r▷D1 and ≻D1 t 8r▷B, where A and B are concept symbols. The definer symbols are eliminated (if they were introduced in the conversion of clauses to the pivot-reduced form) using the rules for concept forgetting once all role symbols in ⌃ have been forgotten. It is for this reason that our implementation defaults to forgetting role symbols first so that the definer symbols can be eliminated as part of subsequent concept forgetting.

Since the underlying language accommodates role inverse, the calculus includes two Role Surfacing rules (shown in Figure 4) to reformulate expressions without occurrences of inverses of the pivot in the TBox and RBox clauses, and to free the other rules in the calculus from needing to cater for role inverse. The Role Surfacing rules are applied after definer symbols have been introduced (if necessary), and before the application of the forgetting rules.

Theorem 4 (Ackermann Lemma, Role Forgetting) Let I be any ALCOIHθ+(O↪ u)-interpretation. For r the pivot, when the AckermannR or PurifyR rule is applicable, the conclusion of the rule is true in I iff for some interpretation I 0 r-equivalent to I, the premises are true in I 0 .

Given a set N of clauses with r 2 NR being the pivot, once N has been transformed into r-reduced form, we apply the AckermannR rule given in Figure 5 to eliminate r. The PurifyR rule can be applied any time provided that r is pure. By definition, clauses in r-reduced form have four distinct forms. We refer to the clauses of the formC j t≻8ruQj ▷Dj (1  j  k) as positive TBox premises (denoted by P + T )

and clauses of the form Ci t 8r▷Di (1  i  m) as negative TBox premises (denoted by P - T ) of the rule. We refer to the clauses of the form ≻T l t r (1  l  u) as positive RBox premises (denoted by P + R) and clauses of the form ≻r t Si (1  i  n) as negative RBox premises (denoted by P - R ) of the rule. Since it is possible for r to occur in any of these premises (and the premises do not necessarily all exist), there are several situations where the AckermannR rule is applicable. For different P - T and P - R the AckermannR rule is performed as follows.

Case (I): If P - T 6= ; and P - R 6= ;, then P - T and P - R (the negative premises) are combined with every clause in P + T (if P + T 6= ;) and every clause in P + R (if P + R 6= ;), which leads to the elimination of r, and a forgetting solution O0 such that r 62 sig(O0 ). Specifically, combining P - T and P - R with one of the positive TBox premises (P + T ) yields a set of TBox clauses (denoted by T -BlockH(j↪m)), where Hj is the conjunction of Qj and the Si (1  i  n) in P - R (Hj = Qj uS1u▷ ▷ ▷uSn), and m denotes the number of negative TBox premises (♣P - T ♣), and j refers to the positive TBox premise with which P - T andP - R combine. [m] denotes the set ¶1↪ ▷ ▷ ▷ ↪m♦, and ¶C j t C Y t ≻8Hj ▷(Dj tDY )♣Y ✓ [m]♦ is the set that contains all clauses corresponding to every assignment of Y . The following example illustrates this case.

Example 1 Given ⌃ = ¶r♦ and a set N of clauses in r-reduced form with P - T = ¶A1 t 8r▷B1↪A2 t 8r▷B2♦, P - R = ¶≻rts1↪ ≻rts-2 ♦, and ≻at≻8r▷B 2 P + T , combining P - T and P - R with ≻a t ≻8r▷B leads to T -BlockH(j↪m) = ¶≻a t C Y t ≻8(s1 u s-2 )▷(B t DY )♣Y ✓ [2]♦ that consists of the following clauses:

Case (II): If P - T 6= ; and P - R = ;, then combining P - T with one of the positive TBox premises yields the same result as in Case (I) (T -BlockH(j↪m)), only that O replaces S1 u ▷ ▷ ▷ u Sn in Hj , i.e., Hj = O u Qj (1  j  k). Combining P - T with one of the positive RBox premises yields the same result as in Case (I), i.e., R-BlockC (l↪m) (1  l  u). Case (III): If P - T = ; and P - R 6= ;, then combining P - R with one of the positive TBox premises and with one of the pos-

Combining P - T with one of the positive RBox premises yields a set of TBox clauses (denoted by R-BlockC (l↪m)), where m ranges over the negative TBox premises and l refers to the positive RBox premise with which P - T combines; combining P - R with one of the positive RBox premises yields a set of RBox clauses (denoted by R-BlockR(l↪ n)), where n ranges over the negative RBox premises and l refers to the positive RBox premise with which P - R combines.

itive RBox premises yields the same results as in Case (I), i.e., T -BlockH(j↪m) (1  j  k) and R-BlockR(l↪ n) (1  l  u), respectively. Case (IV): The case P - T = ; and P - R = ; can be seen as an instance of the case where r is pure and then eliminated using the PurifyR rule.

The pivot is forgotten in the ontology once every premise in P + T and every premise in P + R, i.e., the positive premises, have been combined with P - T (if P - T 6= ;) and P - R (if P - R 6= ;). Given a set of clauses in pivot-reduced form and m negative TBox premises (♣P - T ♣ = m), n negative RBox premises (♣P - R ♣ = n), k positive TBox premises (♣P + T ♣ = k), and u positive RBox premises (♣P + R♣ = u), combining P - T and P - R with all positive TBox premises yields k2m clauses (exponential growth); combining P - T and P - R with all positive RBox premises yields um + un clauses (polynomial growth). The size of the forgetting solution therefore depends largely upon the number of the negative TBox premises (m).

6 Evaluation and Empirical Results

We have implemented a prototype of the forgetting method in Java using the OWL-API 1 and conducted two series of experiments on real-world ontologies to evaluate the practicality of the method. The experiments were run on a desktop with an Intelr Core TM i7-4790 processor, and four cores running at up to 3.60 GHz and 8 GB of DDR3-1600 MHz RAM. The ontologies used for our evaluation were taken from the NCBO BioPortal 2 and Oxford Ontology 3 repositories and were restricted to the ALCOIH(O↪ u)-fragments; any subconcepts beyond the scope of ALCOIH(O↪ u) were replaced by >. Consequently, 180 and 200 ontologies of various sizes were selected from the NCBO BioPortal and Oxford Ontology repositories, respectively. We repeated the experiments 100 times on each ontology and averaged the results to verify the accuracy of our findings.

To fit in with real-world applications such as computing logical difference between ontologies and predicate hiding, where forgetting a small number of symbols is in demand, we set up a series of experiments where we forgot 10% and 30% of concept and role symbols in each ontology. There are also situations where it would be of interest to forget a large number of symbols; ontology reuse is such an example [Koopmann and Schmidt, 2013a; 2013b; 2014; 2015]. We therefore set up another series of experiments where we forgot 80% of the concept symbols and 50% of the role symbols in each ontology. The symbols to be forgotten were randomly selected in the experiments. The heuristic for determining the orders of eliminating concept and role symbols (≻C and ≻R) was also tested. When the heuristic was not applied, the ⌃-symbols were eliminated in the order as returned by the OWL-API function that gets all concept and role symbols in the ontology. We started the evaluation with concept forgetting, where a timeout of 15 minutes was used.

The results obtained from forgetting 10%, 30% and 80%

1 http://owlapi.sourceforge.net/

2 http://bioportal.bioontology.org/

3 http://www.cs.ox.ac.uk/isg/ontologies/

of the concept symbols from the respective BioPortal and Oxford ontologies are shown in Figure 6, which is revealing in several ways. The most notable observation to emerge from the results is that, with the heuristically determined forgetting ordering (indicated by 3), our implementation was successful (forgot all the concept symbols in ⌃) in 96.7% of the BioPortal-cases within a short period of time, with 8.3% of them using fixpoints in the result. In the experiments of 10% of the concept symbols specified to be forgotten, the success rate rose to 100%. Even when not using the heuristic (7), the forgetting solution could be found in 92.6% of the cases. Since the Oxford ontologies were more than twice as large as the BioPortal ontologies and a larger set of concept symbols was specified to be forgotten, a reduction in the performance was expected. The implementation was unable to compute the solution in 11.5% of the Oxford-cases, and in 13.8% of the solved ones fixpoints occurred in the result. The use of the heuristic boosted the overall success rate by 4% and 9.2%, and improved the time efficiency by 124.1% and 136.9% in the BioPortal and Oxford ontologies, respectively.

We evaluated the performance of forgetting different numbers of role symbols with the same ontologies used for the evaluation of concept forgetting (using a timeout of 5 minutes). The results are shown in Figure 7, from which it can be seen that our implementation was successful (forgot all the role symbols in ⌃) in all cases. The time used for forgetting role symbols (including the time for the elimination of definer symbols), as expected, was significantly longer than forgetting the same number of concept symbols, despite the 100% success rate. Because of the nature of the AckermannR rule, role forgetting leads to growth of clauses in the forgetting solution, which was however modest (see Clause ") compared to the theoretical worst case. Definer symbols were introduced only in a small proportion of the ontologies to help conversion to reduced form. This indicates that most clauses in the ontologies were flat. By m◁onto, we mean there were on average m definer symbols introduced in each ontology, and by n onto, we mean that n of all ontologies introduced definer symbols. These definer symbols were successfully eliminated in the subsequent definer elimination phase (D. Left).

Suppose that r 2 NR is the pivot and a set of clauses is in r-reduced form with ♣P + T ♣ ≥ 1 (since role conjunction can only occur in the positive TBox premises). Role forgetting can lead to role conjunctions occurring in forgetting solutions in these situations: (i) Role conjunction already occurs in at least one of the positive TBox premises, i.e., C t ≻8r u Q▷D 2 P + T , where Q is a role. (ii) If none of the positive TBox premises includes role conjunction, then having at least two negative RBox premises (♣P - R ♣ ≥ 2) yields a forgetting solution including role conjunction. In our evaluation it was however found that neither of these cases happened often; in most cases, rather the opposite occurred: the positive TBox premises were in the simple form C t ≻8r▷D and often ♣P - R ♣  1. Only in 8.9% of the tested cases role conjunction occurred in the forgetting solutions.

7 Conclusion and FutureWork

In this paper we have developed a method of concept and role forgetting for expressive description logics with nominals, non-empty TBoxes and ABoxes, and a rich language for expressing properties of roles. The method can handle role inclusion statements, role conjunctions and role inverses. This is extremely useful from the perspective of ontology engineering as it increases the arsenal of tools available to create restricted views of ontologies. The results of the evaluation on real-world ontologies have shown that often fixpoints and role conjunction are not needed to express forgetting solutions, and overall the performance results are very positive.

Currently beyond the scope of our method are forgetting transitive roles. We can extend the method to eliminate concept symbols in the presence of transitive roles, but when forgetting role symbols the interaction between transitive roles and role inclusion statements can lead to results where it is not clear how to represent them finitely; see [Koopmann, 2015] for an example. The problem of extending the method to handle role functionality and numerical quantifier restrictions remains completely open; possibly the techniques of [Koopmann and Schmidt, 2014; 2015] can help extend the method.

Acknowledgments

We thank the anonymous reviewers for useful comments.