=Paper=
{{Paper
|id=None
|storemode=property
|title=OntoMerge: A System for Merging DL-Lite Ontologies
|pdfUrl=https://ceur-ws.org/Vol-969/paper2.pdf
|volume=Vol-969
}}
==OntoMerge: A System for Merging DL-Lite Ontologies==
<pdf width="1500px">https://ceur-ws.org/Vol-969/paper2.pdf</pdf>
<pre>
    OntoMerge: A System for Merging DL-Lite
                  Ontologies

            Zhe Wang1 , Kewen Wang2 , Yifan Jin2 , and Guilin Qi3,4
                      1
                       University of Oxford, United Kingdom
                         2
                            Griffith University, Australia
                          3
                            Southeast University, China
              4
                State Key Laboratory for Novel Software Technology
                       Nanjing University, Nanjing, China



      Abstract. 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-LiteN    bool 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 infinite structures in general, we
      define 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 efficiently via a QBF reduction. We present our system
      OntoMerge, which effectively answers subclass queries on the resulting
      ontology of merging, without first computing the merging results. Our
      system can be used for answering subclass queries on multiple ontologies.


1   Introduction
Ontologies are widely used for sharing and reasoning over domain knowledge,
and their underlying formalisms are often description logics (DLs). To effec-
tively answer queries, ontologies from heterogeneous sources and contributed
by various authors are often needed. However, ontologies developed by multiple
authors under different settings may contain overlapping, conflicting and inco-
herent 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
[5], whose goal is to align entities (with different name) between ontologies, and
which is often a pre-stage of ontology merging.
     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 first 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 finally, remove certain axioms to retain
consistency. However, such an approach is sometimes unsatisfactory because it
is not fine-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 [12], an attempt is made
to provide some semantic justification for the minimality of changes, however,
the result of merging is still syntax-dependant and is often a set of ontologies.
    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 chal-
lenge in adapting model-based merging techniques to DLs is that DL models
are generally infinite structures and the number of models of a DL ontology is
infinite. Several notions of model distance are defined on classical DL models
for ontology revision [13]. Mathematically, it is possible to define a distance o
classical DL models. Such a distance is computationally limited as it is unclear
how to develop an algorithm for the resulting merging operator. A desirable so-
lution is to define ontology merging operators based on a suitable finite semantic
characterisation instead of classical DL models.
    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 [2]. We propose a novel approach for merging
ontologies by adapting a 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 infinite structures in general,
we define our merging operator based on the notion of types. We show that
subclass relation w.r.t. the result of merging can be checked efficiently via a
QBF reduction, which allows us to make use of the off-the-shelf QBF solvers [8].
We present our system OntoMerge, which effectively answers subclass queries
on merging results, without first computing the merging results. Our system can
be used to answer subclass queries on multiple ontologies.

2   A New Semantic Characterisation
In our approach, it is sufficient to consider a finite yet large enough signature.
A signature S is a union of four disjoint finite sets SC , SR , SI and SN , where
SC is the set of atomic concepts, SR is the set of atomic roles, SI is the set of
individual names and SN is the set of natural numbers in S. We assume 1 is
always in SN .
     Formally, given a signature S, a DL-LiteN
                                             bool language has the following syntax
[1]:
     R ← P | P−               S ← P | ¬P
     B←>|A| >nR               C ← B | ¬C | C1 u C2
where n ∈ SN , A ∈ SC and P ∈ 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
¬>, ∃R for ≥ 1 R, and C1 t C2 for ¬(¬C1 u ¬C2 ). Let R+ = P , where P ∈ SR ,
whenever R = P or R = P − . A TBox T is a finite set of concept axioms of the
form C1 v C2 , where C1 and C2 are general concepts. An ABox A is a finite 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 satisfiable
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 satisfiable. Note that
a coherent TBox must be consistent. TBox T entails an axiom C v D, written
T |= 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 > ∈ τ , and
> n R ∈ τ implies > m R ∈ τ for each pair m, n ∈ SN with m < n and each
(inverse) role R ∈ SR ∪ { P − | P ∈ SR }. Type τ satisfies basic concept B if
B ∈ τ , ¬C if τ does not satisfy C, and C1 u C2 if τ satisfies both C1 and C2 .
Given a TBox T , type τ satisfies T if τ satisfies concept ¬C1 t C2 for each axiom
C1 v C2 in T .
    For a TBox T , define 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 τ ∈ TM(T ) and each ∃R in τ , there exists a type τ 0 ∈ TM(T ) (possibly
τ 0 = τ ) containing ∃R− . A type τ is called a type model (T-model) of T if
τ ∈ TM(T ). Note that TM(T ) is uniquely defined 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 , . . . , Tn i.

Proposition 1. Given a TBox T , we have the following results:
 – T is consistent iff TM(T ) 6= ∅.
 – For a general concept C, C is satisfiable wrt T iff there exists a T-model in
   TM(T ) satisfying C.
 – For two general concepts C, D, T |= C v D iff either TM(T ) = ∅ or all
   T-models in TM(T ) satisfy C v D.
 – T ≡ T 0 iff 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 τ = {B | aI ∈ B I , B ∈ BS }. For
example, given A = {A(a), ¬B(b), C(c)}, type τ = {A, B} 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 satisfies 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 iff
TM(T ) ∩ TMa (A) 6= ∅ for each a in A.


3   Merging Operator
In this section, we introduce an approach to merging DL-Lite ontologies to obtain
a coherent unified ontology.
    An ontology profile is of the form Π = hT1 , . . . , Tn i, where Ti is the ontology
from the source n.o. i (1 ≤ i ≤ n). There are two standard definitions of integrity
constraints (ICs) in the classical belief change literature [3], the consistency-
and entailment-based definitions. We also allow two types of ICs for merging,
namely the consistency constraint (CC), expressed as a set Ac of data, and the
entailment constraint (EC), expressed as a TBox Te . We assume the IC is self-
consistent, that is, Te ∪ Ac is always consistent. For an ontology profile Π, a
CC Ac and a EC Te , an ontology merging operator is a mapping (Π, Te , Ac ) 7→
∇(Π, Te , Ac ), where ∇(Π, Te , Ac ) is a TBox, s.t. ∇(Π, Te , Ac )∪Ac is consistent,
and ∇(Π, Te , Ac ) |= Te .
    In classical model-based merging approaches, merging operators are often
defined by certain notions of model distances [11; 6]. We use S4S 0 to denote the
symmetric difference between two sets S and S 0 , i.e., S4S 0 = (S \ S 0 ) ∪ (S 0 \ S).
Given a set S and a tuple S = hS1 , . . . , Sn i of sets, the distance between S and
S is defined to be a tuple d(S, S) = hS4S1 , . . . , S4Sn i. For two n-element dis-
tances 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 S 0 , define σ(S, S 0 ) = S if S 0 is empty, and otherwise,
σ(S, S 0 ) = { e0 ∈ S | ∃e00 ∈ S 0 s.t. ∀e ∈ S, ∀e0 ∈ S 0 , d(e, e0 ) 6≺ d(e0 , e00 ) }. In [6],
given a collection Ψ = {ϕ1 , . . . , ϕn } of propositional formulas, and some ECs
expressed as a propositional theory µ, the result of merging ϕ1 , . . . , ϕn w.r.t. µ
is the theory whose models are exactly σ(mod(µ), mod(Ψ )), i.e., those models
satisfying µ and having minimal distance to Ψ .
    Inspired by classical model-based merging, we introduce a merging opera-
tor in terms of T-models. For an ontology profile Π and an EC Te , we could
define 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 = {A v ¬B}, T2 = {> v B}, Te = ∅, and
Ac = {A(a), B(a)}. Then, σ(TM(Te ), TM(hT1 , T2 i)) consists of only one type
{B}. Clearly, the corresponding TBox {A v ⊥, > v B} does not satisfy the CC,
and it is not coherent.
    Note that in the above example, once the merging result satisfies the CC, then
it is also coherent, because both concepts A and B are satisfiable. In general,
it is also the case that coherency can be achieved by applying certain CC to
merging. We introduce an auxiliary ABox A† in addition to the initial CC Ac ,
in which each concept and each role is explicitly asserted with a member. That
is, A† = {A(a) | A ∈ SC , a ∈ SI is a fresh individual for A} ∪ {P (b, c) | P ∈
SR , b, c ∈ SI are fresh individuals for P }. As assumed, SI is large enough for
us to take these auxiliary individuals. From the definition of CCs, the merged
TBox T must be consistent with all the assertions in A† , which assures all the
concepts and roles in T to be satisfiable. Based on this observation, we have the
following lemma.
Lemma 1. T is coherent iff T ∪ A† is consistent for any TBox T .
To ensure the coherence of merging, we only need to include A† 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 nec-
essarily satisfy this condition, as can be seen from the above example: TMa (Ac )
consists of a single type {A, B} and σ(TM(Te ), TM(Π)) ∩ TMa (Ac ) = ∅. Intu-
itively, for the merging to satisfy the CC, type {A, B} 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 definition of TBox merging is presented
as follows.

Definition 1. Let Π be an ontology profile, Te be a TBox, and Ac be an ABox.
Denote A∗ = Ac ∪ A† . The result of merging Π w.r.t. the EC Te and the CC
Ac , denoted ∇(Π, Te , Ac ), is defined as follows

               TM(∇(Π, Te , Ac )) = σ(TM(Te ), TM(Π))∪
                       [
                                 σ(TM(Te ) ∩ TMa (A∗ ), TM(Π)).
                      a occurs in A∗


From the definition, the T-models of the merging are constituted with two parts.
The first 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 first 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    QBF Reduction

In this section, we consider a standard reasoning problem for ontology merg-
ing, 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 off-the-shelf QBF solvers [8]. We assume that every
TBox in the ontology profile is coherent, and in this case, the T-models of a
TBox T are exactly those satisfying T .
    We achieve the reduction in three steps. Firstly, we introduce a novel proposi-
tional transformation for DL-Lite TBoxes. The transformation is inspired by [1],
which contains a transformation from a DL-Lite TBox into a theory in the one
variable fragment of first order logic. Considering T-models instead of classical
DL models allows us to obtain a simpler transformation to propositional logic
than theirs to first order logic.
   Function φ(·) maps a basic concept to a propositional variable, and a general
concept (resp., a TBox axiom) to a propositional formula.

           φ(⊥) = ⊥,      φ(A) = pA ,     φ(> n R) = pnR ,
           φ(¬C) = ¬φ(C),                φ(C1 u C2 ) = φ(C1 ) ∧ φ(C2 ),
           φ(C1 v 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-LiteN bool 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 define a formula η whose models are exactly the set of
types. Let              ^              ^
                  η=                                pnR → pmR .
                      R+ ∈SR     m,n∈SN with m<n
                               and m<k<n for no k∈SN

Then, mod(η) = {φ(τ ) | τ is a type} where φ(S) stands for for {φ(B1 ) | B ∈ S}
for a set S of basic concepts.                    V
    Given a coherent DL-Lite TBox T , let φ(T ) = α∈T φ(α) ∧ η. 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) ∧       (puP ∧ pvP − )
                               C(a)∈A       P ∈SR


where u and v are respectively, the maximal number in SN s.t. u ≤ |{bi | P (a, bi ) ∈
A}| and v ≤ |{bi | P (bi , a) ∈ A}|. 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 )) = {φ(τ ) | τ ∈ TM(T )};
2. mod(φa (A) ∧ η) = {φ(τ ) | τ ∈ TMa (A)}.
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 mod-
els, we can encode (minimal) distances between them using QBFs, by extending
the encoding in [4], which was introduced for a different purpose. In particular,
we need to encode the distances between the models of φ and the models of
ϕ1 , . . . , ϕn (n ≥ 1), where φ and ϕi ’s are propositional formulas in signature V .
We make n-fresh copies of V to, informally, encode the models of ϕ1 , . . . , ϕn ,
                       i
respectively; let V S    = {pi | p ∈ V } for 1 ≤ i ≤ n where each pi is a fresh variable
for p, and V = 1≤i≤n V i . For a propositional formula ϕ and 1 ≤ i ≤ n, ϕi
                  N

denotes the formula obtained from ϕ by replacing each occurrence of p with pi .
We also need another n-fresh copies of V , Vdi = {pid | p ∈ V } to represent the
distances. An assignment to Vdi is expected to capture the difference between a
model of φ and a model of ϕi , and in particular,       pid is assigned true if the truth
values of p and p are different. Let Vd = 1≤i≤n Vdi . Define
                     i                       N
                                                  S

                                             ^             ^                        

          F (φ, hϕ1 , . . . , ϕn i) = φ ∧           ϕii ∧         (p ↔ ¬pi ) → pid     .
                                            1≤i≤n           p∈V


A model M of F (φ, hϕ1 , . . . , ϕn i) 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 difference between the former two models. We use → instead of ↔
here, as we will further constraint the assignments of VdN to minimal distances.
   Furthermore, define a QBF

 D(φ, hϕ1 , . . . , ϕn i) =(∃V ∃V N F (φ, hϕ1 , . . . , ϕn i)) ∧
                             ^                                                       

                                  pid → ¬∃V ∃V N F (φ, hϕ1 , . . . , ϕn i) ∧ (p ↔ pi ) ,
                           p∈V
                          1≤i≤n


where ∃V with V = {p1 , . . . , pk } is an abbreviation for ∃p1 . . . ∃pk . A model Md
of D(φ, hϕ1 , . . . , ϕn i) is an assignment to VdN representing a minimal distance
between the models of φ and the model tuples of hϕ1 , . . . , ϕn i. The first con-
junct of D(φ, hϕ1 , . . . , ϕn i) says that there is a model of φ and a model tuple
of hϕ1 , . . . , ϕn i 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 , . . . , ϕn i)
be the set of minimal distances (w.r.t. ) between φ and hϕ1 , . . . , ϕn i (of the form
hM 4M1 , . . . , M 4Mn i with M ∈ mod(φ) and Mi ∈ mod(ϕi )). Then,

    mod(D(φ, hϕ1 , . . . , ϕn i)) = {Md ⊆ VdN | ∃d ∈ M D(φ, hϕ1 , . . . , ϕn i) s.t.
                                       m(Md ∩ Vdi ) = di for each 1 ≤ i ≤ n}.

    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 on-
tology profile Π = hT1 , . . . , Tn i and a TBox Te , all the types in σ(TM(Te ), TM(Π))
satisfy TBox axiom α if and only if QBF ¬∃VdN E(Π, Te , α) evaluates to true,
with

         E(Π, Te , α) = D(φ(Te ), hφ(T1 ), . . . , φ(Tn )i) ∧
                                                                        
                     ¬∀V ∃V N F (φ(Te ), hφ(T1 ), . . . , φ(Tn )i) → φ(α) .
                                                                  



This QBF can be understood as follows. A model M of E(Π, Te , α) is an as-
signment to VdN , and represents, by the first 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 hav-
ing 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 individ-
ual a in A, all the types in σ(TM(Te ) ∩ TMa (A), TM(Π)) satisfy α iff QBF
¬∃VdN 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 profile with coherent source TBoxes, Te be
a TBox and Ac be an ABox in DL-LiteN                  ∗        †
                                          bool . Let A = Ac ∪ A . Given a TBox
axiom α, we have ∇(Π, Te , Ac ) |= α iff the following QBF evaluates to true
                                           _
              ¬∃VdN E(Π, Te , α) ∨                     Ea (Π, Te , A∗ , α) .
                                                                          

                                                                                  (1)
                                      a occurs in A∗



5      System Architecture

We have implemented the algorithm for answering subclass queries in ontol-
ogy 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 first 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 unsatisfiable concepts in
the union of input ontologies (as will be explained later) and the input CC. Thus,
the number of unsatisfiable concepts plays a crucial role in the complexity of the
reduction algorithm.
    In OntoMerge, we first check whether the given ontologies can be simply
jointed without causing any incoherency using an off-the-shelf DL reasoner (Her-
miT [7] is used in the current program). The set of unsatisfiable concepts will
be stored for being used later. If the union of input ontologies is coherent, the
query answering can be done by the DL reasoner; otherwise, the system gen-
erates the QBF specified in Eq.(1). For this purpose, the system will first scan
all input ontologies to obtain the set of basic concepts occurring in these on-
tologies and assign a propositional variable with each basic concept. Then the
QBF is generated in QBF 1.0 format5 . The structure of OntoMerge is depicted
in Figure 1.




                    Fig. 1. System Structure of OntoMerge


However, as most of efficient QBF solvers accept only input QBFs in the prenex
normal form, the QBF generated in this way cannot be directly fed to a QBF
solver. So we need to convert the QBF into the prenex normal form first. Un-
fortunately, the standard translation from a given QBF into its prenex normal
form is very inefficient and thus several heuristics based on the specific QBF
are used to optimize the efficiency in our implementation. For instance, from
Eq.(1), we can see that the major source for introducing a large number of new
variables is from the construction of the ABox A∗ . So we introduce new variables
for only those concepts that are unsatisfiable and add new assertions for such
new variables to A∗ in the reduction algorithm. This optimization significantly
reduces the number of new variables.
5
    http://qbflib.org/boole.html
     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
efficient QBF solver is used to decide the validity of the QBF.


6   Experimental Results

To test the efficiency of OntoMerge, we used the DL-LiteN    bool fragment of the
medical ontology Galen8 , which is of medium size. Our experimental results show
that the system is relatively efficient, while further optimization is still under
way. Specifically, various randomly modified 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
   unsatisfiable concepts.
 – Fixed total number of unsatisfiable concepts but varied total number of
   axioms in the input ontologies.
 – Fixed number of unsatisfiable 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 [8] were used in our tests. For each test, the time
is limited to one hour (i. e. the program will be terminated after one hour no
matter a result is returned or not).




          Fig. 2. Total axioms:42, unsatisfiable concepts from 1 to 18

    Figure 2 shows the experimental results in the first set of tests. In each test,
42 axioms were randomly selected from Galen ontology and they were separated
into two sub-ontologies for merging. Then assertions were inserted into one of
them so that some concepts became unsatisfiable in the union of these two
ontologies. The number of unsatisfiable concepts varied from 1 to 18. From this
6
  http://www.qbflib.org/qdimacs.html
7
  http://logic.pdmi.ras.ru/~basolver/rtl.html
8
  http://www.co-ode.org/galen/
figure 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 unsatisfiable concepts increases, the size of the
QBF generated increases linearly. However, when the number of unsatisfiable
concepts is over 18, OntoMerge can still generate the QBF but the QBF solver
is unable to decide the validity of such a QBF.




 Fig. 3. Total number of unsatisfiable concept:1, total axioms from 26 to 174

    In the second set of tests, we fixed the number of unsatisfiable 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 first set of tests. This is partly due to the fact that
with the increase of the total axioms, the size of the QBF significantly increases
too. Similar to the case for the first set of tests, when the total number of axioms
is over 174, the QBF solver fails again.




         Fig. 4. Ratio of unsatisfiable concepts to total axioms = 0.15

    In the third set of tests, we fix the ratio of total number of axioms to the
number of unsatisfiable concepts to around 0.15 but let the total number of
axioms varied from 26 to 92 as well as the number of unsatisfiable 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.
7   Conclusion
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
efficient QBF solvers. We have implemented a preliminary merging system On-
toMerge, 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 dis-
cussions with him. Kewen Wang was partially supported by the ARC grants
DP1093652 and DP110101042. Guilin Qi was partially supported by the NSFC
grant 61272378.

References
 1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite
    family and relations. J. Artif. Intell. Res., 36:1–69, 2009.
 2. D. Calvanese and G. De Giacomo. Data integration: A logic-based perspective. AI
    Magazine, 26(1):59–70, 2005.
 3. J. P. Delgrande and T. Schaub. A consistency-based approach for belief change.
    Artif. Intell., 151(1-2):1–41, 2003.
 4. J. P. Delgrande, T. Schaub, H. Tompits, and S. Woltran. On computing belief
    change operations using quantified boolean formulas. J. Log. Comput., 14(6):801–
    826, 2004.
 5. J. Euzenat and P. Shvaiko. Ontology matching. Springer-Verlag, 2007.
 6. P. Everaere, S. Konieczny, and P. Marquis. Conflict-based merging operators. In
    Proc. KR, 348–357, 2008.
 7. I. Horrocks, B. Motik and Z. Wang. The HermiT OWL Reasoner. Proc. IJCAR-
    ORE workshop, 2012.
 8. R. Goultiaeva, V. Iverson, and F. Bacchus. Beyond CNF: A circuitbased QBF
    solver. In Proc. SAT, 412–426, 2009.
 9. A. Kalyanpur, B. Parsia, E. Sirin, and B. Cuenca Grau. Repairing unsatisfiable
    concepts in OWL ontologies. In Proc. of ESWC, pages 170–184, 2006.
10. A. Kalyanpur, B. Parsia, E. Sirin, and J. A. Hendler. Debugging unsatisfiable
    classes in owl ontologies. J. Web Semantics, 3(4):268–293, 2005.
11. S. Konieczny and R. Pino Pérez. Merging information under constraints: A logical
    framework. J. Log. Comput., 12(5):773–808, 2002.
12. T. Meyer, K. Lee, and R. Booth. Knowledge integration for description logics. In
    Proc. AAAI, 645–650, 2005.
13. G. Qi and J. Du. Model-based revision operators for terminologies in description
    logics. In Proc. IJCAI, 891-897, 2009.
14. S. Schlobach, Z. Huang, R. Cornet, and F. van Harmelen. Debugging incoherent
    terminologies. J. Autom. Reasoning, 39(3):317–349, 2007.
15. Z. Wang, K. Wang, and R. Topor. A new approach to knowledge base revision in
    DL-Lite. In Proc. AAAI, 369–374, 2010.

</pre>