It is known that in Description Logics explicit concept de nability is directly related to concept interpolation. The problem to decide whether a concept is de nable under a TBox wrt a signature usually reduces to entailment in the underlying logic. If an explicit de nition exists, then it can be found as a concept interpolant for a concept inclusion entailed by an appropriately chosen TBox. In fact, it can be extracted from a corresponding proof of the concept inclusion. We describe a graph structure called enriched model that represents proofs in normalized ELTBoxes and show that, built once for a normalization of a given TBox T , it can be used for deciding the existence or direct computation of explicit de nitions of concepts under arbitrary subsets of axioms of T and wrt di erent subsignatures of T . Solving this computational problem has applications in collaborative ontology engineering and is an important part of the recently proposed algorithms for ontology decomposition.
In the paper, we consider the Description Logic E L with the standard set
of constructors for concepts, i.e. the conjunction, existential restriction, and the
distinguished concept symbol >. Consider a scenario in which several experts
are working on the same ontology T and each expert has a vocabulary (a set
of concept and role names) she is using for de ning complex concepts in the
ontology. Vocabularies need not be distinct between experts. If at some point an
expert encounters an axiom in the ontology and a concept which is built using
foreign vocabularies, she wants to gure out whether it still can be de ned in her
own vocabulary. Or at least, whether the encountered concept can be partially
reformulated to use less symbols from foreign vocabularies (and more symbols
from her own one). If the answer is \yes", then the expert has an option to see
the actual reformulation of the concept and can replace it with the obtained
reformulation (if she is allowed to do so under a collaborative ontology change
policy). To illustrate this idea, consider the following simple example. Consider
the TBox T = f'; A v B; D v Ag, where ' = A u B v D. Suppose an
expert is interested in a reformulation of the concept A u B. Independently of
what the expert's vocabulary is, this concept can be reformulated as A, since
T j= A u B A, and it can be replaced with A giving a TBox equivalent to T .
Now assume that the expert's vocabulary is fDg. We have T j= AuB D, but if
? The full paper is available at http://persons.iis.nsk.su/en/person/ponom/papers
we replace the concept AuB with D, we obtain the TBox which is not equivalent
to the initial one. In other words, even though the required reformulation of the
concept A u B exists, it can not be used instead of A u B without further
modi cations of the TBox (e.g. adding the inclusion A v D as an additional
axiom to T ). The reason is that T nf'g 6j= AuB D, i.e. the axiom ' is essential
for proving this equivalence. Thus, the given example demonstrates the need to
check for de nability of concepts under certain subsets of a TBox. Now consider
the TBox S = f'; A v D; 9r:D v 9r:Ag, where ' = 9r:A v B, and assume
that the expert's vocabulary is fDg. We have S n f'g j= 9r:A 9r:D, i.e. the
concept 9r:A can be partially reformulated as 9r:D. Note that the subsignature
which can not be changed under any reformulation wrt the expert's vocabulary
(here, the single symbol r) may not be known in advance and has to be guessed.
It is observed in the results of [
Given a TBox T , a concept C is said to be explicitly de nable under T wrt
a signature if T j= C E, where E is a concept over . The problem to
decide whether C is equivalent in T to a concept containing less symbols from
sig (C) n (thus, possibly having more -symbols than C does) is called the
problem of partial concept reformulation (under T wrt ). Explicit de nability
was studied in Description Logics in the context of query rewriting (Sect. 3 in
[
The aim of the paper is to present the idea that the standard (canonical)
model of an EL-TBox with the closure operators S and R (in the sense of [
Let Nc and Nr stand, as usual, for the countably in nite sets of concept and role names in the alphabet of the language EL. Denote Nc> = Nc [ f>g and let ./ be the symbol for either v or . A formula is an expression of the form C1 ./ C2, where C1; C2 are concepts, and a TBox is a nite set of formulas which does not contain C1 C2 and C1 v C2 simultaneously for some concepts C1; C2. If is a signature, then T erm( ) will stand for the set of all concepts in the signature and if Nc, then T aut( ) will denote the set of tautologies of the form > v >, A v >, A v A, for each A 2 . Let T be a TBox. The notations sub (T ), NcT , and NrT will stand for the sets of all concepts, concept names, and role names respectively, occurring in axioms of T , while Nc>(T ) will be the shorthand for NcT [ f>g. The notation sig (T ) will mean the signature of T and will be slightly abused to denote the signature of a formula or a concept. If C 2 sub (T ) is a concept and A 2 Nc, then T (C=A) will stand for the TBox obtained from T by substituting each occurrence of C in the LHS or RHS of axioms of T with the concept name A. We call a Tbox T 0 conservative extension of T if sig (T ) have T j= ' i
sig (T 0) and for any formula ', with sig (') T 0 j= '. sig (T ), we 3 Proofs in Enriched Models of E L-TBoxes
Informally, an enriched model is a graph structure for representing proofs in a deductive system for normal TBoxes. It is built iteratively in accordance with the inference rules and normal axioms obtained from an input TBox by normalization. In addition, an enriched model stores a map from normal to the original axioms to allow for checking the entailment of concept inclusions from di erent subsets of the input TBox. To illustrate this idea brie y, let us consider an example of eliminating a redundant axiom from a TBox.
Example 1 Consider the TBox S = f'; A v B; A v Dg, where ' = A u B v D and A; B; D 2 Nc. Note that either the rst or the last axiom can be eliminated from S giving an equivalent TBox. Let T = f'0; A v B; A v D; AuB v X; X v A; X v Bg be the conservative extension of S, where '0 = X v D and X is the \pseudonym" for the concept A u B. Note that S n f'g j= ' is equivalent to T n f'0g j= '0. Consider the following graph, where every vertex has one or two labels depicted by the containment relation 2 f (:) and an arrow marked with or . In the gure, if a vertex is marked with labels f (X) and 7! Y , then X; Y 2 NcT and T j= Y v X. The vertices marked with correspond to axioms of T witnessing these entailments. Essentially, the graph represents possible proofs of primitive concept inclusions inside T , note the two disconnected components of the graph depicting independent proofs: The right-most vertex of the second component corresponds to the entailed concept inclusion '0 = X v D. Moreover, there is a subgraph which witnesses this entailment and does not contain vertices labelled by '0. This corresponds to the fact that '0 is entailed by T nf'0gand thus, ' is redundant in S.
The graph considered in the illustration generally corresponds to what we call further enriched model of a TBox. The rest of the section is devoted to a formal justi cation of the idea of checking for entailment of concept inclusions from subsets of a TBox by means of such structures.
De nition 1 (Primitivization). A formula is called primitive if it is of the form A v B for A; B 2 Nc>. A TBox Tp is called primitivization of a Tbox T if every axiom ' of T is equivalent in Tp to a primitive axiom 'p 2 Tp, i.e. if (Tp n f'pg) [ f'g j= 'p and Tp j= '.
An extended primitivization of a TBox T is a pair hTp; 0i, where Tp is a primitivization of T and 0 : Tp ! T [ fnullg is a map, which are both obtained after the application of the following rewriting rule to each axiom of T : (Ax)
A v A (AndR) (AxTop)
A v > A v A1; :::; A v An
A v B (Ex) A v 9r:A1; A1 v A2
A v B if C1 ./ C2 2 T then T := T (Ci=Ai) [ fAi Cig, for each Ci 62 Nc>, i = 1; 2, where Ai is a fresh concept name,
0(Ai Ci) = null and if 'p is the image of C1 ./ C2 under the applied substitutions, then 0('p) = C1 ./ C2.
De nition 2 (Normalization). A formula is normal if it has one of the following forms: A v 9r:B, 9r:B v A, A1 u ::: u An v B, for n > 1, with all A; B; Ai, i = 1; ::; n, being concept names. ATBox is normal if each of its axiom is. A TBox T n is called normalization of a TBox T if it is a conservative extension of T and each axiom of T n is normal. Let Tep = hTp; 0i be an extended primitivization of a TBox T . An extended normalization of Tep is a pair hT n; i, where T n is a normalization of Tp and : T n ! T is a map such that: if A v B 2 Tp, A; B 2 Nc>, then A v B 2 T nm and (A v B) = 0(A v B); if A B 2 Tp, A; B 2 Nc>, then fA v B; B v Ag 2 T nm and (A v B) = (B v A) = 0(A B); (') = null for the rest of the axioms ' 2 T nm.
It follows from the standard decision procedure for E L (see e.g. [
We now introduce the notion of enriched model of a normal TBox. The de nition consists of two parts: the description of an enriched model as an algebraic structure and the description of the process of its construction.
! T [ T aut(NcT ), + ! Nc>(T ) [ (Nc>(T )
+
Let T be a normal TBox. An enriched model of T is a structure M = (( +; ; E); ; ; f ), where ( +; ; E) is a directed bipartite graph with the set E of edges and the set + [ of vertices augmented with maps: { : { : { f : Nc>(T ) [ NrT ! 2 The process of construction of an enriched model for a normal TBox is given in the Appendix. De nition 3 (Submodel of an enriched model). Let M = ( = ( +; ; E); ; ; f ) be an enriched model. The structure Ms = ( s = ( s+; s ; Es); s; s; fs) is called a submodel of M if s is a subgraph of , each s; s; fs is the restriction of the corresponding map from M onto the vertices of s and the following holds: { for every v 2 s , all vertices v+ 2
connected with v in s; { for every v+ 2 s+, there exists v 2 s such that (v ; v+) 2 Es; if such v is unique, then the submodel is called deterministic.
+ with (v+; v ) 2 E are in s+ and In general, the bipartite graph ( +; ; E) may not have a tree-shape due to cycles caused e.g. by equalities between concept names (recall Example 1). However, there always exist submodels which are trees and these submodels are in one-to-one correspondence with proofs in the deductive system of Figure 2. Theorem 1 (Entailment from subset of TBox in enriched model). Let T be a TBox and T ep = hTp; 0i be an extended primitivization of T . Let hT nornmor;mi. be an extended normalization of T ep and M be an enriched model of T Let C1; C2 be concepts appearing on the LHS or RHS of an axiom of T and for i = 1; 2, let Ai 2 sig (Tp) be a concept name which is either Ci (if Ci 2 Nc), or such that Ai 2 sig (Tp) n sig (T ) and Ai Ci 2 Tp. Then, for a subset S T of axioms, it holds T n S j= C1 v C2 i there is a deterministic submodel Ms = ( s = ( s+; s ; Es); s; s; fs) of M and a vertex v+ 2 s+ such that: { v+ 2 fs(A2) and s(v+) = A1, { for any non-leaf vertex v
2 s , ( s(v )) 62 S.
Therefore, in order to check the entailment T n S j= C1 v C2, it su ces to nd rst a plus-vertex v+ witnessing the entailment T norm = A1 v A2 in the enriched model M (the vertex must satisfy the conditionsj v+ 2 fs(A2) and s(v+) = A1) and if it exists, nd an inference of A1 v A2, which does not refer via the map to formulas of S, as a deterministic submodel of M containing v+. The procedure of nding this submodel reduces to a traversal of the graph ( +; ; E) of M starting from the vertex v+. The procedure is conceptually similar to the one presented in the context of computing concept interpolants in Section 4 and is therefore skipped. 4
Let T1 be a TBox, C1 be a concept from the LHS or RHS of an axiom of T , S1 T1 be a subset of axioms, and be a signature. Suppose we want to check whether C1 is {de nable under T1 n S1. Let T2 = f (T1) and S2 = f (S1) T2 be the corresponding \copy"-TBoxes (with sig (T1)\sig (T2) = ) and let C2 = f (C1) be the corresponding \copy"-concept obtained by a renaming function f . We may assume that f (T1 nS1) = T2 nS2 and thus, by concept interpolation, de nability is equivalent to the condition (T1 n S1) [ (T2 n S2) j= C1 v C2. The observations from Section 3 imply that it su ces to consider the case when the TBox T1 is normal and Ci is a concept name from sig (Ti) n , for i = 1; 2. Then (T1 n S1) [ (T2 n S+2); j= C1 v C2 holds i there is a submodel Ms in an enriched model M = (( ; E); ; ; f ) of T1 [ T2 and a vertex v+ 2 + certifying this entailment. Let us show how a concept interpolant for the inclusion C1 v C2 (i.e. an explicit -de nition of C1 under T n S) can be computed while searching for this submodel in M . The submodel Ms must be in direct correspondence with a proof of C1 v C2 from (T1 nS1)[(T2 nS2). We have sig (T1)\sig (T2) = and Ci 2 sig (Ti) n , for i = 1; 2, so it su ces to understand how a concept interpolant between C1 and C2 can be extracted from a proof of C1 v C2 in this situation, which is the purpose of Theorem 3 given in the Appendix. The property of concept interpolation shown in the theorem is well-known for E L, but the proof is given to justify soundness of the procedure for interpolant computation described at the end of this section. Let us consider an example illustrating the main idea.
Example 2 Consider the TBox S = fA u B v C; A Dg, with A; B; C; D 2 Nc, the corresponding primitivization Tp = fX v C; A D; X A u Bg, and a normalization T of Tp. Denote = fD; Bg and let T be the \copy" of T under the injective renaming of all non- -symbols into fresh ones such that X and C are the \copies" of X and C in T , respectively. Then the entailment S n fA u B v Cg j= A u B D u B is equivalent to (T n fX v Cg) [ (T n fX v C g) j= X v X and there is a vertex and a subgraph in the enriched model of T [ T certifying this entailment (note the right-most vertex): Consider the vertex labelled with f (A) and X in the graph, denote it as v. It corresponds to the entailed inclusion X v A and is special, because it contains non- -symbols from T and T on the LHS and RHS, respectively, while all the descending vertices contain non- -symbols only from T . By the concept interpolation property of E L, there must be an interpolant -concept for the inclusion X v A (for the vertex v). In fact, this concept can be obtained from the LHS of the axiom labeling the child vertex of v, i.e. D is the required interpolant for v. To obtain the interpolant for the right-most vertex (corresponding to the inclusion X v X of interest) it su ces to take the conjunction of interpolants for the child vertices preceding the one labeled with A u B v X. We have B 2 and the concept D u B is the required interpolant.
The example shows that there are special intermediate derived concept inclusions in the proof for which an interpolant can be easily computed. It is either the LHS of the side condition of the rule under which the concept inclusion is obtained, or the concept from the RHS of one of the premises of the rule. In particular, such special concept inclusions are the very rst formulas in branches of the proof which are derived using axioms of both, a TBox T and its \copy". For the rest of the derived concept inclusions, the corresponding interpolants can be obtained by combining interpolants for preceding concept inclusions under conjunction and existential restriction. These are the main ideas presented in the proof of Theorem 3 and the procedure of interpolant computation.
Essentially, the proof demonstrates that in case an irregular formula ' is derived from T1 [T2 by an inference rule R, then either there are only regular formulas in the premise of R and the interpolant for ' can be computed immediately, or there are some irregular formulas in the premise for which the corresponding interpolants must be computed rst in order to obtain an interpolant for '. Practically, this means a recursive procedure of computing interpolants while traversing the proof of formula ' (i.e. a submodel starting with the plus-vertex corresponding to '). Every proof starts from axioms which are regular formulas, so the rst irregular formula in a branch of the proof is obtained after application of some rule R with regular premises. As noted in the proof of Theorem 3 (and Example 2), an interpolant in this case can be computed immediately, since it is either the concept from the LHS of the formula in the side condition of R, or the concept 9r:A1 from the RHS of the premise, if R = Ex. Thus, Theorem 3 (together with Theorem 1) evidences soundness of the recursive procedure given below, while termination follows from the niteness of the graph in an enriched model and the usage of ags for visited vertices. The procedure is de ned in words instead of pseudo-code for ease of exposition.
Procedure for computing an explicit de nition as concept interpolant Input: { an enriched model M = ( = ( +; ; E); ; ; f ) of the union of normal
TBoxes T1 [ T2, with sig (T1) \ sig (T2) = , for a signature ; { a concept inclusion A1 v A2, with Ai 2 (sig (Ti) \ Nc) n , for i = 1; 2. Output: Empty i T1 [ T2 6j= A1 v A2; otherwise, a concept interpolant D such that sig (D) and T1 [ T2 j= fA1 v D; D v A2g.
The procedure operates on the graph from M and incorporates a subrootine of graph traversal.
1. If there is no vertex v+ 2 + such that v+ 2 f (A2) and (v+) = A1, then the procedure terminates with the empty output. Otherwise, initiate graph traversal starting from the vertex v+ as follows.
+ 2. Initialize two maps vis : [ ! f0; 1g and int : +[ ! T erm( )[ fnullg for all vertices v of as: vis(v) = 0, int(v) = null. The map vis will be used to mark visited vertices and int will mark vertices with their corresponding interpolants. The value null will mean that there is no interpolant and vis(v) = 0 will imply int(v) = null. The task is compute the value of int(v+), which will not be equal to null, however it can be the case for other vertices in (which are related to proofs inside TBoxes T1, T2, but not from their union, i.e. to the proofs consisting of regular formulas).
3. The recursive subrootine of graph traversal and interpolant computation is as follows. Let v be the currently visited vertex from .
3.1. Let v 2 +. Then we visit an arbitrary vertex w such that (w; v) 2 E, i.e. a child minus-vertex:
If vis(w) = 1, we set int(v) = int(w); If vis(w) = 0, then we initiate recursively graph traversal starting from the vertex w. When the traversal is complete, we set int(v) = int(w).
After these steps, we set vis(v) = 1, i.e. visiting the vertex v is nished and we exit the recursion to one level up.
3.2. Let v 2 . Then we immediately set vis(v) = 1. Let (v) = F1 v F2. If for some i = 1; 2, we have sig (Fi) , then we set int(v) = Fi and exit the recursion to one level up.
Otherwise, initiate graph traversals recursively starting from every irregular (plus-vertex) w, with (w; v) 2 E. If there are no such vertices, then exit the recursion to one level up. Otherwise, when the traversal is complete for all such vertices w, we have int(w) 6= null and proceed as follows.
3.3. Consider di erent cases for the formula (v).
If (v) = A v B, or (v) = A v 9r:B, for some concept names A; B, then there is a single child plus-vertex w for v and we set int(v) = int(w). If (v) = A1 u:::uAn v B, n > 1, then let w1; ::; wn be the child plus-vertices for v, with wi 2 f (Ai) and A = (wi), for i = 1; ::n and a concept name A. Take the maximal subset I f1; ::; ng such that for every i 2 I, the vertex wi is irregular and set int(v) = iF2I int(wi) u jF2f1;::;ngnI Aj .
If (v) = 9r:A2 v B, then there is a child plus-vertex w such that w 2 f (r) and (v) = hA; A1i for some A and A1. If w is irregular, then set int(v) = int(w). Otherwise there is an irregular child vertex w, with w 2 f (A2), (w) = A1, and we set int(v) = 9r:int(w).
.
The de nition of the procedure is complete.
Let v be the minus-vertex from point 3.3 of the procedure and w be one of its child plus-vertices with an interpolant int(w) = D for some concept D. From the consideration of the formula (v), one can see that either the concept int(v) is the same as int(w), or can be of length increased by a constant (when (v) = 9r:A2 v B), or in the worst case, int(v) can be n-times longer than int(w) (if (v) = A1 u:::uAn v B, n > 1, and each corresponding child plus-vertex wi is irregular). This means that the size of the interpolant for the inclusion A1 v A2 is at worst O(nm), where m is the number of axioms in the normal TBox T1 [ T2 and n is the maximal number of conjuncts in an axiom of T1 [ T2. Note that due to arbitrary selection of the minus-vertex in point 3.1, the procedure computes an arbitrary chosen interpolant out of existing ones for the concept inclusion A1 v A2. By Theorem 1, it should be clear that point 3.1 can be easily modi ed to decide concept de nability wrt a subset S of the TBox: it su ces to consider only those child minus-vertices which are labeled with formulas corresponding to axioms of S. 5
The problem of partial reformulation of concepts under a TBox T wrt a
signature considered in the introduction implies several instances of the concept
de nability problem for di erent extensions of . At worst, the number of tests
for de nability to be performed is equal to the number of signature symbols in
a concept C of interest. Moreover, in the decomposition algorithm for E L [
We assume w.l.o.g. that the input TBox T is in the enriched normal form. Given T and , rst an enriched model M for T is built and then its \copy" M is generated wrt an injective renaming of all non- -symbols from T . The pair M; M is then kept as a precomputed template. As soon as an extension 0 of the signature is given, the graphs of these two models are expanded (with the iterative process of model construction described in the Appendix) wrt a set of formulas generated from T and the set 0 n . The idea of constructing this set of formulas is described in Example 3 and Theorem 2.
In the example below, we assume that we are given TBoxes T and T sharing a signature (initially taken to be empty for simplicity) and then is expanded as the result of substituting (or \gluing") some symbols of T with that of T . Example 3 Consider normal TBoxes T = fA v 9r1:A1g and T = f9s1:B1 v Bg, we have = sig (T ) \ sig (T ) = ?. Let T 0 = f9r1:A1 v Bg be the TBox obtained from T by substituting B1 with A1 and s1 with r1; we have 0 = sig (T ) \ sig (T 0) = fA1; r1g . Clearly, T \ T 0 j= A v B.
Now consider the TBox Q = T [T [fA1 B1g[T (s=r), where T (s=r) = f9r1:B1 v Bg, i.e. this TBox consists of the axiom of T with the role s1 substituted with r1. Then Q j= A v B and in fact, it will be shown in Theorem 2 that T [ T 0 and the theory Q constructed for the union T [ T in the way above entail the same normal formulas in signature sig (T [ T ). Therefore, an enriched model for checking entailment from the union of theories T [ T 0 (sharing the signature 0 ) can be obtained by expanding prebuilt models for T and T wrt the additional formulas fA1 B1g [ T (s=r).
We note that a much more general model-theoretic result implying Theorem 2 can be proved, but here we restrict ourselves only to the case important in the context of this paper.
Theorem 2 (Formulas imitate substitutions of signature symbols). Let T1 and T2 be normal TBoxes, = sig (T1) \ sig (T2), and let 1 = fAigi2I [ frjgj2J sig (T1) n , 2 = fBigi2I [ fsjgj2J sig (T2) n be signatures, where all Ai; Bi 2 Nc and rj; sj 2 Nr. Let T20 be the result of substituting every Bi with Ai and every sj with rj in the axioms of T2.
Consider the TBox Q = T1 [ T2 [ fAi Bigi2I [ T2(s=r), where T2(s=r) is the set of formulas of the form 9rj:X v Y , or X v 9rj:Y , j 2 J such that 9sj:X v Y , or X v 9sj:Y , respectively, is an axiom of T2. Then for any normal formula ' in signature sig (T1 [ T20) we have T1 [ T20 j= ' i Q j= '.
It should be clear that precomputing the models M; M does make sense,
when there is a large number of queries for partial concept reformulation to
be executed and answering all these queries would potentially involve all the
axioms of the TBox. In paticular, this is the case for the decomposition algorithm
from [
In the paper, we did not consider questions of e cient implementation of
enriched models and the algorithm of their construction. The iterative procedure
based on rules from Section 3 (including the initialization step) is mentioned to
simplify the exposition and is by no means proposed to be used in applications;
this topic is left out of the scope of this paper to separate the main concepts from
their implementation details. We note that the technique of enriched models can
be easily adopted for solving the problem of concept reformulation by using the
inference systems from the consequence-driven procedures for E L (see e.g. [
Since an enriched model of a TBox contains proofs of primitive concept
inclusions, it can be directly used for computing concept interpolants and hence,
explicit de nitions of concepts. For every proof of a concept inclusion C v C
from T [ T (where C and T are appropriate copies of C and T ), there is
a corresponding explicit de nition of C. It follows from the example on the
non-succinctness of uniform interpolants from Section 7 of [
Acknowledgments. The rst author was supported by the German Research Foundation within the Transregional Collaborative Research Centre SFB/TRR 62 \CompanionTechnology for Cognitive Technical Systems", the Russian Academy of Sciences (Grant No. 15/10), and the Siberian Division of the Russian Academy of Sciences (Integration Project No. 3). The second author was supported by the Russian Foundation for Basic Research (Grant No. 12-01-00460-a).
The de nition consists of two parts: the description of an enriched model as an algebraic structure and the description of the process of its construction. For convenience, we repeat here the algebraic part of the de nition.
By using the last restriction, we will sometimes abuse the notation and write f 1(v) to denote the preimage of the set V + with v 2 V .
Informally, the plus-vertices of the graph (i.e. the elements of +) will correspond to concept and role names and will be mapped by to concept names and pairs of concept names, respectively. The minus-vertices will correspond to axioms of T and tautologies. An enriched model M = (( +; ; E); ; ; f ) of a normal TBox T is built iteratively in accordance with a set of graph expansion rules which correspond to the inference rules from Figure 2. For every A 2 NcT , the graph is rst initialized with connected pairs of vertices hw1; y1i and hw2; y2i with w1; w2 2 and y1; y2 2 +, such that y1 2 f (A), (y1) = A, (w1) is a tautology of the form A v A and y2 2 f (>), (y2) = A, and (w2) is A v >. Besides, a pair hw; yi is initialized, with y 2 f (>), (y) = >, and (w) = > v >. This is the initialization step for the bipartite graph and the mappings ; ; f . To formulate the iterative construction process of M , we present it as a set of graph expansion rules, which describe how the bipartite graph should be expanded (and the mappings updated) based on the previously built vertices and an axiom from T encountered at an iteration step. Each rule has the form (m > 2): + and for all distinct (U1; V1); :::; (Um 1; Vm 1) (Um; Vm) ' where for i = 1; ::; m, Ui 2 Nc>(T ) [ NrT and Vi is either a symbol from Nc>(T ) or a pair of symbols from Nc>(T ), and ' is an axiom of T .
The rule is read as follows: { if there is an axiom ' in T { and for each (Ui; Vi), i = 1; ::; m xi 2 f (Vi) and (xi) = Ui
+ such that { if there does not exist a vertex y 2 + such that y 2 f (Vm) and (y) = Um, then initialize such vertex and { if there does not already exist a vertex w 2 , with (w) = ', such that hxi; wi 2 E for all i = 1; ::; m 1 and hw; yi 2 E, then initialize such vertex. The list of the graph expansion rules is presented in the gure below (n > 2 in the rule AndR ). Each rule is augmented with an illustration of the constructed part of the graph with the above mentioned vertices xi, w, and y, i = 1; ::; m 1.
(A;B) (T rans1) (A;C) B v C
(A;B) (T rans2) (r;hA;Ci) B v 9r:C (AndR ) (A;A1);:::; (A;An) (A;B)
A1 u ::: u An v B (Ex ) (r;hA;A1i); (A1;A2) (A;B)
9r:A2 v B The iterative procedure of model construction nishes when no rule results in an expansion of the graph, i.e. when no vertex or edge can be added. De nition 4 (Enriched model of a normal TBox). Let T be a normal TBox. The structure M = (( +; ; E); ; ; f ) built for T as above is called enriched model of T .
Let us formulate three auxiliary lemmas needed for the proof of Theorem 1. Note that in general, the bipartite graph ( +; ; E) may not have a tree-shape due to cycles caused e.g. by equalities between concept names (recall Example 1). However, there always exist submodels which are trees and these submodels are in one-to-one correspondence with proofs in the deductive system of Figure 2. Lemma 1 (Deterministic tree submodels correspond to proofs) Let M = ( = ( +; ; E); ; ; f ) be an enriched model of a TBox T . For any vertex v+ 2 +, there exists a deterministic submodel Ms = ( s = ( s+; s ; Es); s; s; fs), where s is a tree with the root v+ and each leaf is a vertex v 2 with
(v ) 2 T aut(NcT ). Let S = T n f (v ) j v 2 s g.
The submodel M(vs+)covrrefsp1o(nvd+s) t(oinancaisneference from T omitting S of the concept inclusion (v+) 2 Nc) and of the inclusion A v 9f 1(v+):B (in case (v+) = hA; Bi).
Proof. The claim is proved by induction on the number of iteration steps in the construction process of M for T which are needed to initialize the vertex v+. The base case is trivial by the initialization step for M : in this case the required tree is just a two-element chain corresponding to an inference of a tautology from T aut(NcT ). This inference trivially omits S. The induction step is simple as well, since at each iteration step of the graph expansion, by the induction hypothesis, for every plus-vertex in the premise of an expansion rule, there is a corresponding deterministic submodel, the part of the graph to be constructed has the form of a tree (Figure 3) and the intermediate vertex v to be constructed satis es (v ) 2 T . If the expansion rule applied is T ransi for some i = 1; 2, then the corresponding inference of the concept inclusion is by the rule T rans with the axiom in the side condition equal to (v ); the rest of the rules in Figure 3 are in direct correspondence to the rules from Figure 2.
Let us call proof submodel a submodel with the properties from Lemma 1 for some plus-vertex v+. As expected, the converse of the lemma holds as well. Lemma 2 (Proofs correspond to deterministic tree submodels) Let T be a normal TBox, M be an enriched model of T , and let ' be a formula of either of the forms A v B, A v 9r:B, for A; B 2 Nc. If there is an inference of ' from T which omits a subset S T , then there is a proof submodel of M with the root vertex v+ corresponding to ' and each non-leaf minus-vertex v satisfying (v ) 2 (T n S).
Thus, in the notations of the lemma, there is an inference of ' from T i there is a plus-vertex v+ 2 + in the enriched model of T such that v+ 2 f (B) and (v+) = A, or v+ 2 f (r) and (v+) = hA; Bi, depending on the form of '. By the construction of the enriched model, the vertex v+ in the graph is unique for ', so the number of plus-vertices in the model is at worst O(n2), where n in the size of the input TBox T . Every path of length 3 in the graph starting and ending in a plus-vertex has a minus-vertex in the middle (the graph is bipartite). Every minus-vertex is labeled with an axiom of T and, by the construction, the number of minus-vertices between two plus-vertices does not exceed the number of axioms in T (there can not exist two such minus-vertices v1; v2 with (v1) = (v2)). Thus, the size of the enriched model is polynomial in the size of T . Note that besides the information about all the entailed primitive concept inclusions, the enriched model contains information about all their possible inferences from axioms of T and tautologies T aut(NcT ), recall also the graphical representation of independent inferences from Example 1.
Lemma 3 (Checking for entailment with a normal TBox) Let T be a TBox, S T be a subset of axioms, and ' 2 T be an axiom. Let T ep = hTp; 0i be an extended primitivization of T and T en = hT norm; i be an extended fnor2maTlinzoartmionj o(f T) =ep.'Dg.enTohteenSwneorhmav=e Tf n S2 j=T n'or mi j T(no)rm2nSSgnoarnmdj='n'onrmorm=. Proof. For brevity we consider only the special case, when S = f'g and ' is of the form C1 C2 for some concepts C1; C2 62 Nc>. It follows that the set 'norm is not a singleton. Other cases, when S is an arbitrary subset of axioms, or ' is of the form C1 v C2, or Ci 2 Nc>, for some i = 1; 2, are considered analogously. Let 'p = A1 A2 be the primitive axiom of Tp such that 0('p) = ' and Ai Ci 2 Tp for i = 1; 2. Then, by the de nition of extended normalization, 'norm = fA1 v A2; A2 v A1g (with each of the concept inclusions mapped by to '). Consider the pair h(T n f'g)p; ~)i, where (T n f'g)p = Tp n (f'pg [ Si=1;2fAi Ci j Ci is not the LHS or RHS of an axiom of T n f'gg) and ~ is the restriction of the map 0 onto the set Tp n f'pg. Clearly, h(T n f'g)p; ~)i is an enriched primitivization of T n f'g and hence, its conservative extension. Moreover, any model of (T n f'g)p expands to a model of Tp n f'pg and thus, Tp n f'pg is a conservative extension of (T n f'g)p. Now consider the set T norm n 'norm. It is easy to see that this set is a normalization of Tp n f'pg and thus, its conservative extension.
()) : If T n f'g j= ', then (T n f'g)p j= C1 C2 and Tp n f'pg j= fC1 C2; A1 C2; A2 C2g. But then T norm n 'norm entails this set of formulas too and hence, T norm n 'norm j= 'norm.
(() : Assume that 'norm is entailed by T norm n 'norm. Then it is entailed by Tp n f'pg and, since Tp n f'pg j= fA1 C2; A2 C2g, we have Tp n f'pg j= '. As Tp n f'pg is a conservative extension of T n f'g, we conclude that T n f'g j= '. Theorem 1 (Entailment from subset of TBox in enriched model). Let T be a TBox and T ep = hTp; 0i be an extended primitivization of T . Let hT nornmor;mi. be an extended normalization of T ep and M be an enriched model of T Let C1; C2 be concepts appearing on the LHS or RHS of an axiom of T and for i = 1; 2, let Ai 2 sig (Tp) be a concept name which is either Ci (if Ci 2 Nc), or such that Ai 2 sig (Tp) n sig (T ) and Ai Ci 2 Tp. Then, for a subset S T of axioms, it holds T n S j= C1 v C2 i there is a proof submodel Ms = ( s = ( s+; s ; Es); s; s; fs) of M and a vertex v+ 2 s+ such that: { v+ 2 fs(A2) and s(v+) = A1, { for any non-leaf vertex v 2 s , ( s(v )) 62 S.
Proof. Let us denote ' = C1 v C2. If ' 2 T then, by the de nitions of extended primitivization and normalization, A1 v A2 2 T norm, (A1 v A2) = C1 v C2 and thus, by Lemma 3, the condition T n S j= C1 v C2 is equivalent to T norm n Snorm j= A1 v A2, where Snorm = f 2 T norm j ( ) 2 Sg. If ' 62 T an extended primitivization of Q and hT norm [ fAep1 =v hAT2pg[; fQAi1isvanA2egx;teQn0dieids then consider the TBox Q = T [ f'g. Clearly, Q anroermeqauliazlattioon oafndQep0, rweshpeercetivQel(yA,1onvthAe2r)es=t ofQ0t(hAe1ir vdoAm2a)in=s T'noarnmd anQ0d, TpQ. Observe that T n S j= ' is the same as Qnnor(mS [ f'g) j= ', which by Lemma 3 and the above noted is equivalent to (T [ fA1 v A2g) n P j= A1 v A2, swohtehree Plas=t efnta2ilmTennortmis[thfAe1savmAe2ags jT n(or)m2nSSn[orfm'gj=g. AW1evhaAve2.AT1hvereAfo2r2e, Pin, each of the two considered cases, the condition T n S j= C1 v C2 is equivalent to T norm n Snorm j= A1 v A2.
()) : If we have the entailment above, then there is an inference of A1 v A2 from T norm which omits Snorm. Then, by Lemma 2, there are the required proof submodel Ms and the vertex v+ 2 s+ such that for all non-leaf vertices v 2 we have s(v ) 62 Snorm and hence, ( s(v )) 62 S.
(() : Suppose there is a proof submodel Ms of M satisfying the conditions of the theorem. Then, by the de nition of Snorm and by Lemma 1, there is an inference of A1 v A2 from T norm which omits Snorm n T aut(NcT ), but then T norm n (Snorm n T aut(NcT )) j= A1 v A2 and (T norm n Snorm) [ (T norm \ T aut(NcT )) j= A1 v A2, hence T norm nSnorm j= A1 v A2 and we have (T norm [ fA1 v A2g) n P j= A1 v A2. By Lemma 3, this entailment is equivalent to Q n (S [ fC1 v C2g) j= C1 v C2 which is the same as T n S j= C1 v C2.
Example 2 shows that there are special intermediate derived concept inclusions in the proof for which an interpolant can be easily computed. It is either the LHS of the side condition of the rule under which the concept inclusion is obtained, or the concept from the RHS of one of the premises of the rule. In particular, such special concept inclusions are the very rst formulas in branches of the proof which are derived using axioms of both, a TBox T and its \copy". For the rest of the derived concept inclusions, the corresponding interpolants can be obtained by combining interpolants for preceding concept inclusions under conjunction and existential restriction. These are the main ideas presented in the proof of Theorem 3 and the procedure of interpolant computation from Section 4. Motivated by the observation on these \special" concept inclusions in proofs, we rst introduce the following auxiliary notion.
De nition 5 (Irregular formula, irregular vertex). Let T1 and T2 be normal TBoxes, with sig (T1) \ sig (T2) = for a signature . A formula ' is called regular (wrt T1; T2) if sig (') sig (Ti) for some i = 1; 2. Otherwise, it is called irregular. Let (( +; ; E); ; ; f ) be an enriched model of T1 [ T2. A vertex v+ 2 + is called irregular if { either (v) = A, v 2 f (B), for concept names A; B, and A v B is an irregular formula, { or (v) = hA; Bi, v 2 f (r), for concept names A; B, and A v 9r:B is an irregular formula.
The property of concept interpolation shown in the following theorem is wellknown for EL, but the proof is given to justify soundness of the procedure for interpolant computation described in Section 4.
Theorem 3 (Structural proof of concept interpolation). Let T1 and T2 be normal TBoxes, with sig (T1) \ sig (T2) = for a signature , and let A v F be a normal, but irregular formula such that A 2 sig (T1). If there is an inference of A v F from T1 [ T2, then there is a concept interpolant D such that T1 [ T2 j= fA v D; D v F g and sig (D) .
Proof. We apply induction on the length of the inference of A v F from T1 [ T2. Observe that by the form of the rules in Figure 1, we must have F 2 sub (T1 [ T2) and thus, sig (F ) sig (T2), since A v F is irregular and A 2 sig (T1). Induction step (the base case is trivial): let R be the corresponding derivation rule. Note that the formula in the side condition of R is regular and assume that all the formulas in the premise are regular too. If R is T rans, then we conclude that B is the required interpolant; if R is AndR, then A1 u ::: u An is; if R is Ex, then either fA; r; A1; A2g sig (T1) and thus, 9r:A2 is the required interpolant, or fA1; r; A2; Bg sig (T2), and hence, 9r:A1 is.
Now assume there is an irregular formula in the premise of R. By the induction hypothesis, there is a corresponding interpolant for this formula. If R is T rans, then it is the required interpolant for A v F . If R is AndR, then consider the maximal subset I f1; ::; ng such that for every i 2 I the formula A v Ai is irregular and Di is the corresponding interpolant. Since A v F is irregular, we conclude that Aj 2 for all j 2 f1; ::; ng n I and therefore, iF2I Di u jF2f1;::;ngnI Aj is the required interpolant. Finally, if R is Ex then, in case A v 9r:A1 is irregular, its interpolant is the required interpolant for A v F . Now assume that A v 9r:A1 is a regular formula and A1 v A2 is irregular with an interpolant D. Then r 2 and 9r:D is the required interpolant for A v F .
Theorem 2 (Formulas imitate substitutions of signature symbols) Let T1 and T2 be normal TBoxes, = sig (T1) \ sig (T2), and let 1 = fAigi2I [ frjgj2J sig (T1) n , 2 = fBigi2I [ fsjgj2J sig (T2) n be signatures, where all Ai; Bi 2 Nc and rj; sj 2 Nr. Let T20 be the result of substituting every Bi with Ai and every sj with rj in the axioms of T2.
Consider the TBox Q = T1 [ T2 [ fAi Bigi2I [ T2(s=r), where T2(s=r) is the set of formulas of the form 9rj:X v Y , or X v 9rj:Y , j 2 J such that 9sj:X v Y , or X v 9sj:Y , respectively, is an axiom of T2. Then for any normal formula ' in signature sig (T1 [ T20) we have T1 [ T20 j= ' i Q j= '. Proof. ()): We show that Q is a conservative extension of T1 [ T20. By the de nition of Q it su ces to verify that Q j= T20 n T2. Let 2 T20 n T2, this is a formula obtained from an axiom 2 T2 by substituting Bi with Ai and sj with rj for i 2 I, j 2 J . Let fAk; : : : ; Alg = sig ( ) \ 1 \ Nc (a possibly empty set). Consider several possible cases for the signature of . If sig ( ) \ frjgj2J = ?, then [ fAi Bigi2fk;:::;lg j= , so we have Q j= , because 2 T2 Q. If there is a role rj 2 sig ( ) for some j 2 J , then there must be a formula 2 T2(s=r) such that either j= (in case sig ( )\ 1 \Nc = ?), or f g[fAi Bigi2fk;:::;lg j= . In each of the cases we have Q j= .
((): Let Q0 be the TBox obtained from T1[T2[T2(s=r) by substituting every occurrence of symbol Bi with Ai, for i 2 I. We have Q j= ' i Q0 j= ', since Q j= Q0, every model of Q0 expands to a model of Q, and sig (') sig (Q0). Observe that any formula 9rj:X v Y , or X v 9rj:Y from a \copy" of T2(s=r) obtained after this substitution, is a formula of T20. Therefore, T1 [ T20 Q0 and the set di erence D = Q0n(T1[T20) consists of formulas of the form 9sj:X v Y , or X v 9sj:Y , with X; Y 2 sig (T20), j 2 J , such that there exists a corresponding axiom 9rj:X v Y , or X v 9rj:Y in T20. We now prove by induction that for an inference of a (normal) formula ' from Q0, with sig (') sig (T1 [ T20), there is a corresponding inference of ' from T1 [ T20. Induction step (the base case is trivial): if ' is obtained by AndR or T rans, then by the form of formulas in D, the axiom in the side condition can not belong to D and thus there is nothing to prove. If the rule is Ex with an axiom 9sj:Y 0 v Z 2 D in the side condition, then there are formulas of the form X v 9sj:Y 2 D and Y v Y 0 in the premise. The formula Y v Y 0 is normal and Y; Y 0 2 sig (T20), thus by the induction hypothesis, there exists an inference of Y v Y 0 from T1 [ T20. Since there are corresponding formulas 9rj:Y 0 v Z and X v 9rj:Y in T20, we conclude that there is an inference of ' from T1 [ T20 in which ' is obtained by Ex from formulas X v 9rj:Y , Y v Y 0 and X v 9rj:Y is obtained by T rans from the tautology X v X.