Merging multi-sourced ontologies in a consistent manner is an important and challenging research topic. In this paper, we propose a novel approach for merging DL-LitebNool ontologies by adapting the classical model-based belief merging approach, where the minimality of changes is realised via a semantic notion, model distance. Instead of using classical DL models, which may be in nite structures in general, we de ne our merging operator based on a new semantic characterisation for DL-Lite. We show that subclass relation w.r.t. the result of merging can be checked e ciently via a QBF reduction. We present our system OntoMerge, which e ectively answers subclass queries on the resulting ontology of merging, without rst computing the merging results. Our system can be used for answering subclass queries on multiple ontologies.
Ontologies are widely used for sharing and reasoning over domain knowledge,
and their underlying formalisms are often description logics (DLs). To e
ectively answer queries, ontologies from heterogeneous sources and contributed
by various authors are often needed. However, ontologies developed by multiple
authors under di erent settings may contain overlapping, con icting and
incoherent domain knowledge. The ultimate goal of ontology merging is to obtain
a single consistent ontology that preserves as much knowledge as possible from
two or more heterogeneous ontologies. This is in contrast to ontology matching
[
Existing merging systems often adopt formula-based approaches to deal with
logical inconsistencies [10; 9; 14]. Most of such approaches can be described as
follows: the system rst combine the ontologies by taking their union; then, if any
inconsistency is detected (through a standard reasoning), it pinpoints the axioms
which (may) cause inconsistency; and nally, remove certain axioms to retain
consistency. However, such an approach is sometimes unsatisfactory because it
is not ne-grained either in the way it measures the minimality of changes, and
thus it is often unclear how close the result of merging is to the source ontologies
semantically; or in the way it resolve inconsistency. In [
On the other hand, model-based merging operators have been intensively
studied in propositional logic, which are syntax-independent and usually satisfy
more rationality postulates than formula-based ones. However, a major
challenge in adapting model-based merging techniques to DLs is that DL models
are generally in nite structures and the number of models of a DL ontology is
in nite. Several notions of model distance are de ned on classical DL models
for ontology revision [
In this paper, we focus on merging ontologies expressed as DL-Lite TBoxes,
which can be also accompanied with the ontology-based data access (OBDA)
framework for data integration [
[
Formally, given a signature S, a DL-LitebNool language has the following syntax R
P j P
S
P j :P
B > j A j > n R C B j :C j C1 u C2 where n 2 SN , A 2 SC and P 2 SR. B is called a basic concept and C is called a general concept. BS denotes the set of basic concepts on S. We write ? for :>, 9R for 1 R, and C1 t C2 for :(:C1 u :C2). Let R+ = P , where P 2 SR, whenever R = P or R = P . A TBox T is a nite set of concept axioms of the form C1 v C2, where C1 and C2 are general concepts. An ABox A is a nite set of membership assertions of the form C(a) or S(a; b), where a; b are individual names. In this paper, an ontology is represented as a DL TBox.
The classical DL semantics are given by models. A TBox T is consistent with an ABox A if T [ A has at least one model. A concept or role is satis able in T if it has a non-empty interpretation in some model of T . A TBox T is coherent if all atomic concepts and atomic roles in T are satis able. Note that a coherent TBox must be consistent. TBox T entails an axiom C v D, written T j= C v D, if all models of T satisfy C v D. Two TBoxes T1; T2 are equivalent, written T1 T2, if they have the same models.
Now, we introduce a semantic characterisation for DL-Lite TBoxes in terms of types. A type BS is a set of basic concepts over S, such that > 2 , and > n R 2 implies > m R 2 for each pair m; n 2 SN with m < n and each (inverse) role R 2 SR [ f P j P 2 SR g. Type satis es basic concept B if B 2 , :C if does not satisfy C, and C1 u C2 if satis es both C1 and C2. Given a TBox T , type satis es T if satis es concept :C1 t C2 for each axiom C1 v C2 in T .
For a TBox T , de ne TM(T ) to be the maximal set of types satisfying the following conditions: (1) all the types in TM(T ) satisfy T ; (2) for each type 2 TM(T ) and each 9R in , there exists a type 0 2 TM(T ) (possibly 0 = ) containing 9R . A type is called a type model (T-model) of T if 2 TM(T ). Note that TM(T ) is uniquely de ned for each TBox T . Note that for a coherent TBox T , TM(T ) is exactly the set of all types satisfying T . Let TM( ) = TM(T1) TM(Tn) for = hT1; : : : ; Tni.
Proposition 1. Given a TBox T , we have the following results: { T is consistent i TM(T ) 6= ;. { For a general concept C, C is satis able wrt T i there exists a T-model in
TM(T ) satisfying C. { For two general concepts C; D, T j= C v D i either TM(T ) = ; or all
T-models in TM(T ) satisfy C v D. { T T 0 i TM(T ) = TM(T 0), for any TBox T 0.
Given a type , an individual a and an ABox A, we say is a type of a w.r.t. A if there is a model I of A such that = fB j aI 2 BI ; B 2 BS g. For example, given A = fA(a); :B(b); C(c)g, type = fA; Bg is a type of a, but not a type of either b or c in A. For convenience, we will say a type of a when the ABox A is clear from the context. Let TMa(A) be the set of all the types of a in A if a occurs in A; and otherwise, TMa(A) be the set of all the types. A set M of T-models satis es an ABox A if there is a type of a in M , i.e., M \ TMa(A) 6= ;, for each individual a in A.
Proposition 2. Given a TBox T and an ABox A, T [ A is consistent i TM(T ) \ TMa(A) 6= ; for each a in A. 3
In this section, we introduce an approach to merging DL-Lite ontologies to obtain a coherent uni ed ontology.
An ontology pro le is of the form = hT1; : : : ; Tni, where Ti is the ontology
from the source n.o. i (1 i n). There are two standard de nitions of integrity
constraints (ICs) in the classical belief change literature [
In classical model-based merging approaches, merging operators are often
de ned by certain notions of model distances [11; 6]. We use S4S0 to denote the
symmetric di erence between two sets S and S0, i.e., S4S0 = (S n S0) [ (S0 n S).
Given a set S and a tuple S = hS1; : : : ; Sni of sets, the distance between S and
S is de ned to be a tuple d(S; S) = hS4S1; : : : ; S4Sni: For two n-element
distances d and d0, d d0 if di d0i for each 1 i n, where di is the i-th element
in d. Given two sets S and S0, de ne (S; S0) = S if S0 is empty, and otherwise,
(S; S0) = f e0 2 S j 9e00 2 S0 s.t. 8e 2 S; 8e0 2 S0; d(e; e0) 6 d(e0; e00) g: In [
Inspired by classical model-based merging, we introduce a merging operator in terms of T-models. For an ontology pro le and an EC Te, we could de ne the T-models of the merging to be a subset of TM(Te) (so that Te is entailed) consisting of those T-models which have minimal distance to , i.e., (TM(Te); TM( )). However, this straightforward adoption does not take the CC into consideration, and the merging result obtained in this way may not be coherent. For example, let T1 = fA v :Bg, T2 = f> v Bg, Te = ;, and Ac = fA(a); B(a)g. Then, (TM(Te); TM(hT1; T2i)) consists of only one type fBg. Clearly, the corresponding TBox fA v ?; > v Bg does not satisfy the CC, and it is not coherent.
Note that in the above example, once the merging result satis es the CC, then it is also coherent, because both concepts A and B are satis able. In general, it is also the case that coherency can be achieved by applying certain CC to merging. We introduce an auxiliary ABox Ay in addition to the initial CC Ac, in which each concept and each role is explicitly asserted with a member. That is, Ay = fA(a) j A 2 SC ; a 2 SI is a fresh individual for Ag [ fP (b; c) j P 2 SR; b; c 2 SI are fresh individuals for P g: As assumed, SI is large enough for us to take these auxiliary individuals. From the de nition of CCs, the merged TBox T must be consistent with all the assertions in Ay, which assures all the concepts and roles in T to be satis able. Based on this observation, we have the following lemma.
To ensure the coherence of merging, we only need to include Ay into the CC.
For the merging to be consistent with the CC Ac, from Proposition 2, the T-model set M of the merging needs to satisfy Ac. That is, M needs to contain a type of a for each individual a in Ac. However, (TM(Te); TM( )) does not necessarily satisfy this condition, as can be seen from the above example: TMa(Ac) consists of a single type fA; Bg and (TM(Te); TM( )) \ TMa(Ac) = ;. Intuitively, for the merging to satisfy the CC, type fA; Bg need to be added to the T-models of merging. In general, the T-models of merging can be obtained by extending (if necessary) the set (TM(Te); TM( )) with at least one type of a w.r.t. Ac for each individual a in Ac, and if there are multiple such types, choose those with minimal distances.
Based on the above intuitions, the de nition of TBox merging is presented as follows.
De nition 1. Let be an ontology pro le, Te be a TBox, and Ac be an ABox. Denote A = Ac [ Ay. The result of merging w.r.t. the EC Te and the CC Ac, denoted r( ; Te; Ac), is de ned as follows
TM(r( ; Te; Ac)) = (TM(Te); TM( ))[ [
(TM(Te) \ TMa(A ); TM( )): From the de nition, the T-models of the merging are constituted with two parts. The rst part consists of those T-models of Te (for the satisfaction of the EC) with minimal distances to . The second part consists of types of a, for each individual a in A , which are added to the rst part for the satisfaction of the CC. These types are also required to be T-models of Te and have minimal distances to . It is clear from Proposition 1 that the result of merging is unique up to TBox equivalence. 4
In this section, we consider a standard reasoning problem for ontology
merging, namely the subclass queries : whether or not the result of merging entails a
subclass relation C v D. We present a QBF reduction for this problem, which
allows us to make use of the o -the-shelf QBF solvers [
We achieve the reduction in three steps. Firstly, we introduce a novel
propositional transformation for DL-Lite TBoxes. The transformation is inspired by [
Function ( ) maps a basic concept to a propositional variable, and a general concept (resp., a TBox axiom) to a propositional formula.
(?) = ?; (:C) = : (C); (C1 v C2) = (C1) !
(C2): (A) = pA; (> n R) = pnR; (C1 u C2) = (C1) ^ (C2); Here, pA and pnR are propositional variables. We use VS to denote the set of propositional variables corresponding to the basic concepts over S, and we omit the subscript S in what follows for simplicity. We can see that ( ) is a bijective mapping between the set of DL-LitebNool general concepts and the set of propositional formulas only referring to symbols in VS and boolean operators :, ^ and !.
Naturally, given the mapping ( ), an arbitrary propositional model may not correspond to a type. We de ne a formula whose models are exactly the set of types. Let = ^
^ R+2SR and m<k<n for no k2SN m;n2SN with m<n pnR ! pmR: Then, mod( ) = f ( ) j is a typeg where (S) stands for for f (B1) j B 2 Sg for a set S of basic concepts.
Given a coherent DL-Lite TBox T , let (T ) = V 2T ( ) ^ : The models of (T ) correspond to the T-models of T . For a DL-Lite ABox A and an individual name a in A, let a(A) =
^ C(a)2A (C) ^
^ (puP ^ pvP ) P 2SR where u and v are respectively, the maximal number in SN s.t. u jfbi j P (a; bi) 2 Agj and v jfbi j P (bi; a) 2 Agj. Note that we are not transforming an ABox into a propositional theory, but using the encodings a(A) as constraints over the models.
It is worth noting that the sizes of (T ) and (a; A) are both polynomial in the size of T [ A. The intuition behind (T ) and (a; A) can be shown by the following lemma.
Lemma 2. Given a coherent TBox T and an ABox A, then, 1. mod( (T )) = f ( ) j 2 TM(T )g; 2. mod( a(A) ^ ) = f ( ) j 2 TMa(A)g.
This transformation essentially allows us to build a connection between our merging operator and propositional belief merging.
Secondly, as we have a transformation from T-models to propositional
models, we can encode (minimal) distances between them using QBFs, by extending
the encoding in [
F ( ; h'1; : : : ; 'ni) = ^
^ 1 i n
i 'i ^ ^ (p $ :pi) ! pid
: p2V A model M of F ( ; h'1; : : : ; 'ni) consists of the assignments to three sets of variables V , V N and VdN . For a set S V [ V N [ VdN , m(S) is the set obtained from S by eliminating the super- and subscripts. Then, M \ V is a model of , and m(M \V i) is a model of 'i. From (p $ :pi) ! pid, m(M \Vdi) subsumes the symmetric di erence between the former two models. We use ! instead of $ here, as we will further constraint the assignments of VdN to minimal distances.
Furthermore, de ne a QBF D( ; h'1; : : : ; 'ni) =(9V 9V N F ( ; h'1; : : : ; 'ni)) ^ ^
pid ! :9V 9V N F ( ; h'1; : : : ; 'ni) ^ (p $ pi) ; 1p2iV n where 9V with V = fp1; : : : ; pkg is an abbreviation for 9p1 : : : 9pk. A model Md of D( ; h'1; : : : ; 'ni) is an assignment to VdN representing a minimal distance between the models of and the model tuples of h'1; : : : ; 'ni. The rst conjunct of D( ; h'1; : : : ; 'ni) says that there is a model of and a model tuple of h'1; : : : ; 'ni such that the distance between them is subsumed by m(Md). The second conjunct checks that m(Md) is minimal, i.e., there is no distance properly subsumed by m(Md).
Lemma 3. Given propositional formulas and '1; : : : ; 'n, let M D( ; h'1; : : : ; 'ni) be the set of minimal distances (w.r.t. ) between and h'1; : : : ; 'ni (of the form hM 4M1; : : : ; M 4Mni with M 2 mod( ) and Mi 2 mod('i)). Then, mod(D( ; h'1; : : : ; 'ni)) = fMd
V N
d j 9d 2 M D( ; h'1; : : : ; 'ni) s.t. m(Md \ Vdi) = di for each 1 i ng:
Finally, with the encoding of minimal distances, we can encode the T-models of the merging and we are ready to encode the entailment relation. Given an ontology pro le = hT1; : : : ; Tni and a TBox Te, all the types in (TM(Te); TM( )) satisfy TBox axiom if and only if QBF :9VdN E( ; Te; ) evaluates to true, with
E( ; Te; ) = D( (Te); h (T1); : : : ; (Tn)i) ^ :8V
9V N F ( (Te); h (T1); : : : ; (Tn)i) ! ( ) : This QBF can be understood as follows. A model M of E( ; Te; ) is an assignment to VdN , and represents, by the rst conjunct of E( ; Te; ), a minimal distance between the T-models of Te and the T-model tuples of . The second conjunct states the non-entailment, that is, not all of the T-models of Te having such a distance satisfy . The QBF as a whole essentially says that there does not exists a minimal distance d such that a type (in (TM(Te); TM( ))) selected with d fails to satisfy . Similarly, given an ABox A and an individual a in A, all the types in (TM(Te) \ TMa(A); TM( )) satisfy i QBF :9VdN Ea( ; Te; A; ) evaluates to true, where Ea( ; Te; A; ) is obtained from E( ; Te; ) by replacing (Te) with (Te) ^ a(A).
Now, we can reduce the subclass query answering for TBox merging to QBF as follows.
Theorem 1. Let be an ontology pro le with coherent source TBoxes, Te be a TBox and Ac be an ABox in DL-LitebNool. Let A = Ac [ Ay. Given a TBox axiom , we have r( ; Te; Ac) j= i the following QBF evaluates to true _ We have implemented the algorithm for answering subclass queries in ontology merging, called OntoMerge, and it is publicly available for test at http: //www.ict.griffith.edu.au/~kewen/OntoMerge/. The ultimate goal of our system OntoMerge is to transform the entailment over merged ontologies to the validity of QBFs as given in Eq.(1). If the input ontologies are T1; : : : ; Tn and the query is , then the corresponding QBF can be split into two parts: one is the formula E( ; Te; ), and the other is a disjunction of formulas of the form Ea( ; Te; A ; ). The size of the rst part is only determined by the sizes of the input ontologies, the input EC and the query , and the size of is often small compared to the ontologies. In the second part of the resulting QBF, the number of disjuncts is essentially determined by the number of unsatis able concepts in the union of input ontologies (as will be explained later) and the input CC. Thus, the number of unsatis able concepts plays a crucial role in the complexity of the reduction algorithm.
In OntoMerge, we rst check whether the given ontologies can be simply
jointed without causing any incoherency using an o -the-shelf DL reasoner
(HermiT [
Once the QBF is generated, a publicly available program is used to convert it from QBF 1.0 format to QDIMACS format6 or ISCAS format7 and then an e cient QBF solver is used to decide the validity of the QBF. 6
To test the e ciency of OntoMerge, we used the DL-LitebNool fragment of the medical ontology Galen8, which is of medium size. Our experimental results show that the system is relatively e cient, while further optimization is still under way. Speci cally, various randomly modi ed fragments of Galen were merged using OntoMerge and the following three types of experiments were conducted: { Fixed total number of axioms in the input ontologies but varied number of unsatis able concepts. { Fixed total number of unsatis able concepts but varied total number of axioms in the input ontologies. { Fixed number of unsatis able concepts but varied total number of input ontology axioms.
A PC with Intel Core 2 Duo E8400, 4GB RAM, running Linux Mint 13
64bit, and CirQit QBF solver [
7 http://logic.pdmi.ras.ru/~basolver/rtl.html 8 http://www.co-ode.org/galen/ gure we can see that the program is quite fast according to the time used for generating the QBF and the time used for deciding the validity of the QBF. This is because when the number of unsatis able concepts increases, the size of the QBF generated increases linearly. However, when the number of unsatis able concepts is over 18, OntoMerge can still generate the QBF but the QBF solver is unable to decide the validity of such a QBF.
In the second set of tests, we xed the number of unsatis able concepts to 1 but increased the total number of axioms from 26 to 174. Figure 3 shows that when the number of axioms is increased, the time cost for generating QBF increases faster than in the rst set of tests. This is partly due to the fact that with the increase of the total axioms, the size of the QBF signi cantly increases too. Similar to the case for the rst set of tests, when the total number of axioms is over 174, the QBF solver fails again.
In the third set of tests, we x the ratio of total number of axioms to the number of unsatis able concepts to around 0:15 but let the total number of axioms varied from 26 to 92 as well as the number of unsatis able concepts. Figure 4 shows a similar pattern to Figure 3. When the total number of axioms is over 92, the QBF solver failed to return an answer.
We have developed a novel approach for merging ontologies in DL-Lite, in terms of types instead of classical DL models. We have also presented algorithms to reduce subclass queries of DL-Lite merging to the evaluation of QBFs and thus provided a novel way of reasoning with the result of ontology merging using e cient QBF solvers. We have implemented a preliminary merging system OntoMerge, and reported some experimental results in the paper. Currently we are extending the approach in two directions: (1) merging DL-Lite ontologies with both TBoxes and ABoxes, and (2) merging ontologies in expressive DLs.
Acknowledgement: We would like to thank the three anonymous referees for their helpful comments. Special thanks to Rodney Topor for various discussions with him. Kewen Wang was partially supported by the ARC grants DP1093652 and DP110101042. Guilin Qi was partially supported by the NSFC grant 61272378.