Saturation-Based Forgetting in the Description Logic S I F

Abstract

Forgetting, which has also been studied under the names uniform interpolation, projection and variable elimination, deals with the elimination of symbols from an input ontology in such a way that all entailments in the remaining signature are preserved. The computed result, the uniform interpolant, can be seen as a restricted view of the original ontology, projected to a speci ed subset of the signature. Forgetting has applications in ontology reuse, ontology analysis and information hiding, and has been studied for a variety of description logics in the last years. However, forgetting in description logics with functional role restrictions and inverse roles has been an open problem so far. In this paper, we study the problem of forgetting concept symbols in the description logic SIF , an expressive description logic supporting transitive roles, inverse roles and functional role restrictions. Saturation-based reasoning has been proven to be a well-suited technique for computing uniform interpolants practically in recently introduced methods. Since existing methods are usually optimised towards a speci c aim such as satis ability checking or classi cation, they cannot always directly be used for forgetting. In this paper we present a new saturation technique that is complete for forgetting concept symbols, and show how it can be used for computing uniform interpolants.

-

We present a method for forgetting concept symbols from SIF -ontologies. Modern applications, especially in bio-informatics or medical domains, lead to the development of ontologies that cover a large vocabulary. With rising complexity, these ontologies become harder to maintain and modify. It can therefore be advantageous to have tool-support for reducing the vocabulary used in an ontology. Forgetting restricts the vocabulary in an ontology in such a way that all entailments over the restricted vocabulary are preserved. In contrast to modules, uniform interpolants are completely in the desired signature and may contain di erent axioms than the input ontology.

There are numerous applications of forgetting that make the problem worth studying, of which we give a few examples. Ontology Summary. Comprehending a complex ontology can be hindered by a too large vocabulary used in the ontology. If the central concepts and roles of the ontology are known, forgetting all but the central concepts of an ontology can be used to compute a more focused high-level summary of the ontology. Ontology Analysis. With increasing complexity of the ontology, understanding the relations between concepts and roles involved becomes more di cult. By forgetting all but a few chosen symbols, one can obtain a direct representation of the interactions between them. Logical Di erence. In order to maintain an evolving ontology, it is necessary to be able to exhibit changes between di erent ontology versions. However, a syntactical di between text representations of the ontologies is rarely useful in practice. In contrast, the logical di erence between two ontologies is a semantic notion, which is de ned by the di erence of logical entailments in the common signature of these ontologies, or in a speci ed signature [ 8,7 ]. [ 16 ] show that the logical di erence can easily be computed using the uniform interpolants of the ontologies. Information Hiding. As pointed out in [ 4 ], ontology-based systems are increasingly used in a range of applications that deal with sensitive information. Forgetting can be used as a means to eliminate con dential information if an ontology is to be shared between users with di ering privileges.

Methods for forgetting have been investigated for a range of description logics, including DL-Lite [ 29 ], E L [ 9,17,20 ], ALC [ 28,16,12,11,14,15 ], ALCH [ 10 ] and SHQ [ 13 ]. So far, forgetting for description logics with inverse roles and functional role restrictions was an open problem.

As with most expressive description logics, SIF does not have uniform interpolation. This means that the result of forgetting may not always be nitely representable in SIF . Take as an example the ontology O = fA v 9r:B, B v 9r:Bg. If we only use the expressivity SIF provides, forgetting B from O would result in an in nite ontology of the form fA v 9r:9r:9r: : : :g. A solution to this problem is to use xpoint operators in the resulting ontology [ 19,12 ]. Fixpoints are not a common formalism for description logics, but can be simulated in classical description logics using additional concept symbols, and can serve as a basis for approximating of the result of forgetting [ 12 ].

As is shown in [ 18,20 ], if nite and if xpoints are not used in the result, already for the description logics E L and ALC, the result of forgetting can be of size triple exponential in the size of the input. By using xpoint operators, we obtain a double-exponential upper-bound, which also holds for the description logic SIF . Since this is still of high complexity, a goal-oriented approach is required in order to be able to compute uniform interpolants practically. Practicality has been achieved in [ 10,13,14,16 ] by using a saturation-based approach, which eliminates concept symbols by resolving on these symbols. This approach is also followed in this paper. Saturation-based reasoning has recently received increased interest in the description logic community, due to the success of consequencebased reasoning methods for classi cation [ 6,22,24,25,26 ]. However, these methods are optimised for speci c reasoning tasks, and can not directly be used for forgetting.

In this paper, we present a new sound and refutationally complete saturationprocedure for SIF , and show that it can be used for forgetting concept symbols in a goal-oriented manner. The method is based on the methods presented in [ 12,10 ], which we extend to incorporate transitive roles, inverse roles and functional role restrictions. 2

De nition of S I F

and Forgetting We de ne the description logic SIF , which is SIF extended with xpoint operators.

Let Nc, Nr, Ni and Nv be four pair-wise disjoint sets of respectively concept symbols, role symbols, individuals and concept variables. A role is either of the form r or r , where r 2 Nr. We de ne the inverse of a role Inv(R) as Inv(r) = r and Inv(r ) = r. An RBox R is a set of transitivity axioms trans(R), where R is a role. A role R is transitive in R if trans(R) 2 R or trans(Inv(R)) 2 R.

SIF -concepts have the following form: ? j A j X j :C j C1 t C2 j 9R:C j 1R:> j

X:C[X]; where A 2 Nc, X 2 Nv, C, C1 and C2 are arbitrary concepts and R is any role, and C[X] is a concept expression in which X occurs under an even number of negations. We de ne further concept expressions as abbreviations: > = :?, C1 u C2 = :(:C1 t :C2), 8R:C = :(9R::C), 2R:> = : 1R:>. Concepts of the form 1R:> are called functional role restrictions. Concepts of the form X:C[X] are called greatest xpoint expressions. X:C[X] denotes the greatest xpoint of C[X], and is the greatest xpoint operator. A concept variable X is bound if it occurs in the scope C[X] of a xpoint expression X:C[X]. Otherwise it is free. A concept is closed if it does not contain any free variables, otherwise it is open.

A TBox T is a set of concept axioms of the forms C v D (concept inclusion) and C D (concept equivalence), where C and D are closed concepts. C D is short-hand for the two concept axioms C v D and D v C. We further require greatest xpoint expressions to occur only positively in an axiom, that is, on the right-hand side of a concept inclusion and only under an even number of negations. An ontology O = hT ; Ri consists of a TBox T and an RBox R with the additional restriction that roles that are transitive in R do not occur under functional role restrictions. This is a common restriction that has been used to guarantee decidability of common reasoning tasks for description logics with number restrictions [ 5 ] , and our forgetting method assumes that it is satis ed.

In the de nition of the semantics of SIF , an interpretation I is a pair h I ; I i of the domain I , a nonempty set, and the interpretation function I , which assigns to each concept symbol A 2 Nc a subset of I and to each role symbol r 2 Nr a subset of I I . The interpretation function is extended to SIF -concepts as follows.

?I = ; ( (:C)I =

I n CI

(C t D)I = CI [ DI nr:C)I = fx 2

I j #f(x; y) 2 rI j y 2 CI g ng The semantics of xpoint expressions is de ned following [ 2 ]. Whereas concept symbols are assigned xed subsets of the domain, concept variables range over arbitrary subsets, which is why only closed concepts have a xed interpretation. Open concepts are interpreted using valuations that map concept variables to subsets of I . Given a valuation and a set W I , [X 7! W ] denotes a valuation identical to except that [X 7! W ](X) = W . Given an interpretation I and a valuation , the function I is I extended with the cases XI = (X) and ( X:C)I = [fW

I j W

CI[X7!W ]g: If C is closed, we de ne CI = CI for any valuation . Since C does not contain any free variables in this case, this de nes CI uniquely.

A concept inclusion C v D is true in an interpretation I i CI DI and a transitivity axiom trans(R) is true in I if for any domain elements x; y; z 2 I we have (x; z) 2 RI if (x; y) 2 RI and (y; z) 2 RI . I is a model of an ontology O if all axioms in O are true in I. An ontology O is satis able if a model exists for O, otherwise it is unsatis able. Two TBoxes T1 and T2 are equi-satis able if every model of T1 can be extended to a model of T2, and vice versa. T j= C v D holds i in every model I of T we have CI DI . If an axiom is true in all models of O, we write O j= .

Let sig(E) denote the concept and role symbols occurring in E, where E can denote a concept, an axiom, a TBox, an RBox or an ontology.

De nition 1 (Forgetting). Let A be a concept symbol and O and O A be ontologies. An ontology O A is a result of forgetting A from O if the following conditions hold: 1. A 62 sig(O A), and 2. for all concept inclusions with A 62 sig( ): O

A j= i

O j= .

Given an ontology O and a set of concept symbols S, a result of forgetting S from O is a result of forgetting each symbol in S one by one. An ontology OS is a uniform interpolant of O for S i O is a result of forgetting every symbol from O that is not in S. 3

Normalisation

The saturation method works on ontologies of a speci c normal form, which is de ned as follows.

De nition 2. Let Nd Nc be a set of designated concept symbols called de ner symbols or, simply, de ners. A SIF literal is a concept of one of the following forms:

A j :A j 9R:D j 8R:D j 2R:> j 1R:>; where A 2 Nc, D 2 Nd, and R is of the form r or r , with r 2 Nr. A SIF clause is a transitivity axiom or an axiom of the form > v L1 t : : : t Ln, where L1; : : : ; Ln are SIF literals. We may omit the leading \> v" in clauses, and Non-Cyclic De ner Elimination:

O [ fD v Cg

O[D=C] De ner Puri cation:

O

O[D=>] Cyclic De ner Elimination: provided D 62 sig(C) provided D occurs only positively in O O [ fD v C[D]g

O[D= X:C[X]]

provided D 2 sig(C[D]) assume clauses are represented as sets, that is, they do not contain duplicate elements and the order is not important.

An ontology N is in SIF normal form if every axiom in N is a SIF clause, and if for every clause trans(R) 2 N , there is also a clause trans(Inv(R)) 2 N .

Note that the description logic SIF allows for number restrictions of the form 2R:>, since SIF concepts are closed under negation, and 2R:> :( 1R:>).

Any SIF ontology can be transformed into an ontology in SIF normal form using standard structural transformation and CNF transformation techniques. Example 1. Consider the following ontology O1:

A1 u B1 v ?

A1 v 9r :B2

B2 v 1r:>

B2 v 9r:(B1 t A2) The SIF normal form of O1 is the following set of clauses: 1: :A1 t :B1 2: :A1 t 9r :D1 3: :D1 t B2 4: :B2 t

1r:> 5: :B2 t 9r:D2 6: :D2 t B1 t A2

Given a set N of SIF clauses such that every clause contains at most one literal of the form :D, where D 2 Nd, it is possible to eliminate all de ner literals in N using the rewrite rules shown in Figure 1. This is crucial for our method for forgetting concept symbols, since the method described in the next section operates on sets of SIF clauses. For the rules in Figure 1, it is assumed that for every de ner D occurring negatively in N , the set of clauses of the form :D tC1, : : :, :D t Cn is replaced by a single axiom D v C1 u : : : u Cn. Note that the last rule in Figure 1 introduces xpoint operators to the ontology. The rules in Figure 1 are applications of Ackermann's Lemma [ 1 ] and its generalisation [ 21 ], which have been used in the context of second-order quanti er elimination to eliminate predicate symbols [ 3 ]. The result of applying these rules does not contain any de ners, but preserves all entailments of input that do not involve de ner symbols, which is a consequence of these lemmata.

Transitivity Rule: Universalisation Rule:

C t 8R:D C t 8R:Dtrans :D0 t D trans(R)

:D0 t 8R:Dtrans C1 t 9R:D C2 t

C1 t C2 t 8R:D

1R:> In order to forget a concept symbol A, we infer all inferences on that symbol using a saturation-based approach, and then eliminate occurrences of that symbol from the resulting clause set. Using the transformation rules in Figure 1, we can then eliminate all de ner symbols introduced by the normalisation or throughout the reasoning process.

Due to possible interactions between the rules of our calculus, we process the clause set in several stages, where only certain rules are allowed in each stage. This is a major di erence between this method and the methods for ALC and ALCH presented in [ 12,10 ], and is necessary to guarantee termination of the method. In the rst stage, we only apply rules that infer clauses with universal restrictions. The function of this stage is to infer all clauses that can serve as premise in the second stage of the calculus. In the second stage, we handle inverse roles in universal restrictions using the role inversion rule. In the last stage, we apply all remaining inferences of the calculus with the aim of computing inferences on A. We describe the stages one by one, and illustrate them on the example introduced in the last section.

Stage 1. The rules for the rst stage are shown in Figure 2. The transitivity rule is directly taken from [ 13 ], which presents a similar calculus for the description logic SHQ. The rule works in a similar fashion as common rewriting rules to reduce reasoning with transitivity roles to reasoning without (see for example [ 27,23 ]).

The universalisation rule infers from a functional role restriction and an existential role restriction a universal restriction. The soundness of this rule can be explained as follows. If a domain element x in a model I has an Rsuccessor that satis es D (x 2 (9R:D)I ), and if x has maximally one R-successor (x 2 ( 1R:>)I ), then every R-successor of x satis es D, since there is only one such successor (x 2 (8R:D)I ). This means (9R:Du 1R:>) j= 8R:D, and implies that the universalisation rule is sound.

Role Inversion Rule: Resolution Rule:

C1 t 8R:D1 C2 t QR:D2

C1 t C2 t QR:D12 where Q 2 f8; 9g and D12 is a possibly new de ner representing D1 u D2.

C1 t 9R:D1 C2 t 9R:D2

C1 t C2 t 9R:D12 t 2R:> where D12 is a possibly new de ner representing D1 u D2.

C t 8R:D D t 8Inv(R):DInv :DInv t C

Example 2. Following the clause set constructed in the last example, in Stage 1, we apply the universalisation rule on Clause 4 and 5 to infer the following clause. 7: :B2 t 8r:D2

(Universalisation 4, 5)

Stage 2. In this stage, the inversion rule shown in Figure 3 is applied. Example 3. Continuing the previous example, there is only one clause in the current clause set that has a universal role restriction, which is Clause 7 that was derived in Stage 1. By applying the role inversion rule, the following new clauses are derived: 8: D2 t 8r :DInv 9: :DInv t :B2 (Role Inversion 7) (Role Inversion 7)

Stage 3. This is the main reasoning stage, where we compute all inferences on the symbols we want to forget. The rules for this stage are shown in Figure 4. The rules of this stage are an extension of the calculus used for forgetting presented in [ 12,10 ]. The 9-rule is in uenced by the calculus for reasoning in SHQ presented in [ 13 ].

A key for ensuring termination is the dynamic introduction of new symbols through the rules of the calculus. This is necessary to preserve the normal form and still be able to infer all clauses that are required for the forgetting result. There are two rules in the rst stage that introduce new de ners: the transitivity rule and the role inversion rule. In the third stage, the 8-rule and the 9-rule may introduce new de ners that represent conjunctions of existing de ners. More speci cally, given two de ners D1 and D2, we may introduce a new de ner D12 representing D1 u D2 by adding the clauses :D12 t D1 and :D12 t D2. By doing this in an optimised way, the number of de ner symbols introduced can be restricted to by 2n, where n is the number of de ner symbols present in the input clause set [ 12 ].

The resolution rule is standard in resolution-based reasoning. The 8-rule are directly taken from [ 12 ]. The 8-rule propagates concepts below a universal role restrictions into other role restrictions. If 8R:D1 is satis ed by some element x of the domain, we know that all R-successors of x have to satisfy D1. This implies that, if x furthermore satis es QR:D2 for some Q 2 f9; 8g, then it also satis es QR:(D1 u D2).

The 9-rule is new and necessary in order to preserve entailments that use a 2-restriction. Assume we have a model with a domain element x that has at least one R-successor x1 satisfying D1 and at least one R-successor x2 that satis es D2. If x1 = x2, then x satis es 9R:(D1 u D2). If x1 6= x2, then x satis es 2R:>. Hence, we have (C1 t 9R:D1) u (C2 t 9R:D2) j= (C1 t C2 t 9R:(D1 u D2) t 2R:>), and the 9-rule is sound.

In order to forget a concept symbol A, we compute all resolvents on A and on de ner literals that lead to clauses with maximally one negative de ner literal. Clauses with multiple negative de ner literals are not needed for the computation, which can be argued in similar ways as in [ 12 ].

Note that even though only the resolution rule directly infers clauses on a concept symbol, the 8- and the 9-rule may introduce new de ners, which subsequently makes new inferences on the symbol to be forgotten possible. For the forgetting result, only inferences with maximally one negative de ner literal are required. The role inversion rule may derive clauses with more than one negative de ner literal, but these inferences are only required if they allow for further inferences of clauses with maximally one negative de ner.

In the resulting clause set, we omit all clauses containing A or more than one negative de ner literal. Then, we eliminate all de ners using the technique described in the last section. The ontology obtained is the result of forgetting A from the original ontology.

Example 4. Assume we want to forget B1 and B2. We begin by computing inferences on B1, for which only one inference step is needed.

10: :D2 t :A1 t A2 (Resolution 1, 6) We continue by computing inferences on B2. This time, in order to make all inferences possible, we have to use the 8-rule rst.

11: :D1 t

1r:> 12: :D1 t 9r:D2 13: :D1 t 8r:D2 14: :A1 t D2 t 9r :D1Inv 15: :D1Inv t D1 16: :D1Inv t DInv 17: :A1 t A2 t 9r :D1Inv 18: :D1Inv t B2 19: :D1Inv t :B2 20: :D1Inv (Resolution 3, 4) (Resolution 3, 5) (Resolution 3, 7)

(8-rule 2, 8) (D1Inv v D1 u DInv) (D1Inv v D1 u DInv) (Resolution 10, 14) (Resolution 3, 15) (Resolution 9, 16) (Resolution 18, 19) Even though we did not discuss redundancy elimination techniques here, one can easily see that further inferences of clauses of the form :D1Inv t C are not needed, since we already inferred the unary clause :D1Inv. For the same reason, we do not have to include any other clause containing :D1Inv in the result. In fact, no further inferences are necessary for the forgetting result. If we ignore all clauses that do contain the symbols B1 and B2 we are forgetting, we are left with Clauses 2, 7, 10{13, 17 and 20. Eliminating the de ners in these clauses results in the following ontology:

A1 v 9r :( 1r:> u 9r:(:A1 t A2) u 8r:(:A1 t A2))

A1 v A2 t 9r :? We can simplify the second axiom to A1 v A2, which allows us to further simplify the rst axiom, and obtain as result of forgetting B1 and B2 the following: A1 v 9r :( 1r:> u 9r:>) A1 v A2 5

Correctness of the Method

In order to prove that the method is correct, we show that the resulting ontology preserves all entailments of axioms that do not use the symbols to be forgotten. More formally, if O A denotes the output of our method for an ontology O and a concept symbol A, we show that O A j= i O j= for all axioms with A 62 sig( ). If = C1 v C2, we can prove O j= by showing that O [ f9r :(C1 u :C2)g is unsatis able, where r is a role not occurring in O.

In order to show that our forgetting method works correctly, we extend our reasoning method to a refutational complete calculus, that, in order to prove the satis ability of a clause set, rst infers inferences on a designated concept symbol A using only the rules of the forgetting method. If this calculus is refutational complete, we have that a contradiction can be derived from O [f9r :(C1 u:C2)g 9-Elimination Rule: 2-Elimination Rule I: 2-Elimination Rule II:

C1 t 9R:D

C1

:D C1 t 2R:> C2 t

C1 t C2

1R:> C1 t 2R:>

C2 t 8R:D C1 t C2 :D exactly in the same cases as it can from O A [ f9r :(C1 u :C2)g. This implies O A j= C1 v C2 i O j= C1 v C2 for all concept inclusions C1 v C2 with A 62 sig(C1 v C2), as required.

In order to obtain a refutationally complete calculus, we additionally need the rules shown in Figure 5. Whereas the rules for the forgetting procedure are aimed at making inferences on concept symbols possible, they are not su cient for detecting whether a set of clauses is unsatis able. The rules in Figure 5 are aimed at detecting inconsistencies between clauses and eliminating unsatis able literals, and transform the set of rules into a decision procedure for SIF -ontology satis ability.

The 9-elimination rule eliminates unsatis able literals of the form 9R:D. The 2-elimination rule I resolves on literals of the form 2R:> and 1R:>. The rule is sound since an individual can only satisfy 2R:> or 1R:> at the same time. The 2-elimination rule II eliminates unsatis able literals, similarly to the 9-elimination rule. If the de ner D is unsatis able, any instance of 8R:D cannot have R-successors. Therefore, we can resolve between 8R:D and 2R:>.

We obtain the reasoning procedure RefSIF by extending the forgetting procedure presented in the last section by the rules in Figure 5, which are applied in the last reasoning stage. We further re ne the calculus with an ordering. The reasoning procedure RefSAIF uses the same rules as RefSIF , but for clauses containing the concept symbol A, it only performs inferences on literals of the form A or :A.

We have the following theorem.

Theorem 1. Let A be any concept symbol, RefSIF and RefSAIF are sound and refutationally complete, that is, for any set N of clauses, one can infer the empty clause i N is inconsistent.

Proof (Sketch). In order to prove refutational completeness, we have to show that we can build a model based on any saturated set N of clauses such that ? 62 N . Such a model can be obtained by adapting the model construction presented in [ 10 ]. This construction rst constructs a model fragment for each de ner, and then connects these elements to a complete model, where each de ner is represented by a designated domain element. Di erent to ALCH, SIF does not have the nite model property. By unravelling the possibly cyclic models created in [ 10 ] to a possibly in nite tree, it is however possible to construct a model for N , which can be veri ed by a careful analysis of the cases used in the proof in [ 10 ]. tu

This theorem allows us to establish that the forgetting procedure described in the last section is correct.

Theorem 2. For any SIF -ontology O and any concept symbol A, the described method always terminates and computes the result of forgetting A from O. A uniform interpolant for any ontology O and signature S with Nr S can be computed by step-wise forgetting every symbol in sig(O) n S. 6

Conclusion and Future Work

We described a method for forgetting concept symbols from ontologies formulated in the description logic SIF , where results are represented in SIF . Forgetting eliminates a speci ed set of symbols from an ontology in such a way, that all entailments that do not use these symbols are preserved. The method uses a resolution-based saturation procedure to compute inferences on the symbols to be eliminated. By extending this saturation procedure to a refutationally complete reasoning method, which performs inferences on the symbols to be forgotten rst, we could prove that our method indeed preserves all entailments in the desired signature.

In order to properly handle the interactions between functional role restrictions and inverse roles without losing termination, the method works in three stages. In the rst stage all clauses with a universal restriction are computed, on which in the second stage inferences based on inverse roles are performed. An interesting question is whether this approach can also be used in connection with role hierarchies or with cardinality restrictions. A method for forgetting in the description logic SHQ is presented in [ 13 ]. A simple combination of the rules presented in this paper and presented in [ 13 ] is not su cient to obtain a refutational complete method already for SHIF . An open question is whether this also a ects the appropriateness of such a calculus for forgetting concept symbols, and whether a su cient calculus can be developed by adding additional rules and possibly further extending the underlying description logic, for example with role conjunctions.

We are working on a prototypical implementation of the method, which we aim to integrate into our forgetting tool Lethe.1 Experiments on similar methods for ALC, ALCH and SHQ had promising results [ 11,10,13,15 ], and we are con dent that similar results can be obtained for SIF . 1 www.cs.man.ac.uk/~koopmanp/lethe

References

1. Ackermann , W.: Untersuchungen uber das Eliminationsproblem der mathematischen Logik . Mathematische Annalen 110 ( 1 ), 390 { 413 ( 1935 )

2. Calvanese , D. , De Giacomo , G. , Lenzerini , M.: Reasoning in expressive description logics with xpoints based on automata on in nite trees . In: Proceedings of the Sixteenth International Joint Conference on Arti cial Intelligence, IJCAI 99 . pp. 84 { 89 . Morgan Kaufmann ( 1999 )

3. Gabbay , D.M. , Schmidt , R.A. , Szalas , A. : Second Order Quanti er Elimination: Foundations, Computational Aspects and Applications , Studies in Logic, vol. 12 . College Publications ( 2008 )

4. Grau , B.C. : Privacy in ontology-based information systems: A pending matter . Semantic Web 1 ( 1-2 ), 137 { 141 ( 2010 )

5. Horrocks , I. , Sattler , U. , Tobies , S. : Practical reasoning for very expressive description logics . Logic Journal of the IGPL 8 ( 3 ), 239 | 263 ( 2000 )

6. Kazakov , Y. : Consequence-Driven Reasoning for Horn SHIQ Ontologies . In: Boutilier, C . (ed.) Proceedings of the International Joint Conference on Arti cial Intelligence (IJCAI-09) . pp. 2040 { 2045 . AAAI Press ( 2009 )

7. Konev , B. , Ludwig , M. , Walther , D. , Wolter , F. : The logical di erence for the lightweight description logic EL . Journal of Arti cial Intelligence Research 44 ( 1 ), 633 { 708 ( 2012 )

8. Konev , B. , Walther , D. , Wolter , F. : The logical di erence problem for description logic terminologies . In: Automated Reasoning, Lecture Notes of Computer Science , vol. 5195 , pp. 259 { 274 . Springer ( 2008 )

9. Konev , B. , Walther , D. , Wolter , F. : Forgetting and uniform interpolation in largescale description logic terminologies . In: Proceedings of the Internation Conference on Arti cial Intelligence (IJCAI-09) . pp. 830 { 835 . AAAI Press ( 2009 )

10. Koopmann , P. , Schmidt , R.A. : Forgetting concept and role symbols in ALCHontologies . In: Logic for Programming, Arti cial Intelligence and Reasoning. Lecture Notes in Computer Science , vol. 8312 , pp. 552 { 567 . Springer ( 2013 )

11. Koopmann , P. , Schmidt , R.A. : Implementation and evaluation of forgetting in ALC-ontologies . In: Proceedings of the 7th International Workshop on Modular Ontologies (WoMO'13) . CEUR Workshop Proceedings , vol. 1081 , pp. 37 { 48 . CEUR-WS.org ( 2013 )

12. Koopmann , P. , Schmidt , R.A. : Uniform interpolation of ALC-ontologies using xpoints . In: Frontiers of Combining Systems. Lecture Notes in Computer Science , vol. 8152 , pp. 87 { 102 . Springer ( 2013 )

13. Koopmann , P. , Schmidt , R.A. : Count and forget: Uniform interpolation of SHQontologies . In: Automated Reasoning. Lecture Notes in Computer Science , vol. 8562 , pp. 434 { 448 . Springer ( 2014 )

14. Koopmann , P. , Schmidt , R.A. : Forgetting and uniform interpolation for ALContologies with ABoxes . In: Proceedings of the 27th International Workshop of Description Logics (DL 2014 ). CEUR Workshop Proceedings , vol. 1193 , pp. 245 { 257 . CEUR-WS.org ( 2014 )

15. Koopmann , P. , Schmidt , R.A. : Uniform interpolation and forgetting for ALC ontologies with ABoxes . In: Proceedings of the Twenty-Ninth AAAI Conference on Arti cial Intelligence (AAAI-15) . vol. 1 , pp. 175 { 181 . AAAI-Press ( 2015 )

16. Ludwig , M. , Konev , B. : Practical uniform interpolation and forgetting for ALC TBoxes with applications to logical di erence . In: Proc. KR'14 . AAAI Press ( 2014 )

17. Lutz , C. , Seylan , I. , Wolter , F. : An automata-theoretic approach to uniform interpolation and approximation in the description logic EL . In: Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference (KR-12) . pp. 286 { 296 . AAAI Press ( 2012 )

18. Lutz , C. , Wolter , F. : Foundations for uniform interpolation and forgetting in expressive description logics . In: Proceedings of the International Joint Conference on Arti cial Intelligence (IJCAI-11) . pp. 989 { 995 . AAAI Press ( 2011 )

19. Nikitina , N.: Forgetting in general EL terminologies . In: Proceedings of the 2011 International Workhop on Description Logics (DL2011) . CEUR Workshop Proceedings , vol. 745 , pp. 345 { 355 . CEUR-WS.org ( 2011 )

20. Nikitina , N. , Rudolph , S. : (Non-) Succinctness of uniform interpolants of general terminologies in the description logic EL . Arti cial Intelligence 215 , 120 { 140 ( 2014 )

21. Nonnengart , A. , Szalas , A. : A xpoint approach to second-order quanti er elimination with applications to correspondence theory . In: Orlowska, E . (ed.) Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, Studies in Fuzziness and Soft Computing , vol. 24 , pp. 307 { 328 . Springer ( 1999 )

22. Ortiz , M. , Rudolph , S. , Simkus , M. : Worst-case optimal reasoning for the HornDL fragments of OWL 1 and 2 . In: Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference (KR-10) ( 2010 )

23. Schmidt , R.A. , Hustadt , U. : A principle for incorporating axioms into the rstorder translation of modal formulae . In: Automated Deduction{CADE-19 , pp. 412 { 426 . Springer ( 2003 )

24. Simanc k , F., Kazakov , Y. , Horrocks , I. : Consequence-based reasoning beyond Horn ontologies . In: Proceedings of the Twenty-Second International Joint Conference on Arti cial Intelligence (IJCAI-11) . vol. 22 , pp. 1093 { 1098 . AAAI Press ( 2011 )

25. Simanc k , F., Motik , B. , Krotzsch, M.: Fixed parameter tractable reasoning in DLs via decomposition . In: Proceedings of the 24th International Workshop on Description Logics (DL 2011 ). CEUR Workshop Proceedings , vol. 745 , pp. 400 { 410 . CEUR-WS.org ( 2011 )

26. Steigmiller , A. , Glimm , B. , Liebig , T. : Coupling tableau algorithms for expressive description logics with completion-based saturation procedures . In: Automated Reasoning, Lecture Notes of Computer Science , vol. 8562 , pp. 449 { 463 . Springer ( 2014 )

27. Tobies , S. : Complexity results and practical algorithms for logics in knowledge representation . Ph.D. thesis , LuFG Theoretical Computer Science, RWTH-Aachen, Germany ( 2001 )

28. Wang , K. , Wang , Z. , Topor , R.W. , Pan , J.Z. , Antoniou , G.: Eliminating concepts and roles from ontologies in expressive descriptive logics . Computational Intelligence 30 ( 2 ), 205 { 232 ( 2014 )

29. Wang , Z. , Wang , K. , Topor , R.W. , Pan , J.Z. : Forgetting for knowledge bases in DL-Lite . Annals of Mathematics and Arti cial Intelligence 58 ( 1 {2), 117 { 151 ( 2010 )