On the Use of Automated Reasoning Systems in Ontology Integration.

On the Use of Automated Reasoning Systems in Ontology Integration Joaqu´ın Borrego-D´ıaz and Antonia M. Ch´avez-Gonz´alez Departamento de Ciencias de la Computaci´on e Inteligencia Artificial. E.T.S. Ingenier´ıa Inform´atica-Universidad de Sevilla. Avda. Reina Mercedes s.n. 41012-Sevilla {jborrego, tchavez}@us.es Abstract. Ontology Integration is a challenge in the field of Knowledge Engineering, whose solution is indispensable for the envisioned Semantic Web. Some approximations suffer from logical confidence, and others are hard to mechanize. In this paper a method – assisted by Automated Reasoning Systems – to solve a subproblem, the merging of ontologies, is presented. A case study of application is drawn from the field of Qualitative Spatial Reasoning. Key words: Ontology merging, lattice categorical theory, formal ontology building 1 Introduction Ontology building has been an aim of the Knowledge Representation (KR) community during the last decades and, with special emphasis, in the last years, with the project of Semantic Web (SW). Such a project aims to enrich the Web by machine processable information [5]. Ontologies help to assign metadata to information by means of the formal description of the elements which belong to the discourse universe. This point of view restricts the attention to projects more feasible than ontologies for commonsense reasoning, which need the representation of a huge portion of human experience, encompassing knowledge about spatial, physical, social, temporal, and psychological aspects [19]. Nevertheless, ontology building is not sufficent. Knowledge Engineering practice shows that the representation is not static. Ontologies must be maintained as any other component of information systems. Knowledge Reuse requires ontologies are extended, refined or integrated [28]. The acceptation of ontology representation languages as OWL1has facilitated the proliferation of ontologies. Thus, the necessity of relating ontologies arises in order to take advantage of the knowledge jointly contributed by different ontologies. Basically, there exist three kinds of reconciliation of the knowledge represented by ontologies: merging, alineation and integration. Partially financed by project 2C/040 belonging to Proyecto Minerva, plataforma de sevicios en movilidad Cartuja 93 1http://www.w3.org/TR/owl-features/ 38 Proceedings of ONTOSE 2009 The aim of this paper is to propose a formal definition of ontology merging, following ideas from [9]. The definition we propose is inspired in methods for cleaning Knowledge Databases referenced by ontologies [3, 11]. Likewise, a merging method assisted by Automated Reasoning Systems (ARS) is described. This method is based on the formal framework of ontological extensions presented in [9, 10]. For the sake of clarity, the method is illustrated by merging two spatial ontologies designed for Qualitative Spatial Reasoning (QSR). Two spatial ontologies will be merged. The first one is the Region Connection Calculus (RCC) [12]. The second one is a micro-ontology about the relative size of spatial entities, SIZE. The interest of this merging arises from human perception. For example, it is known that some topological relationships (i.e. A is properly contained in B) only are possible if the involved objects possess relatively suitable size. Thus, it is interesting the joint management of both ontologies. In this case, merging is advisable. Currently, we use RCC as meta-ontology in order to spatially interpret concepts associated to ontologies [8]. Spatial metaphora is a powerfull technique for user’s understanding of ontology-based information systems (see [15, 23]). In general, the mereology is a natural source for supporting metaproperties on concepts and relations in Ontological Engineering [18, 20]. The structure of the paper is as follows. Next section addresses the problem of ontological evolution, using as example the case of Qualitative Spatial Reasoning. Ontologies RCC and SIZE are described in section 3. In section 4, the notion of lattice categorical ontology is presented and practicalfeaturesofthisnotion are justified. Next, section 5 contains the logical ground for the formalization of the ontology merging method and the running example is computed. The article ends with some notes on related work and future aims. 2 Evolution of ontologies: Extending or revising? The revision of an ontology may be considered, to some extent, from two points of view. On one hand, the task is similar to knowledge revision, thus the problem can be analysed by means of classic methods (see e.g. chapter 6 in [25]). On the other hand, ontology evolution should preserve some sort of backward compatibility, while possible. Therefore, the advantage of extension on revision is the feasibility of preserving ontological features of source theory. This option is only possible if the theory is robust [6]. A formalization of robustness given in [2] is presented in [9], and it will be described in section 4. A discussion of these aspects can be found in [10]. Nevertheless, an ontological insertion is not interesting if it is not supported by a good theory about its relationship with the source theory, as well as a sound expansion of a representative class of models of the source theory to models of the new one (such class have to contain the intended models). For example, in the case of mereotopological reasoning, it can be necessary to show an intuitive topological interpretation of the new elements (and a re-interpretation of the older ones compatible with basic original principles), which should be formalized. Proceedings of ONTOSE 2009 39 This requirement is mandatory if one wishes to expand models of theory source to models of the new theory [11]. Therefore, one could consider ontology evolution as a sequence of extensions and revisions. As we have already commented, both methods are intimately tied. Likewise, above discussion is appliable for merging formal ontologies. Therefore, two ways for merging two ontologies O1and O2basedontheseideascanbe considered. A first one consists in repeatedly extending O1by defining the terms of O2(using the language of O1) producing this way a conservative extension of O1. Such definitions cannot exist in many cases, so it is necessary to consider a second method, based on the ontological insertion of the terms of O2in O1 (possibly in parallel). For obtaining sound extensions, it is necessary to design axioms relating terms of both ontologies, for preserving basic features [9]. 3 Two examples of formal ontologies We succintly present the main features of the ontologies used in the example. 3.1 RCC ontology The Region Connection Calculus is a well-known topological approach to qualitative spatial representation and reasoning. For RCC, the spatial entities are non-empty regular sets (NERC)2(A deep introduction to the theory can be found in [12], and the set of axioms appears in figure 1). The topological models of RCC have been investigated by N.M. Gotts in [16], where the author shows that every regular connected nontrivial topological space is a model of the theory (choosing as elements the NERCs); although it is also possible to study the models by means of a complete algebraic description [29]. Spatio-temporal reasoning has been studied in several papers [31,27,17]. DC(x, y)↔¬C(x, y)(xdisconnected from y) P(x, y)↔∀z[C(z,x)→C(z,y)] (xpart of y) PP(x, y)↔P(x, y)∧¬P(y,x)(xproper part of y) EQ(x, y)↔P(x, y)∧P(y,x)(xidentical with y) O(x, y)↔∃z[P(z,x)∧P(z,y)] (xoverlaps y) DR(x, y)↔¬O(x, y)(xdiscrete from y) PO(x, y)↔O(x, y)∧¬P(x, y)∧¬P(y,x)(xpartially overlaps y) EC(x, y)↔C(x, y)∧¬O(x, y)(xexternally connected to y) TPP(x, y)↔PP(x, y)∧∃z[EC(z,x)∧EC(z, y)] (xtangential prop. part of y) NTPP(x, y)↔PP(x, y)∧¬∃z[EC(z,x)∧EC(z,y)] (xnon-tang. prop. part of y) Fig. 1. Axioms of RCC 2Asetxof a topological space is regular if it agrees with the interior of its closure. 40 Proceedings of ONTOSE 2009 Fig. 2 illustrates the set of eight jointly exhaustive and pairwise disjoint (JEPD) relations called RCC8. If one considers RCC8 as a calculus, all possible unions of the basic relations are also considered. ab ababab a b ab b a PO(a,b) TPPi(a,b) EC(a,b) TPP(a,b) NTPP(a,b) NTPPi(a,b)DC(a,b) EQ(a,b) a b Fig. 2. Spatial relations of RCC8 The set RCC relations enjoys the structure of lattice whose Hasse diagram is shown in figure 3, that coincides with their intended meanings. This structure is provable by RCC [11]. 12345678 910 1211 13 14 15 16 0 CDR O PPi PPiPP PO NTPP TPP EQ TPPi NTPPi EC DC Fig. 3. The lattice of spatial relations of RCC 3.2 SIZE ontology The ontology RCC is insufficient for reasoning with many spatial features. Therefore there appears the need of enriching RCC to reason with other features. The second ontology dealed in this paper is SIZE, the natural ontology about the relative size of spatial entities. Such an ontology has already been used jointly with RCC in [14], where the authors extend the study of constraint satisfaction problems on RCC8 done in [27]. The SIZE relationships are: LS(x, y)(xhave less size than y)anditsinverse, LSi(x, y); the relation LSE (xhave less or equal size than y)anditsinverse LSEi(x, y); and SS(x, y)(xand yhave the same size). Some axioms of SIZE are shown in figure 4 (rigth). The SIZE ontology suffices to prove that the relations form the lattice depicted in figure 4 (left). Proceedings of ONTOSE 2009 41 LS LSE SS LSi LSEi ∀x, y(LS(x, y)∨LSi(x, y)∨SS(x, y)) ∀x, y(LS(x, y)→¬(LSi(x, y)∨SS(x, y)) ∀x, y(LSE(x, y)↔LS(x, y)∨SS(x, y)) ∀x, y(SS(x, y)↔SS(y,x)) ∀x, y(LS(x, y)↔LSi(y,x)) Fig. 4. Some axioms of SIZE and the associated lattice Note that SIZE does not deal with the qualitative size of regions. In this case, adjectifs (unary predicates) have to be used [21]. 3.3 Articulation of RCC and SIZE The articulation of two ontologies describes the existent relationship between terms of both ontologies (see [4] for a formalization of such notion). The articulation of RCC and SIZE is depicted in figure 5. Note that the articulation is E:= ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ TPP LS EQ SS NTPP LS SS DC EC POEQ TPPi LSi LSi DC EC POTPPiNTPPi NTPP LSi LS DC EC POTPP NTPP Fig. 5. Relationship between RCC and SIZE simple; in fact, it can be considered as a sublattice of that of RCC (see fig. 6). In this work the merging of RCC and SIZE as running example is computed, preserving articulation and satisfying a minimality condition (the size of concept lattice) more feasible to achieve than categorical minimality [4]. Lastly, note that SIZE is independent from space dimension. Thus it is also valid for working with temporal intervals, then one might think of combining SIZE with Allen’s ontology about temporal intervals [1]. 4 Extension of lattice-categorical theories In this section we remember formal definitions and properties, formalizing two notions: robustness (lattice categoricity) and extension (lattice categorical extension). Our thesis states that one can change logical completeness by lattice categoricity to make easier the design of feasible methods for extending a theory. A formalization of these ideas can be found in [9, 10]. Consider a first order language, let R={R1,...,R n}be a (finite) set of concept symbols (or relations symbols with the same arity n)andletTbe a theory3.GivenM|=T, we consider the structure L(M,R), in the language 3In the general case, one can consider definable concepts/relations in T. 42 Proceedings of ONTOSE 2009 LS LSE SS LSi LSEi 12345678 910 1211 13 14 15 16 0 CDR O PPi PPiPP PO NTPP TPP EQ TPPi NTPPi EC DC PP EQ PPi PiP P V Pi Fig. 6. Articulation of RCC and SIZE LR={,⊥,≤}+{r1,...,r n}, whose universe is the interpretations in Mof the relations (interpreting rias RM i), is Mn,⊥is ∅and ≤is the subset relation. Notice that, in general, L(M,R) does not have lattice structure. Nevertheless, this requisite is assumed in the remainder of the paper. The Formal Concept Analysis FCA [13], produce such structures. In any case, it is easy to satisfy it by extending by definitions of new relations. From the logic point of view, a finite lattice Lon a set A={a1,...a n}can be categorically axiomatized by the set of axioms composed by: 1. A set ΘRof formulas that contains the axioms of lattice theory 2. The domain closure axiom (d.c.a.), 3. Unique names axiom (u.n.a.), And additionally, a set of (dis)equations ERwhich characterizes the Hasse diagram of the lattice. When L(M,R) is a lattice, the relationship with the self model Mis based on two facts. The first one is that the lattice Lcan be characterized by a finite set of equations EL,plusΘR. The second observation is that there exists a natural translation Πof such equations into formulas in the First Order Logic language in such way that if Eis a set of lattice equations characterizing L(M,R)(so L(M,R)|=E), it holds that M|=Π(E). Note that Π(E) is consistent with T. Definition 1. Let Ebe a LR-theory. We say that Eis a lattice skeleton for a theory Tif the following conditions hold: Proceedings of ONTOSE 2009 43 1. There exists M|=Tsuch that L(M,R)|=E+ΘR. 2. E+ΘRhas only one model (modulo isomorphism). Proposition 1. Suppose that Eis a set of equations in the language LRsuch that E+ΘRhas an only model. The following conditions are equivalent: 1. Eis a lattice skeleton of T. 2. T+Π(E)is consistent. Corollary 1. Every consistent theory has a lattice skeleton. The theory that we preserve throughout is the translation of RCC8 language of ERCC (In figure 7 it is described using Propositional Description Logic notation)4. Note that such theory has a limited syntactic complexity; one can say that this theory has exogenous character, as countepart to the endogenous character of their definitions in RCC. That is, it is a theory on relations without explicit reference to their definitions with respect to elements of the universe of the model. ≡CDPO¬P¬Pi¬DR DR ≡EC DC NTP P ¬TPP ¬Pi¬DR C≡OEC TPP ¬Pi¬DR O≡POPPi EQ ¬PPi¬DR Pi ≡EQ PPi TPPi ¬NTPPi¬DR P≡EQ PP NTPPi ¬DR PPi ≡TPPiNTPPi EC ¬DC PP ≡TPP NTPP Fig. 7. Exogenous representation of ERCC in Propositional Description Logic. Definition 2. Tis called a lattice categorical (l.c.) theory if any two lattice skeletons of Tare equivalent modulo ΘR. In other words, if one assumes that the only relations are in R,thenTcan prove the intended lattice structure induced by R. Proposition 2. The following conditions are equivalent: 1. Tis l.c. 2. If Eis any lattice skeleton for T,thenTΠ(E). That is, Tis a l.c. if E0+ΘR≡E1+ΘRfor all E0,E 1lattice skeletons of T. Since a l.c. theory Thas an only nonisomorphic lattice associated to R,we denote this lattice by L(T,R), to emphasize the lattice categoricity5. As it will shown in the next section, RCC is l.c. 4The last two formulas are ommited because their translations are tautologies. 5Tis a l.c. theory if ET+ΘRis a strictly categorical theory (that is, given any two models of ET+ΘR, there exists one only isomorphism between them). 44 Proceedings of ONTOSE 2009 Theorem 1. Let Tbe a consistent theory. There exists Tan extension of T which is lattice categorical. Apair(T,E)whereTis lattice categorical and Eis a lattice skeleton for T, called lattice categorical core (l.c.c.). Thus, (T,E) is a l.c.c. if T+Π(E) is a l.c. theory. The pair (RCC, ERCC ) that it will describe in next section is a l.c.c. To simplify the discourse, in the remainder of the paper a l.c.c. will be simply called ontology. Definition 3. Given two ontologies O1=(T1,E 1)and O2=(T2,E 2)with respect to sets of concepts/relations R1and R2respectively, we will say that O2 is a lattice categorical extension of O1(denoted by O1→lc O2)ifR1⊆R 2and E2|=E1. 5 Merging Lattice categorical ontologies In this section a proposal of ontology merging is presented. To simplify, suppose O1and O2are two ontologies with disjoint signatures. We assume that Eis a set of formulas relating concepts of both ontologies. Definition 4. An l.c. ontology O=(T,E)is a lattice categorical merging of O1and O2with respect to Eif O1→lc O,O2→lc O,L(T,R)|=E, and it is the lattice of minimum size with that property. In the case that articulation Oa exists, then the following diagram is conmutative, the interpretation of Oain O does not depend on the intermediate ontology: O1 lc lc  OaO lc  lc O2 The following method for l.c. merging is based on the one for lattice categorical extensions introduced in [9]: 1. First stage: Joint skeletons E1and E2with E;letE0:= E1∪E2∪E 2. Find, with MACE4, the lattices that models E0. If such lattices do not exist, ontologies are not compatible with respect to E0, then there is not merging (E0is not satisfiable). If MACE4 outputs some model, follow in (3). 3. Second stage: User analysis of a lattice of minimum size.Ifanyofthe relationships of the lattice is not accepted by the user, refine E0by adding new (dis)equations, to discard such lattice. Turn to the apply MACE4 to the refinement. This stage is repeatedly applied until a model L(of minimum size k)is accepted by the user. On this way a skeleton S0is obtained. Proceedings of ONTOSE 2009 45 4. Third stage: achieving lattice categoricity. Refine S0(by the addition of (dis)equations) until that the only model of size kis L.LetSbe the resulting set of equations. 5. Fourth stage: Certification. Certify (with an automated reasoning system, OTTER, if it is necessary) that Lis the only model of Sof size k.This way it is accurated that O=(T1∪T2∪S, S) is a l.c. merging. Theorem 2. The method described above outputs a l.c. merging of O1and O2. 5.1 Merging RCC and SIZE Suppose that it is intended to use SIZE on connected regions. Intuition says that it is unknown (a priori) the size relation between disconnected regions. Notice that this implies an ontological re-interpretation of SIZE relations. For example, LS(x, y) has to be understood as region xis connected with a region yof bigger size. That reinterpretation is compatible with articulation depicted in figure 6. Starting with the SIZE skeleton: E2=⎧ ⎨ ⎩ ≡LS LSi SS LSE ≡SS LS LSi LSE ¬SS LSi ¬SS ¬SS ≡LS LSi LSEi ≡SS LSi The set E0is compounded by E(fig. 5) jointly with: EC  LSE EC  LSEi SS ¬EC DC  LSE DC  LSEi SS ¬DC The execution trace of the method is described by the following table: Refinement Minimum size of a model Number of models without refinements 23 8 LS  O, LS ⊆ O24 1 SS  O24 1 LS PO ≡⊥ 27 1 LSi PO ≡⊥ 31 1 SS PO ≡⊥ 31 1 It accepts the final lattice depicted in figure 8. It is important to note that the user may need to interpret some of the new nodes. For example, node 22 represents the relation distinct sizes (that is, ¬SS), and node 23 represents the relation xpartially overlaps with a region yof distinct size. However, the use of new nodes can be unnecessary in practice; some nodes only represent algebraic operations on basic nodes (to satisfy lattice structure). Therefore, this lattice canbeprunedinordertoobtainaontological simpler structure.