# forgetting_concept_and_role_symbols_in__8687f0df.pdf

Forgetting Concept and Role Symbols in

ALCOIHµ+(O, u)-Ontologies

Yizheng Zhao and Renate A. Schmidt

The University of Manchester, UK

Forgetting is a non-standard reasoning problem concerned with creating restricted views for ontologies relative to subsets of their initial signatures while preserving all logical consequences up to the symbols in the restricted views. In this paper, we present an Ackermann-based approach for forgetting of concept and role symbols in ontologies expressible in the description logic ALCOIHµ+(O, u). The method is one of only few approaches that can eliminate role symbols, that can handle role inverse, ABox statements, and is the only approach so far providing support for forgetting in description logics with nominals. Despite the inherent difﬁculty of forgetting for this level of expressivity, performance results with a prototypical implementation have shown very good success rates on real-world 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 quantiﬁer elimination) has gained signiﬁcant 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 signiﬁcantly 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 quantiﬁer 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 inﬂuenced 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 ﬁxpoint 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},

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

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 quantiﬁer 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 ﬁnitely 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 quantiﬁers 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 ﬁxpoint operators, at present mainstream tools do not support ﬁxpoints. We avoid this problem by restricting occurrences of ﬁxpoints 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)

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.

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 superﬂuous, 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.

The language of ALCOIHµ+(O, u) extends that of ALCOIH(O, u) with atomic least ﬁxpoint 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 deﬁned in terms of an interpretation I = h I, Ii, where I is any nonempty set, and I assigns to every nominal a 2 NO a singleton set a I I, to every concept symbol A 2 NC a subset AI of I, and to every role symbol r 2 NR a subset r I of I I. The interpretation function I is inductively extended to concept and role expressions as follows:

>I = I OI = I I ( C)I = I\CI

(C t D)I = CI [ DI (R u S)I = RI \ SI

(8R.C)I = {x 2 I | 8y.(x, y) 2 RI ! y 2 CI}

(R )I = {(y, x) 2 I I | (x, y) 2 RI}

The semantics of least ﬁxpoint expressions takes additionally an assignment function V, mapping concept variables to subsets of I, which is deﬁned by: (µX.C)I,V = T{E I | CI,V[X/E] E}, where V[X/E] denotes an assignment function identical to V except that XV = E. CI,V is the interpretation CI of C that adopts the assignment function V, and CI,V = CI when V is deﬁned for all variables in C.

A concept axiom C v D is true in an interpretation I iff CI 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. Theorem 1 Reasoning in ALCOIHµ+(O, u) is decidable. This follows, e.g., from the decidability of guarded ﬁxpoint 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 Met Te L, 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 ﬁnite 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 clausiﬁcation 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 speciﬁed 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 I0 be interpretations. We say I and I0 are equivalent up to S, or S-equivalent, if I and I0 coincide but differ possibly in the interpretations of S. More generally, I and I0 are equivalent up to a set , or -equivalent,

if I and I0 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.

Deﬁnition 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 I0 |= O, for some interpretation I0 -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 Forgetting Method

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 deﬁner 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 .

Convert to set of clauses N

Transform to r-reduced form

to forget r

Transform to A-reduced form

Ackermann to forget A Elimination of deﬁner symbols

Forgetting solution O

Analyzer = {S1, ..., S2} into

Figure 1: Overview of the forgetting method

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 ﬁrst 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, speciﬁcally

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 ﬂexibility in how the steps are performed, auxiliary concept symbols, called deﬁner symbols, are introduced in the role forgetting rounds. The ﬁnal 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 ﬁnd appropriate orderings for eliminating -symbols. Our method either follows the user-speciﬁed 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 ﬂagged 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 ﬂagged 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 ﬁnd a forgetting solution (because it is unable to ﬁnd a suitable reduced-form for the non-forgettable symbols).

Inexpensive equivalence-preserving simpliﬁcation rules are applied throughout the forgetting process, ensuring that the current clauses are always simple representations for efﬁciency. Our experimental results suggest that the simpliﬁcation 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 ﬁxpoints, 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 ﬁxpoint 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.

Non-Cyclic Ackermann C

N, C1 t A, . . . , Cn t A

C1t...t Cn provided: (i) A does not occur in the Ci, and (ii) N is

negative w.r.t. A. Cyclic Ackermann C

N, C1[A] t A, . . . , Cn[A] t A

µX.( C1t...t Cn)[X] provided: (i) the Ci are negative w.r.t. A, and (ii) N is

negative w.r.t. A. Purify C

provided: N is positive (negative) w.r.t. A.

Figure 2: Rules for forgetting pivot A 2 NC

Deﬁnition 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 At C, 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 Ackermann C rules and the Purify C 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 Ackermann C rule and the Cyclic Ackermann C rule, respectively. The Ackermann C 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 Ackermann C rule is applicable, the conclusion of the rule is true in I iff for some interpretation I0 A-equivalent to I, the premises are true in I0. The

Concept Clausify N, C t (D1 t . . . t Dn) N, C t D1, . . . , C t Dn provided: A occurs positively in (D1 t . . . t Dn).

Concept Surfacing N, C t 8R.D N, (8R .C) t D provided: (i) A does not occur positively in C, and (ii)

A occurs positively in 8R.D.

Skolemization R N, a t 8R.C N, a t 8R. b, b t C provided: (i) A occurs positively in 8R.C, and (ii) b is

a fresh nominal.

Skolemization O N, C t 8O.D N, b t D t 8O.C provided: (i) A occurs positively in 8O.D, and (ii) b is

a fresh nominal.

Case Splitting N, a t C1 t . . . t Cn N, a t C1 | . . . | a t Cn provided: A occurs positively in C1 t . . . t Cn.

Sign Switching N 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 ﬁnding A-reduced form

same is true for the Cyclic Ackermann C and the Purify C rules.

This states that eliminating the pivot symbol with the Ackermann C and Purify C rules preserves equivalence up to the pivot. Given a pivot A 2 NC and a set N of clauses in A-reduced form, the Ackermann C and Purify C rules are applied in different situations. Speciﬁcally, the Non-Cyclic Ackermann C rule is applied when A does not occur in the concepts Ci of the positive premises (1 i n). The Cyclic Ackermann C 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 ﬁnite 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 Purify C 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 ﬁnding the pivotreduced form of a clause for the pivot a concept symbol. New compared to [Zhao and Schmidt, 2015], besides the Cyclic Ackermann C rule, is the Skolemization O 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 equivalence-

preserving simpliﬁcation 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.

Role Surfacing to TBox clauses

N, C t 8r .D

N, D t 8r.C provided: r does not occur in C and D. Role Surfacing to RBox clauses

N, S t r provided: S is a role symbol or an inverted role symbol.

Figure 4: The rewrite rules for ﬁnding r-reduced form

Deﬁnition 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 ﬁrst 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 deﬁner symbols are introduced. Deﬁner 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 deﬁner 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 deﬁner symbol. For example, introducing a deﬁner symbol D1 leads to A t 8r.8r.B being rewritten with A t 8r.D1 and D1 t 8r.B, where A and B are concept symbols. The deﬁner 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 ﬁrst so that the deﬁner symbols can be eliminated as part of subsequent concept forgetting.

Ackermann R

N, C1 t 8r u Q1.D1, . . . , Ck t 8r u Qk.Dk ,

T 1 t r, . . . , T u t r ,

C1 t 8r.D1, . . . , Cm t 8r.Dm,

r t S1, . . . , r t Sn

N, T -Block H(1, m), . . . , T -Block H(k, m) ,

R-Block C(1, m), . . . , R-Block C(u, m)

R-Block R(1, n), . . . , R-Block R(u, n)

provided: (i) r does not occur in N, and (ii) N is in

r-reduced form. Purify R

provided: N is positive (negative) w.r.t. r.

Notation in the Ackermann R rule (1 j k, 1 l u): T -Block H(j, m) denotes the set

{Cj t CY t 8Hj.(Dj t DY )|Y [m]}, where

( > if Y = ; F

Ci otherwise, DY =

( > if Y = ; F

Di otherwise,

S1 u . . . u Sn u Qj if P

R 6= ; O u Qj otherwise. R-Block C(l, m) denotes the set

{C1 t 8T l.D1, . . . , Cm t 8T l.Dm}.

R-Block R(l, n) denotes the set { T l t S1, . . . , T l t Sn}.

Figure 5: Rules for forgetting pivot r 2 NR

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 deﬁner 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 Ackermann R or Purify R rule is applicable, the conclusion of the rule is true in I iff for some interpretation I0 r-equivalent to I, the premises are true in I0.

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 Ackermann R rule given in Figure 5 to eliminate r. The Purify R rule can be applied any time provided that r is pure. By deﬁnition, clauses in r-reduced form have four distinct forms. We refer to the clauses of the form Cj t 8r u Qj.Dj (1 j k) as positive TBox premises (denoted by P+

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 Ackermann R rule is applicable. For different P

R the Ackermann R rule is performed as follows.

Case (I): If P

T 6= ; and P

R 6= ;, then P

R (the negative premises) are combined with every clause in P+

T 6= ;) and every clause in P+

R 6= ;), which leads to the elimination of r, and a forgetting solution O0 such that r 62 sig(O0). Speciﬁcally, combining P

R with one of the positive TBox premises (P+

T ) yields a set of TBox clauses (denoted by T -Block H(j, m)), where Hj

is the conjunction of Qj and the Si (1 i n) in P

R (Hj = Qj u S1u. . .u Sn), and m denotes the number of negative TBox premises (|P

T |), and j refers to the positive TBox premise with which P

R combine. [m] denotes the set {1, . . . , m}, and {Cj t CY t 8Hj.(Dj t DY )|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

R with a t 8r.B leads to T -Block H(j, m) = { a t CY t 8(s1 u s

2 ).(B t DY )|Y [2]} that consists of the following clauses:

2 ).(B t > |{z}

a t A1 |{z}

2 ).(B t B1 |{z}

) if Y = {1}

a t A2 |{z}

2 ).(B t B2 |{z}

) if Y = {2}

a t A1 t A2 | {z } CY

2 ).(B t B1 t B2 | {z } DY

) if Y = {1, 2}.

Combining P

T with one of the positive RBox premises yields a set of TBox clauses (denoted by R-Block C(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-Block R(l, n)), where n ranges over the negative RBox premises and l refers to the positive RBox premise with which P

R combines. 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 -Block H(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-Block C(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-

itive RBox premises yields the same results as in Case (I), i.e., T -Block H(j, m) (1 j k) and R-Block R(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 Purify R 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 6= ;) and 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

R with all positive TBox premises yields k2m clauses (exponential growth); combining 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-API1 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 Bio Portal2 and Oxford Ontology3 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 Bio Portal and Oxford Ontology repositories, respectively. We repeated the experiments 100 times on each ontology and averaged the results to verify the accuracy of our ﬁndings.

To ﬁt 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%

1http://owlapi.sourceforge.net/ 2http://bioportal.bioontology.org/ 3http://www.cs.ox.ac.uk/isg/ontologies/

Input Setting Results Ontology | | (%) C Time (sec.) Timeout Success R. Fixp. 7 4.890 0.0% 100.0% 0.0% 20 (10%) 3 3.260 0.0% 100.0% 0.0% 7 18.672 4.4% 94.4% 7.2% 60 (30%) 3 9.336 1.1% 98.3% 7.8% 7 70.416 13.8% 83.3% 13.3%

160 (80%) 3 29.340 5.6% 91.7% 17.2%

(354 Axioms

7 31.326 6.3% 92.6% 6.8%

80 Avg. 3 13.979 2.4% 96.7% 8.3% 7 44.392 3.0% 97.0% 0.5% 36 (10%) 3 27.745 1.5% 98.5% 0.5% 7 193.106 17.0% 79.5% 11.5% 108 (30%) 3 80.461 9.5% 88.5% 14.5% 7 412.852 34.5% 61.5% 19.0%

288 (80%) 3 166.270 17.5% 78.5% 26.5%

(875 Axioms

7 216.783 18.2% 79.3% 10.3%

144 Avg. 3 91.492 9.5% 88.5% 13.8%

Figure 6: Evaluation results for concept forgetting

of the concept symbols from the respective Bio Portal 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 Bio Portal-cases within a short period of time, with 8.3% of them using ﬁxpoints in the result. In the experiments of 10% of the concept symbols speciﬁed 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 Bio Portal ontologies and a larger set of concept symbols was speciﬁed 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 ﬁxpoints occurred in the result. The use of the heuristic boosted the overall success rate by 4% and 9.2%, and improved the time efﬁciency by 124.1% and 136.9% in the Bio Portal and Oxford ontologies, respectively.

Setting Results | | (%) R Deﬁner in Time (sec.) Success R. D. Left Clause " 7 1.1/onto. 2.120 sec. 100.0% 0 4.1% 4 (10%) 3 10 onto. 2.101 sec. 100.0% 0 4.1% 7 1.9/onto. 8.658 sec. 100.0% 0 14.5% 12 (30%) 3 13 onto. 8.314 sec. 100.0% 0 14.5% 7 3.0/onto. 20.913 sec. 100.0% 0 26.5% 20 (50%) 3 16 onto. 20.566 sec. 100.0% 0 26.5% 7 2.0/onto. 10.564 sec. 100.0% 0 15.0% Avg. 3 13 onto. 10.327 sec. 100.0% 0 15.0% 7 2.4/onto. 3.187 sec. 100.0% 0 2.2% 5 (10%) 3 25 onto. 3.072 sec. 100.0% 0 2.2% 7 3.7/onto. 18.537 sec. 100.0% 0 6.9% 15 (30%) 3 28 onto. 17.998 sec. 100.0% 0 6.9% 7 5.7/onto. 36.292 sec. 100.0% 0 14.6% 25 (50%) 3 39 onto. 34.117 sec. 100.0% 0 14.6% 7 3.9/onto. 19.339 sec. 100.0% 0 7.9% Avg. 3 30 onto. 18.396 sec. 100.0% 0 7.9%

Figure 7: Evaluation results for role forgetting

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 deﬁner symbols), as expected, was signiﬁcantly longer than forgetting the same number of concept symbols, despite the 100% success rate. Because of the nature of the Ackermann R rule, role forgetting leads to growth of clauses in the forgetting solution, which was however modest (see Clause ") compared to the theoretical worst case. Deﬁner 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 ﬂat. By m/onto, we mean there were on average m deﬁner symbols introduced in each ontology, and by n onto, we mean that n of all ontologies introduced deﬁner symbols. These deﬁner symbols were successfully eliminated in the subsequent deﬁner 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 Future Work 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 ﬁxpoints 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 ﬁnitely; see [Koopmann, 2015] for an example. The problem of extending the method to handle role functionality and numerical quantiﬁer 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.

References [Ackermann, 1935] W. Ackermann. Untersuchungen uber das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110(1):390 413, 1935. [Conradie et al., 2006] W. Conradie, V. Goranko, and D. Vakarelov.

Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in Computer Science, 2(1), 2006. [D Agostino and Hollenberg, 2000] G. D Agostino and M. Hollen-

berg. Logical questions concerning the µ-Calculus: Interpolation, Lyndon and Los-Tarski. Journal of Symbolic Logic, 65(1):310 332, 2000. [Doherty et al., 1997] P. Doherty, W. Łukaszewicz, and A. Szałas.

Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning, 18(3):297 336, 1997. [Gabbay and Ohlbach, 1992] D. M. Gabbay and H. J. Ohlbach.

Quantiﬁer elimination in second order predicate logic. In Proc. KR 92, pp. 425 435. Morgan Kaufmann, 1992. [Gabbay et al., 2008] D. M. Gabbay, R. A. Schmidt, and A. Szałas.

Second Order Quantiﬁer Elimination. College Publ., 2008. [Goranko and Vakarelov, 2006] V. Goranko and D. Vakarelov. Ele-

mentary canonical formulae: extending Sahlqvist s theorem. Annals of Pure and Applied Logic, 141(1-2):180 217, 2006. [Gr adel and Walukiewicz, 1999] E. Gr adel and I. Walukiewicz.

Guarded ﬁxed point logic. In Proc. LICS 99, pp. 45 54. IEEE Computer Society, 1999. [Herzig and Mengin, 2008] A. Herzig and J. Mengin. Uniform in-

terpolation by resolution in modal logic. In Proc. JELIA 08, vol. 5293 of LNCS, pp. 219 231. Springer, 2008. [Konev et al., 2009a] B. Konev, C. Lutz, D. Walther, and F. Wolter.

Formal properties of modularisation. In Modular Ontologies, vol. 5445 of LNCS, pp. 25 66. Springer, 2009. [Konev et al., 2009b] B. Konev, D. Walther, and F. Wolter. Forget-

ting and uniform interpolation in extensions of the description logic EL. In Proc. DL 09, vol. 477 of CEUR Workshop Proceedings. CEUR-WS.org, 2009. [Konev et al., 2013] B. Konev, C. Lutz, D. Walther, and F. Wolter.

Model-theoretic inseparability and modularity of description logic ontologies. Artiﬁcial Intelligence, 203:66 103, 2013. [Koopmann and Schmidt, 2013a] P. Koopmann and R. A. Schmidt.

Forgetting concept and role symbols in ALCH-ontologies. In Proc. LPAR 13, vol. 8312 of LNCS, pp. 552 567. Springer, 2013. [Koopmann and Schmidt, 2013b] P. Koopmann and R. A. Schmidt.

Uniform interpolation of ALC-ontologies using ﬁxpoints. In Proc. Fro Co S 13, vol. 8152 of LNCS, pp. 87-102. Springer, 2013. [Koopmann and Schmidt, 2014] P. Koopmann and R. A. Schmidt.

Count and forget: Uniform interpolation of SHQ-ontologies. In Proc. IJCAR 14, vol. 8562 of LNCS, pp. 434 448. Springer, 2014. [Koopmann and Schmidt, 2015] P. Koopmann and R. A. Schmidt.

Saturated-based forgetting in the description logic SIF. In Proc. DL 15, vol. 1350 of CEUR Workshop Proceedings. CEURWS.org, 2015. [Koopmann, 2015] P. Koopmann. Practical uniform interpolation

for expressive description logics. Ph D thesis, University of Manchester, 2015. [Lin and Reiter, 1994] F. Lin and R. Reiter. Forget it! In Proc. AAAI Fall Symposium on Relevance, pp. 154 159, 1994.

[Ludwig and Konev, 2014] M. Ludwig and B. Konev. Practical uni-

form interpolation and forgetting for ALC TBoxes with applications to logical difference. In Proc. KR 14. AAAI Press, 2014. [Lutz and Wolter, 2011] C. Lutz and F. Wolter. Foundations for uni-

form interpolation and forgetting in expressive description logics. In Proc. IJCAI 11, pp. 989 995. IJCAI/AAAI, 2011. [Lutz et al., 2012] C. Lutz, I. Seylan, and F. Wolter. An automata-

theoretic approach to uniform interpolation and approximation in the description logic EL. In Proc. KR 12, pp. 286 297. AAAI Press, 2012. [Nikitina and Rudolph, 2014] N. Nikitina and S. Rudolph. (Non-)Succinctness of Uniform Interpolants of General Terminologies in the Description Logic EL. Artiﬁcial Intelligence, 215:120 140, 2014. [Nonnengart and Szałas, 1999] A. Nonnengart and A. Szałas. A ﬁxpoint approach to second-order quantiﬁer elimination with applications to correspondence theory. In E. Orlowska, editor, Logic at Work, pp. 307 328. Springer, 1999. [Sahlqvist, 1975] H. Sahlqvist. Completeness and correspondence

in the ﬁrst and second order semantics for modal logics. In Proc. 3rd Scandinavian Logic Symposium, 1973, pp. 110 143. North Holland, 1975. [Schmidt and Tishkovsky, 2014] R. A. Schmidt and D. Tishkovsky.

Using tableau to decide description logics with full role negation and identity. ACM Transactions of Computational Logic, 15(1):7:1 7:31, 2014. [Schmidt, 2012] R. A. Schmidt. The Ackermann approach for modal logic, correspondence theory and second-order reduction. Journal of Applied Logic, 10(1):52 74, 2012. [Szałas, 1993] A. Szałas. On the correspondence between modal

and classical logic: An automated approach. Journal of Logic and Computation, 3:605 620, 1993. [Szałas, 2006] A. Szałas. Second-order reasoning in description logics. Journal of Applied Non-Classical Logics, 16(3-4):517 530, 2006. [Tishkovsky et al., 2012] D. Tishkovsky, R. A. Schmidt, and M. Khodadadi. The tableau prover generator Met Te L2. In Proc. JELIA 12, vol. 7519 of LNCS, pp. 492 495. Springer, 2012. [Visser, 1996] A. Visser. Bisimulations, Model Descriptions and

Propositional Quantiﬁers. Logic Group Preprint Series. Department of Philosophy, Utrecht Univ., 1996. [Wang et al., 2008] Z. Wang, K. Wang, R. W. Topor, and J. Z. Pan.

Forgetting concepts in DL-Lite. In Proc. ESWC 08, vol. 5021 of LNCS, pp. 245 257. Springer, 2008. [Wang et al., 2009] K. Wang, Z. Wang, R. Topor, J. Z. Pan, and

G. Antoniou. Concept and role forgetting in ALC ontologies. In Proc. ISWC 09, vol. 5823 of LNCS, pp. 666 681. Springer, 2009. [Wang et al., 2014] K. Wang, Z. Wang, R. Topor, J. Z. Pan, and

G. Antoniou. Eliminating concepts and roles from ontologies in expressive description logics. Computational Intelligence, 30(2):205 232, 2014. [Wernhard, 2011] C. Wernhard. Computing with logic as operator

elimination: The Toy Elim system. In Proc. INAP/WLP 11, vol. 7773 of LNCS, pp. 289 296. Springer, 2011. [Zhao and Schmidt, 2015] Y. Zhao and R. A. Schmidt. Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. In Proc. ISWC 15, vol. 9366 of LNCS, pp. 587 602. Springer, 2015.