Uniform Interpolation in General EL Terminologies Nadeschda Nikitina Karlsruhe Institute of Technology, Karlsruhe, Germany nikitina@kit.edu Abstract. Recently, different forgetting approaches for knowledge bases expressed in different logics were proposed. For EL terminologies containing each atomic concept at most once on the left-hand side, an approach has been proposed based on sufficient, but not necessary acyclicity conditions. In this paper, we propose an approach for computing a uniform interpolant for general EL terminologies. We first show that a uniform interpolant of any EL terminology w.r.t. any sig- nature always exists in EL enriched with least and greatest fixpoint constructors and show how it can be computed by reducing the problem to the computation of Most General Subconcepts and Most Specific Superconcepts for atomic concepts. Then, we give the exact conditions for the existence of a uniform interpolant in EL and show how it can be obtained using our algorithms. 1 Introduction The importance of non-standard reasoning services supporting knowledge engineers in modelling a particular domain or in understanding existing models by visualizing im- plicit dependencies between concepts and roles was pointed out by the research commu- nity [3], [5]. An example of such reasoning services supporting knowledge engineers in different activities is the uniform interpolation. In particular for the understanding and the development of complex knowledge bases, e.g., those consisting of general concept inclusions (GCIs), the appropriate tool support would be beneficial. However, the exist- ing approach [7] to uniform interpolation in EL is restricted to terminologies containing each atomic concept at most once on the left-hand side of concept inclusions and ad- ditionally satisfying sufficient, but not necessary acyclicity conditions. Lutz et al.[10] propose an approach to uniform interpolation in expressive description logics such as ALC w.r.t. general terminologies by encoding ALC TBoxes as concepts, which, how- ever does not solve the problem of uniform interpolation in EL. Clearly, the existence of the results for such reasoning problems is closely related to the notion of fixpoint semantics. For instance, Baader [2] shows that the structurally similar problems of computing Least Common Subsumer and Most Specific Concept can always be solved in cyclic classical TBoxes w.r.t. to greatest fixpoint semantics. Similar results were obtained for general EL TBoxes with descriptive semantics[9] , however extended with the greatest fixpoint constructor (ELν ). In this paper, we extend the above results by showing that uniform interpolants preserving all EL consequences of general EL terminologies w.r.t. an arbitrary signature can always be expressed in an extension of EL with least fixpoint and greatest fixpoint constructors µ, ν as well as the disjunction used only on the left-hand side of concept inclusions. We extend the previ- ous approach [7] and propose the algorithms for computing such uniform interpolants for general EL terminologies based on the notion of most general subconcepts and most specific superconcepts. In the usual application scenarios it is rather useful to obtain uniform interpolants expressed in the DL of the original terminology instead of introducing additional lan- guage constructs. Therefore, in addition to the above algorithms, we derive the existence criteria for uniform interpolants in EL (i.e., expressed without the above extension) and show how such a uniform interpolant can be obtained using our algorithms. Full proofs are available in the extended version of this paper [11]. 2 Preliminaries Let NC and NR be countably infinite and mutually disjoint sets of concept symbols and role symbols. An EL concept C is defined as C ::= A|>|C u C|∃r.C where A and r range over NC and NR , respectively. In the following, we use symbols A, B to denote atomic concepts and C, D to denote arbitrary concepts. A terminology or TBox consists of concept inclusion axioms C v D and concept equivalence axioms C ≡ D used as a shorthand for C v D and D v C. While knowledge bases in general can also include a specification of individuals with the corresponding concept and role assertions (ABox), in this paper we abstract from ABoxes and concentrate on TBoxes. The signature of an EL concept C or an axiom α, denoted by sig(C) or sig(α), respec- tively, is the set of concepts and role symbols occurring in it. The signature of a TBox T , in symbols sig(T ), is analogously NC ∪ NR . In what follows, we denote the set NC ∪ {>} as NC+ . Before introducing the fixpoint operators, we recall the semantics of the above in- troduced DL constructs, which is defined by the means of interpretations. An interpre- tation I is given by the domain ∆I and a function ·I assigning each concept A ∈ NC a subset AI of ∆I and each role r ∈ NR a subset rI of ∆I × ∆I . The interpretation of > is fixed to ∆I . The interpretation of an arbitrary EL concept is defined inductively, i.e., (C u D)I = C I ∩ DI and (∃r.C)I = {x | (x, y) ∈ rI , y ∈ C I }. An interpretation I satisfies an axiom C v D if C I ⊆ DI . I is a model of a TBox, if it satisfies all of its axioms. We say that a TBox T entails an axiom α, if α is satisfied by all models of T . In combination with fixpoint constructors, we will additionally use concept disjunction C t D, the semantics of which is defined by (C t D)I = C I ∪ DI . We now introduce the logics ELµ(t),ν , a fragment of monadic second order log- ics that we use to compute uniform interpolants of general EL TBoxes. ELµ(t),ν is an extension of EL by the two fixpoint constructors, νX.Cν [9] and µX.Cµ [4]. X is an ele- ment of the countably infinite set of concept variables NV and Cν , Cµ are constructed as follows: Cν ::= X|A|>|νX.Cν |Cν u Cν |∃r.Cν Cµ ::= X|A|>|µX.Cµ |Cµ t Cµ |Cµ u Cµ |∃r.Cµ where A ranges over atomic concepts and X ranges over NV . All ELν concepts and all ELµ(t) concepts are closed Cν and Cµ expression, i.e., all concept variables are bound by the corresponding fixpoint constructor. Note that we define ELν concepts and all ELµ(t) concepts in such a way, that no concept can contain both fixpoint constructors, i.e., we do not combine the two constructors within concepts. The semantics of the fixpoint constructors is defined using a mapping ϑ of concept variables to subsets of ∆I . For an ELµ(t),ν concept C and W ⊆ ∆I , we denote a replacement of X by W as C I,ϑ[X→W] . The semantics of ELµ(t),ν concepts is defined by [ (νX.C)I,ϑ = {W ⊆ ∆I |W ⊆ C I,ϑ[X→W] } \ (µX.C)I,ϑ = {W ⊆ ∆I |C I,ϑ[X→W] ⊆ W}. In order to allow for more succinct concept expressions, we use an extended ver- sion of the fixpoint constructs allowing for mutual recursion [12], [9]. The extended constructors have the form νi X1 ...Xn .Cν,1 , ..., Cν,n and µi X1 ...Xn .Cµ,1 , ..., Cµ,n with 1 ≤ i ≤ n. The semantics is defined as follows: (νi X1 ...Xn .C1 , ..., Cn )I,ϑ = {Wi } and S (µi X1 ...Xn .C1 , ..., Cn )I,ϑ = {Wi } such that there are W1 , ..., Wi−1 , Wi+1 , ..., Wn with re- T 1 →W1 ,...,Xn →Wn ] 1 →W1 ,...,Xn →Wn ] spectively W j ⊆ C I,ϑ[X j and C I,ϑ[X j ⊆ W j for 1 ≤ j ≤ n. 3 TBox Inseparability and Uniform Interpolation Intuitively, two TBoxes T1 and T2 are inseparable w.r.t. a signature Σ if they have the same Σ consequences, i.e., consequences whose signature is a subset of Σ. Depending on the particular application requirements, the expressivity of those Σ consequences can vary from subsumption queries and instance queries to conjunctive queries. In this paper, we investigate forgetting based on concept inseparability of general EL termi- nologies defined analogously to previous work on inseparability, e.g., [8] or [7], as follows: Definition 1. Let T1 and T2 be two general EL TBoxes and Σ a signature. T1 and T2 are concept-inseparable w.r.t. Σ, in symbols T1 ≡cΣ T2 , if for all EL concepts C, D with sig(C) ∪ sig(D) ⊆ Σ holds T1 |= C v D, iff T2 |= C v D. Given a signature Σ and a TBox T , the aim of uniform interpolation or forgetting is to determine a TBox T 0 with sig(T 0 ) ⊆ Σ such that T ≡cΣ T 0 . T 0 is also called a Uniform Interpolant (UI) of T w.r.t. Σ. We call Σ = sig(T ) \ Σ the forgotten signature. In practise, the uniform interpolants are required to be finite. Therefore, in this paper, we investigate the existence of such uniform interpolants in EL, i.e., uniform interpolants expressible by a finite set of finite axioms using only the language constructs of EL. As demonstrated by the following example, in the presence of cyclic concept inclusions, a finite UI in EL might not exist for a particular T and a particular Σ. Example 1. Forgetting the concept A in the TBox T = {A0 v A, A v A00 , A v ∃r.A, ∃s.A v A} results in an infinite chain of consequences A0 v ∃r.∃r.∃r....A00 and ∃s.∃s.∃s....A0 v A00 containing nested existential quantifiers of unbounded maximal depth. Such infinite chain of consequences can be easily expressed in a finite way using the greatest fixpoint constructor ν and the least fixpoint constructor µ, thereby resulting in the inclusion axioms A0 v νX.(A00 u ∃r.X) and µX.(A0 t ∃s.X) v A00 . In the following, we show that for any EL TBox T and any signature Σ, a corresponding UI of T w.r.t. Σ in ELµ(t),ν can always be computed. For this purpose, we reduce the problem of computing UI to the problem of computing most general subconcepts MGS(Σ, T , A) and most specific superconcepts MSS(Σ, T , A) for each concept A ∈ sig(T ). Definition 2. Let T be an EL TBox and Σ a signature. Further, let A ∈ NC . A set of EL concepts Ci for 1 ≤ i ≤ n is MSS(T , Σ, A), if: – sig(Ci ) ⊆ Σ for all i, – T |= Ci v A and T 6|= A v Ci , F F – for all EL concepts D with sig(D) ⊆ Σ holds:  T |= D v A, iff T |= D v Ci . A set of EL concepts Ci for 1 ≤ i ≤ n is MGS(T , Σ, A) if the following conditions are fulfilled: – sig(Ci ) ⊆ Σ for all i,   – T |= A v Ci and T 6|= Ci v A – for all EL concepts D with sig(D) ⊆ Σ holds:  T |= A v D, iff T |= Ci v D. We denote MSS(A) and MGS(A) expressed in logic L by MSSL (A) and MGSL (A). If MGS(T , Σ, A) consists of several incomparable disjuncts Ci , it cannot be expressed by an EL concept. However, in the following, it will come into notice that this is not further problematic for the computation of UI, since the disjunction appears only on the left-hand side and can therefore be expressed by the means of several inclusion axioms. If the TBox T and the signature Σ do not change, we omit them and simply write MSS(A) and MGS(A). For the remainder of this paper, we fix T to be a general EL TBox and Σ a signature. 4 Normalization In order to simplify the computation of MGS and MSS, we apply the following normal- ization thereby restricting the syntactic form of T . Analogously to the normalization employed in other approaches ([1], [6], [7]), we decompose complex axioms into syn- tactically simple ones. The decomposition is realized recursively by replacing expres- sions B1 u ... u Bn and ∃r.B with fresh concept symbols until each axiom in T is one of {A v B, A ≡ B1 u ... u Bn , A ≡ ∃r.B}, where A, B, Bi ∈ NC ∪ {>} and r ∈ NR . For this purpose, we introduce a minimal required set of fresh concept symbols A0 ∈ ND and the corresponding definition axioms (A0 ≡ C) for each of them. In what follows, we assume that knowledge bases are normalized and refer to NC ∪ ND as NC . Since concept symbols in ND are fresh, they do not appear in Σ and are therefore elements of the forgotten signature Σ. Further, we assume that equivalent concept symbols have Algorithm 1 computing MGScore (A) for an EL TBox T and a signature Σ 1: M ← MGScond (D, A), D ∈ NC such that T |= D v A, A , D S  2: for all A ≡ 1≤i≤n Bi ∈ T do  3: M ← M ∪ { C∈REDUCEMSS ({Ci |1≤i≤n}) C|(C1 , ..., Cn ) ∈ MGScond (B1 , A) × ... × MGScond (Bn , A)} 4: end for 5: for all A ≡ ∃r.B ∈ T with r ∈ Σ do 6: M ← M ∪ {∃r.C|C ∈ MGScond (B, A)} 7: end for 8: return REDUCEMGS (M) Algorithm 2 computing MSScore (A) for an EL TBox T and a signature Σ 1: M ← MSScond (D, A), D ∈ NC+ such that T |= A v D, A , D S  2: for all A ≡ 1≤i≤n Bi ∈ T do 3: M ← M ∪ {C|C ∈ MSScond (Bi , A)} 4: end for 5: for all A ≡ ∃r.B ∈ T with r ∈ Σ do  6: M ← M ∪ {∃r. C∈MSScond (B,A) C} 7: end for 8: return REDUCEMSS (M) been replaced by a single representative of the corresponding equivalence class.1 The following lemma summarizes the properties of normalized TBoxes. Lemma 1. Any T can be extended into a normalized TBox T 0 and each model of T can be extended into a model of T 0 . Proof Sketch. All introduced concepts in ND are defined in terms of concepts with sig(C) ⊆ sig(T ), therefore each model of T can be extended into a model of T 0 . t u 5 Computing MGS and MSS for Acyclic TBoxes Given an acyclic, normalized EL TBox T and a signature Σ, Algorithms 1 and 2 compute for each A ∈ NC the elements of MGS(A) and MSS(A), respectively. The algo- rithms are derived from a Gentzen-style proof system and proceed along the definitions for A in T as well as the inferred inclusions between atomic concepts involving A. The computation is indirectly recursive and consists of the procedure MGScore (MSScore ) containing the core computation and procedure MGScond (MSScond ) realizing the termi- nation of the computation: if the first parameter of MGScond (MSScond ) – a concept B – is in Σ, it returns B itself, which is the basecase of the computation; otherwise, it calls in turn MGScore (B) (MSScore (B)). Thereby, MGScond (MSScond ) ensures that MGS and MSS only contain Σ-concepts. To avoid confusion, we denote MGS(A) and MSS(A) obtained using this simple definition of MGScond (MSScond ) by MGSacyc (A) and MSSacyc (A). 1 The elimination of equivalent symbols does not affect the correctness or completeness of the uniform interpolation, since the removed symbols can easily be included into the resulting TBox. Definition 3. Let T an acyclic EL TBox and A ∈ NC . MGSacyc (A) = MGScore (A) and MSSacyc (A) = MSScore (A). While this separation of concerns between MGScore (A) (MSScore (A)) and MGScond (B, A) (MSScond (B, A)) appears not necessary in the simple case of acyclic TBoxes, in the next section we extend the computation to the general case of GCIs by adding further condi- tions to MGScond (B, A) (MSScond (B, A)) without changing the core computation presented in Algorithms 1 and 2. In particular, the role of second parameter of MGScond will be- come clear. The functions REDUCEMGS and REDUCEMSS eliminate redundancy within the computed results, which is not just an optimization, but will also play an important role when deciding the existence of a uniform interpolant in EL. The two functions are defined as follows: Definition 4. Let M = {Ci |0 ≤ i ≤ n} be a set of EL concepts and Te = {}. REDUCEMSS (M) = {Ci ∈ M| there is no C j ∈ M such that Te |= C j v Ci } REDUCEMGS (M) = {Ci ∈ M| the is no C j ∈ M such that Te |= Ci v C j } Both, REDUCE and REDUCEC , can be easily realized using standard reasoning procedures in ELµ(t),ν , which is known to be decidable in ExpT ime [4]. It is easy to see that, in case of an acyclic TBox T , both algorithms terminate, while, in case of cyclic terminologies, the algorithms do not need to terminate. In the next section, we extend the computation to be applicable to general TBoxes and ensure the termination also for this case. 6 MGS and MSS for General TBoxes As already mentioned, the computation based on the simple version of MGScond (B, A) and MSScond (B, A) does not always terminate in case of general TBoxes such as the TBox in Example 1. In order to exactly specify the case, in which Algorithms 1 and 2 do not terminate, we use the following graph structures representing the possible flow of computation of MGScore and MSScore for a particular TBox T (independent from a particular signature): Definition 5. The MSS- and MGS-graphs AMSS (T ) and AMGS (T ) are defined as – AMSS (T ) = (ΓMSS , Q, EMSS ) with the set of edge labels ΓMSS = NR ∪ {v}, the set of states Q = NC and the set of edges EMSS = {(A, r, B)|A ≡ ∃r.B ∈ T } ∪ {(A, v, B)|T |= A v B, A , B}, where A, B ∈ Q and r ∈ ΓMSS . – AMGS (T ) = (ΓMGS , Q, EMGS ) with the set of edge labels ΓMGS = NR ∪ {w, u}, the set of states Q = NC and the set of edges EMGS = {(A, r, B)|A ≡ ∃r.B ∈ T } ∪ {(A, w, B)|T |= A w B, A , B}∪{(A, u, B)|A ≡ BuC ∈ T for any conjunction C of elements from Q}, where A, B ∈ Q and r ∈ ΓMGS . The two graphs can be constructed in linear time after the classification of the normalized TBox is finished. For X ∈ {MGS, MSS}, we denote the set of the paths in AX (T , Σ) from A to B as LX (A, B) and the set of the intersection-free paths from node Fig. 1. MGS-graph (left) and MSS-graph (right) of T . A to itself as L1X (A, A) , i.e., such paths not contain any node except for A more than once. As illustrated by the example below, cyclic paths in AMSS (T ) and AMGS (T ) do not necessarily coincide. Example 2. The corresponding MGS- and MSS-graphs of the TBox T = {A1 ≡ ∃s.A2 , A3 ≡ ∃r.A2 , A3 v A4 , A5 ≡ A3 u A4 , A5 v A2 , A5 v A6 } are shown in Fig. 1. Given AMSS (T ) and AMGS (T ), we can easily determine for a particular signature Σ, whether the computation of the UI by the means of Algorithms 1 and 2 with the simple version of MGScond (B, A) and MSScond (B, A) terminates: if neither AMSS (T ) nor AMGS (T ) contain cyclic paths formed only by concepts from Σ. Note that other cycles do not lead to a non-termination, since MGScond (B, A) = {B} for any B ∈ Σ and A ∈ NC , i.e., the computation terminates. We denote such cyclic intersection-free paths from A containing only concepts from Σ by L1,ΣX (A, A) and the sets of concepts involved in such cycles by Σ C,MGS = {A|A ∈ Σ, LMGS 1,Σ (A, A) , ∅} and Σ C,MSS = {A|A ∈ Σ, LMSS 1,Σ (A, A) , ∅}. In order to be able to compute MSS and MGS also in case of Σ C,MSS ∪ Σ C,MGS , ∅, we extend MGScond (A, B) and MSScond (A, B) by introducing a new condition for concepts A ∈ Σ C,MSS ∪ Σ C,MGS . Here, we require the second parameter B to determine when the quantification of the fixpoint expressions is necessary. If MGScond or MSScond is called from outside of the corresponding cycles (Σ C,MGS for MGScond and Σ C,MSS for MSScond ), we return the complete fixpoint expression in its quantified form. Otherwise, we prefer to return the simplest possible value necessary, which can then be used as a part of a more complex, quantified concept expression. This second parameter is used by the caller – MGScore or MSScore – to pass its own parameter to the called MGScond or MSScond and let it then decide, whether to return a quantified fixpoint expression or a non-quantified one. Definition 6. Let n, m be the cardinality of Σ C,MSS and Σ C,MGS , respectively. Further, let Ai ∈ Σ C,MSS with 0 ≤ i ≤ n and A j ∈ Σ C,MGS with 0 ≤ j ≤ m. Let {X(Ai )|Ai ∈ Σ C,MSS } and {Y(A j )|A j ∈ Σ C,MGS } be two disjoint sets of concept variables. Then, we define for each Ai ∈ Σ C,MSS and each A j ∈ Σ C,MGS : N(Ai ) = νi X(A1 ), ..., X(An ). uC∈MSScore (A1 ) C, ..., uC∈MSScore (An )C M(A j ) = µ j Y(A1 ), ..., Y(Am ). tC∈MGScore (A1 ) C, ..., tC∈MGScore (Am )C. MSScond (A, B) and MGScond (A, B) for any A, B ∈ NC is then given by: MSScond (A, B) = MGScond (A, B) = {A} if A ∈ Σ {A} if A ∈ Σ         {X(A)} if A ∈ Σ C,MSS , {Y(A)} if A ∈ Σ C,MGS ,           B ∈ Σ C,MSS B ∈ Σ C,MGS           {N(A)} if A ∈ Σ C,MSS , {M(A)} if A ∈ Σ C,MGS ,           < Σ C,MSS < Σ C,MGS        B      B  MSScore (A) otherwise   MGScore (A) otherwise ,  and MGS(A) = MGScond (A, >) and MSS(A) = MSScond (A, >). Note that, in case of an acyclic TBox, MGS(A) coincides with MGSacyc (A) described in Section 5, and the same holds for MSS(A). Theorem 1 (Termination). Let A ∈ NC . The computation of MSS(A) and MGS(A) al- ways terminates in at most exponential time. Proof Sketch. We first show by induction in case Σ C,MSS = ∅ that the computation of MSS(A) for each A ∈ NC terminates. Then, we consider the case Σ C,MSS , ∅. MSScond en- capsulates all concepts in Σ C,MSS into a single computational unit with direct or indirect incoming dependencies from concepts referencing concepts in Σ C,MSS and direct or in- direct outgoing dependencies to concepts referenced from any concept in Σ C,MSS . These two sets of referencing and referenced concepts are disjoint by definition of cyclicity. In the computation of N(A), either concept variables or results of acyclic computations of MSS(B) for B not referencing Σ C,MSS are used, therefore each computation terminates. Once N(A) is computed, references to A ∈ Σ C,MSS do not require further computation and the remaining computation terminates as shown in case Σ C,MSS , ∅. Since the structure of MGScond and MSScond is analogous and MGScore also only iterates through the finite in- put directly, the argumentation for the termination of MGS is identical. The complexity is due to the conjunction constructs introduced in line 3 of Algorithm 1. t u Theorem 2 (Correctness MSS and MGS). Let A ∈ NC . The computed MSS(A) and MGS(A) satisfy the conditions stated in Definition 2. The proof of Theorem 2 is based on a Gentzen-style proof system for normalized TBoxes. 7 Computing Uniform Interpolants Given MGS(A) and MSS(A) for each A ∈ NC , we can compute the UI in ELµ(t),ν as follows: Definition 7. UI(T , Σ) = UIΣ,MSS (T , Σ) ∪ UIΣ,MGS (T , Σ) ∪ UIΣ (T , Σ) with – UIΣ,MSS (T , Σ) = {A v D|A ∈ NC ∩ Σ, D ∈ MSS(A)}, – UIΣ,MGS (T , Σ) = {C v A|A ∈ NC ∩ Σ, C ∈ MGS(A)}, – UIΣ (T , Σ) = {C v D| there is A ∈ NC ∩ Σ, such that C ∈ MGS(A) and D ∈ MSS(A)}. Now, we have to prove that UI(T , Σ) ≡cΣ T , i.e., the TBox UI(T , Σ) is in fact a uniform interpolant of T w.r.t. Σ. Theorem 3 (UI). UI(T , Σ) always exists and it holds that UI(T , Σ) ≡cΣ T . The proof of Theorem 3 is also based on a Gentzen-style proof system for normalized TBoxes. Deciding the Existence of UI in EL Clearly, if T does not contain pure Σ cycles, the UI(T , Σ) only contains EL constructs and, therefore, a UI in EL exists. This would be a sufficient, but not necessary criterion for the existence of a UI. From Definition 7, we can deduce a very general form of criterion requiring the deductive closure of any UI2 to contain an (arbitrary) finite EL justification for the set of all non-EL axioms in the UI(T , Σ). Interestingly, given the EL TBox UIEL (T , Σ) obtained by extracting the EL part of each fixpoint concept within the non-mutual representation of UI(T , Σ), this criterion can be easily checked, since it is equivalent to a very simple criterion, which is an immediate consequence of the following theorem: Theorem 4 (Existence). Let UIEL (T , Σ) be the EL TBox obtained by extracting the EL part of each fixpoint concept within the non-mutual representation of UI(T , Σ) and let T 0 be an EL TBox with sig(T 0 ) ⊆ Σ such that T 0 ≡cΣ T . Then UIEL (T , Σ) ≡ T 0 . The theorem claims that, if a finite EL justification for the set of all non-EL axioms in UI(T , Σ) exists, it is already a contained in the non-mutual representation of UI(T , Σ). Subsequently, a UI of T w.r.t. Σ in EL exists, iff UIEL (T , Σ) |= UI(T , Σ). The proof of this theorem is based on the ideas stated in Lemmas 2 and 3, which show that there is a close relation between the existence of a UI in EL and redundancy in UI(T , Σ). Lemma 2. Let T 0 be an EL TBox with sig(T 0 ) ⊆ Σ such that T 0 ≡cΣ T . Further, let A ∈ Σ C,MGS with C1 ∈ MGS(A) and C2 ∈ MSS(A). Then there is an EL concept C 0 such that – T 6|= C 0 ≡ C1 and T 6|= C 0 ≡ C2 – {} |= C1 v C 0 – UI(T , Σ) |= C 0 v C2 . Let A ∈ Σ C,MSS with C1 ∈ MGS(A) and C2 ∈ MSS(A). Then there is an EL concept C 0 such that – T 6|= C 0 ≡ C1 and T 6|= C 0 ≡ C2 – {} |= C 0 v C2 – UI(T , Σ) |= C1 v C 0 . 2 The deductive closure is the same for any UI by definition. Proof Sketch. Consider C1 = µX.(A t ∃r.X), which is the simplest possible non-EL concept in MGS. C1 is semantically equivalent to an infinite disjunction of more and more specific EL concepts. The language constructs of EL do not allow us to specify a concept, which captures exactly the subset of the interpretation domain C1I in all models. Let C2 be an arbitrary concept with UI(T , Σ) |= C1 v C2 . If C1 v C2 is a consequence of T 0 , then there must be an EL concept C10 , which subsumes C1I in all models. Since T 0 is a finite EL TBox, it must hold that T 0 |= C1 v C10 , i.e., the latter inclusion axiom must be derived from the finite EL TBox itself (e.g., C10 = B with {∃r.B v B, A v B} ∈ T 0 ). Moreover C10 v C2 must have a justification in T 0 consisting of finitely many EL axioms. The same argumentation applies to C2 as a concept with greatest fixpoint constructs. t u The above proof is the first step towards a connection between the redundancy in UI(T , Σ) and the existence of a UI in EL. Since {C1 v C 0 , C 0 v C2 } |= C1 v C2 and any minimal justification of {C1 v C 0 , C 0 v C2 } in any T 0 does not contain C1 v C2 , it also holds that UI(T , Σ) ∪ UIEL (T , Σ) \ {C1 v C2 } |= C1 v C2 . There- fore, if T 0 exists, each non-EL axiom is redundant, i.e., it could be removed from UI(T , Σ) ∪ UIEL (T , Σ) without losing any consequences. To avoid confusion, we de- note the non-mutual representation of MSS(A) and MGS(A) with the corresponding EL parts explicitly appearing outside of all fixpoint quantifiers by MSS(A) ∪ EL(MSS(A)) and MGS(A) ∪ EL(MGS(A)). The functions REDUCEMSS and REDUCEMGS have to be applied also when computing MSS(A) ∪ EL(MSS(A)) and MGS(A) ∪ EL(MGS(A)). Therefore, the re- dundancy can only appear during the construction of UI(T , Σ) ∪ UIEL (T , Σ). From the definition of MGS and MSS follows that the sets UIΣ,MSS (T , Σ) and UIΣ,MGS (T , Σ) in Defi- nition 7 cannot be redundant if the sets MSS(A) ∪ EL(MSS(A)) and MGS(A) ∪ EL(MGS(A)) contain only incomparable elements. Therefore, it remains to consider the redundancy introduced during the construction of UIΣ (T , Σ). We denote by PΣ = {(C1 , C2 )| there is A ∈ Σ s.t. C1 ∈ MGS(A) ∪ EL(MGS(A)), C2 ∈ MSS(A) ∪ EL(MSS(A))} the set of all con- cept pairs relevant for the construction of UIΣ (T , Σ) and the subset of PΣ containing the “redundant” concept pairs by R = {(C1 , C2 ) ∈ PΣ |(UI(T , Σ) ∪ UIEL (T , Σ)) \ {C1 v C2 } |= C1 v C2 }. I.e., R is the set of concept pairs that are potentially nonessential for the construction of a UI due to entailment of the corresponding inclusion axiom by the remainder of a UI if the axiom itself is omitted. Due to possible dependen- cies between the elements of R, there may be several different maximal subsets M of R such that (UI(T , Σ) ∪ UIEL (T , Σ)) \ {C1 v C2 |(C1 , C2 ) ∈ M} |= UI(T , Σ). We denote the set of all such maximal subsets of R as RMAX = {M|M ⊆ R, (UI(T , Σ) ∪ UIEL (T , Σ)) \ {C1 v C2 |(C1 , C2 ) ∈ M} |= UI(T , Σ), for all (C10 , C20 ) ∈ PΣ \ M holds (UI(T , Σ) ∪ UIEL (T , Σ)) \ ({C10 v C20 } ∪ {C1 v C2 |(C1 , C2 ) ∈ M}) 6|= UI(T , Σ)}. The next lemma states that if a concept pair with at least one non-EL concept is contained in one set M ∈ RMAX , it is contained in all M ∈ RMAX . Lemma 3. Let T 0 be an EL TBox with sig(T 0 ) ⊆ Σ such that T 0 ≡cΣ T . Further, let A ∈ Σ C,MSS ∪ Σ C,MGS with C1 ∈ MGS(A) and C2 ∈ MSS(A). Let let M 0 ∈ RMAX such that (C1 , C2 ) ∈ M 0 . Then for each M ∈ RMAX holds (C1 , C2 ) ∈ M. Note that all concept pairs with at least one non-EL concept are contained in the inter- section of RMAX , iff UIEL (T , Σ) ≡ T 0 . As a consequence of the above two lemmas and the fact that for any (C1 , C2 ) ∈ R there exists at least one M ∈ RMAX , it is sufficient to check whether all concept pairs with at least one non-EL concept are contained in R to determine whether the T 0 in Theorem 4 exists. 8 Summary In this paper, we provide an ExpT ime algorithm for computing a uniform interpolant of general EL terminologies preserving all EL concept inclusions for a particular signa- ture based on the notion of most general subconcepts and most specific superconcepts. The result of the computation is expressed in logic ELµ(t),ν —an extension of EL with least fixpoint and greatest fixpoint constructors µ, ν as well as the disjunction used only on the left-hand side of concept inclusions. We also state the exact existence criteria for an EL interpolant and show how it can be obtained from the corresponding interpolant expressed in ELµ(t),ν . References 1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05. Morgan-Kaufmann Pub- lishers, Edinburgh, UK (2005) 2. Baader, F.: Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles. In: Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI’03). pp. 319–324 (2003) 3. Baader, F., Sertkaya, B., Turhan, A.Y.: Computing the least common subsumer w.r.t. a back- ground terminology. J. Applied Logic 5(3), 392–420 (2007) 4. Calvanese, D., De Giacomo, G., Lenzerini, M.: Reasoning in expressive description logics with fixpoints based on automata on infinite trees. In: Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI’99). pp. 84–89 (1999) 5. Colucci, S., Di Noia, T., Di Sciascio, E., Donini, F.M., Ragone, A.: A unified framework for non-standard reasoning services in description logics. In: Proc. of the 19th European Conf. on Artificial Intelligence (ECAI’10). pp. 479–484 (2010) 6. Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: IJCAI. pp. 2040–2045 (July 11-17 2009) 7. Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-scale de- scription logic terminologies. In: Proc. of the 21st Int.Joint Conf. on Artificial Intelligence (IJCAI’09). pp. 830–835 (2009) 8. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and mod- ule extraction, with an application to dl-lite. Artif. Intell. 174, 1093–1141 (October 2010) 9. Lutz, C., Piro, R., Wolter, F.: Enriching EL-concepts with greatest fixpoints. In: Proc. of the 19th European Conf. on Artificial Intelligence (ECAI’10). pp. 41–46 (2010) 10. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive de- scription logics. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI-11) (2011) 11. Nikitina, N.: Uniform interpolation in general EL-terminologies. Techreport, Institut AIFB, KIT, Karlsruhe (Mai 2011) 12. Schild, K.: Terminological cycles and the propositional µ-calculus. In: Proc. of the KR’94. pp. 509–520 (1994)