Recently, di erent forgetting approaches for knowledge bases expressed in di erent 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 su cient, 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 signature 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.
The importance of non-standard reasoning services supporting knowledge engineers in
modelling a particular domain or in understanding existing models by visualizing
implicit dependencies between concepts and roles was pointed out by the research
community [
Clearly, the existence of the results for such reasoning problems is closely related
to the notion of fixpoint semantics. For instance, Baader [
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
language 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 [
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 ::= Aj>jC u Cj9r: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( ), respectively, 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 [ f>g as N+.
C
Before introducing the fixpoint operators, we recall the semantics of the above introduced DL constructs, which is defined by the means of interpretations. An interpretation I is given by the domain I and a function I assigning each concept A 2 NC a subset AI of I and each role r 2 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 = CI \ DI and (9r:C)I = fx j (x; y) 2 rI; y 2 CIg. An interpretation I satisfies an axiom C v D if CI 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 = CI [ DI.
We now introduce the logics EL (t); , a fragment of monadic second order
logics 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 [
C ::= XjAj>j X:C jC u C j9r:C
C ::= XjAj>j X:C jC t C jC u C j9r: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 CI;#[X!W]. The semantics of EL (t); concepts is defined by ( X:C)I;# = [fW ( X:C)I;# = \fW
IjW
CI;#[X!W]g IjCI;#[X!W]
Wg:
In order to allow for more succinct concept expressions, we use an extended
version of the fixpoint constructs allowing for mutual recursion [
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
terminologies defined analogously to previous work on inseparability, e.g., [
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 j= C v D, i T2 j= 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 ) n 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 = fA0 v A; A v A00; A v 9r:A; 9s:A v Ag results in an infinite chain of consequences A0 v 9r:9r:9r::::A00 and 9s:9s:9s::::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 9r:X) and X:(A0 t 9s: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 2 sig(T ).
– sig(Ci) for all i, – T j= F Ci v A and T 6j= A v F Ci, – for all EL concepts D with sig(D)
T j= D v A, i T j= D v Ci.
fulfilled: – sig(Ci)
for all i, – T j= A v Ci and T 6j= Ci v A – for all EL concepts D with sig(D)
T j= A v D, i T j= Ci v D.
holds: holds: i
n is MGS(T ; ; A) if the following conditions are 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
In order to simplify the computation of MGS and MSS, we apply the following
normalization thereby restricting the syntactic form of T . Analogously to the normalization
employed in other approaches ([
1 i n Bi 2 T do 9r:B 2 T with r 2
do
M [ f C2REDUCEMSS(fCij1 i ng) Cj(C1; :::; Cn) 2 MGScond(B1; A) ::: MGScond(Bn; A)g 8: return REDUCEMGS(M) Algorithm 2 computing MSScore(A) for an EL TBox T and a signature S MSScond(D; A); D 2 NC+ such that T j= A v D; A , D
1 i n Bi 2 T do
9r:B 2 T with r 2 M [ f9r: C2MSScond(B;A) Cg
do sig(T ), therefore each model of T can be extended into a model of T 0. tu 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 2 NC the elements of MGS(A) and MSS(A), respectively. The algorithms 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 termination 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 a ect 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 2 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 conditions 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 become 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 = fCij0 i
ng be a set of EL concepts and Te = fg.
REDUCEMSS(M) = fCi 2 Mj there is no C j 2 M such that Te j= C j v Cig
REDUCEMGS(M) = fCi 2 Mj the is no C j 2 M such that Te j= Ci v C jg
Both, REDUCE and REDUCEC, can be easily realized using standard reasoning procedures
in EL (t); , which is known to be decidable in E xpT ime [
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):
– AMSS(T ) = ( MSS; Q; EMSS) with the set of edge labels MSS = NR [ fvg, the set of states Q = NC and the set of edges EMSS = f(A; r; B)jA 9r:B 2 T g [ f(A; v; B)jT j= A v B; A , Bg, where A; B 2 Q and r 2 MSS. – AMGS(T ) = ( MGS; Q; EMGS) with the set of edge labels MGS = NR [ fw; ug, the set of states Q = NC and the set of edges EMGS = f(A; r; B)jA 9r:B 2 T g [ f(A; w; B)jT j=
The two graphs can be constructed in linear time after the classification of the normalized TBox is finished. For X 2 fMGS; MSSg, 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
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 = fA1 9r:A2; A3 v A4; A5 A3 u A4; A5 v A2; A5 v A6g are shown in Fig. 1. 9s:A2; A3 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) = fBg for any B 2 and A 2 NC , i.e., the computation terminates. We denote such cyclic intersection-free paths from A containing only concepts from by L1X; (A; A) and the sets of concepts involved in such cycles by C;MGS = fAjA 2 ; LM1;GS(A; A) , ;g and C;MSS = fAjA 2 ; LM1;SS(A; A) , ;g.
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 2 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.
C;MGS : Ai 2 fY (A j)jA j 2
Definition 6. Let n; m be the cardinality of C;MSS and C;MGS, respectively. Further, let
N(Ai) = i X(A1); :::; X(An): uC2MSScore(A1) C; :::; uC2MSScore(An)C M(A j) =
jY (A1); :::; Y (Am): tC2MGScore(A1) C; :::; tC2MGScore(Am)C: MSScond(A; B) and MGScond(A; B) for any A; B 2 NC is then given by: > > > > > > > < 8 > > > > > > > > > > > > > > >
MSScond(A; B) =
fAg if A 2 fX(A)g if A 2 C;MSS, fN(A)g if A 2 C;MSS,
B 2 C;MSS B <
C;MSS >:> MSScore(A) otherwise > > > > > > > < 8 > > > > > > > > > > > > > > >
MGScond(A; B) =
fAg if A 2 fY(A)g if A 2 C;MGS, fM(A)g if A 2 C;MGS,
B 2 C;MGS B <
C;MGS >:> 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). ways terminates in at most exponential time.
Proof Sketch. We first show by induction in case MSS(A) for each A 2 NC terminates. Then, we consider the case C;MSS , ;. MSScond encapsulates 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 indirect 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.
C;MSS = ; that the computation of Once N(A) is computed, references to A 2 the remaining computation terminates as shown in case C;MSS do not require further computation and
C;MSS , ;. Since the structure of MGScond and MSScond is analogous and MGScore also only iterates through the finite input 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. tu MGS(A) satisfy the conditions stated in Definition 2.
Theorem 2 (Correctness MSS and MGS). Let A 2 NC. The computed MSS(A) and The proof of Theorem 2 is based on a Gentzen-style proof system for normalized TBoxes. follows: 7
Given MGS(A) and MSS(A) for each A 2 NC, we can compute the UI in EL (t); as Definition 7. UI(T ; ) = UI ;MSS(T ; ) [ UI ;MGS(T ; ) [ UI (T ; ) with – UI ;MSS(T ; ) = fA v DjA 2 NC \ ; D 2 MSS(A)g, – UI ;MGS(T ; ) = fC v A A 2 NC \ ; C 2 MGS(A)g,
j – UI (T ; ) = fC v Dj there is A 2 NC \ , such that C 2 MGS(A) and D 2 MSS(A)g. 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 su cient, 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:
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, i UIEL(T ; ) j= 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
that – T 6j= C0 C1 and T 6j= C0 – fg j= C1 v C0 – UI(T ; ) j= C0 v C2. C2 Let A 2 such that
– T 6j= C0 C1 and T 6j= C0 – fg j= C0 v C2 – UI(T ; ) j= C1 v C0.
C2 2 The deductive closure is the same for any UI by definition. greatest fixpoint constructs.
Proof Sketch. Consider C1 =
X:(A t 9r: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 ; ) j= C1 v C2. If C1 v C2 is a consequence of T 0, then there must be an EL concept C0 , which subsumes C1I in all 1 models. Since T 0 is a finite EL TBox, it must hold that T 0 j= C1 v C10, i.e., the latter f9r:B v B; A v Bg 2 T 0). Moreover C10 v C2 must have a justification in T inclusion axiom must be derived from the finite EL TBox itself (e.g., C10 = B with 0 consisting of finitely many EL axioms. The same argumentation applies to C2 as a concept with tu
The above proof is the first step towards a connection between the redundancy in and any minimal justification of fC1 v C0; C0 v C2g in any T UI(T ; ) and the existence of a UI in EL. Since fC1 v C0; C0 v C2g j= C1 v C2 0 does not contain C1 v C2, it also holds that UI(T ; ) [ UIEL(T ; ) n fC1 v C2g j= C1 v C2. Therefore, 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 denote 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 redundancy 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 Definition 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 = f(C1; C2)j there is A 2
s.t. C1 2 MGS(A) [ EL(MGS(A)); C2 2 MSS(A) [ EL(MSS(A))g the set of all concept pairs relevant for the construction of UI (T ; ) and the subset of P the “redundant” concept pairs by R = f(C1; C2) 2 P j(UI(T ; ) [ UIEL(T ; )) n fC1 v containing C2g j= C1 v C2g. 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 dependencies between the elements of R, there may be several di erent maximal subsets M of R such that (UI(T ; ) [ UIEL(T ; )) n fC1 v C2j(C1; C2) 2 Mg j= UI(T ; ). We denote the set of all such maximal subsets of R as RMAX = fMjM UIEL(T ; )) n fC1 v C2j(C1; C2) 2 Mg j= UI(T ; ); for all (C0 ; C0 ) 2 P 1 2
R; (UI(T ; ) [ n M holds (UI(T ; ) [ UIEL(T ; )) n (fC10 v C20g [ fC1 v C2j(C1; C2) 2 Mg) 6j= UI(T ; )g. The next lemma states that if a concept pair with at least one non-EL concept is contained in one set M 2 RMAX, it is contained in all M 2 RMAX. (C1; C2) 2 M0. Then for each M 2 RMAX holds (C1; C2) 2 M.
such that T 0 c
C;MSS [
Note that all concept pairs with at least one non-EL concept are contained in the intersection of RMAX, i UIEL(T ; )
T 0. As a consequence of the above two lemmas and the fact that for any (C1; C2) 2 R there exists at least one M 2 RMAX, it is su cient 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
In this paper, we provide an E x pT ime algorithm for computing a uniform interpolant of general EL terminologies preserving all EL concept inclusions for a particular signature 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); .