Extension of Ontologies Assisted by Automated Reasoning Systems

Extension of Ontologies Assisted by Automated Reasoning Systems 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. Spain Abstract. A method to extend ontologies with the assistance of automated reasoning systems and preserving a kind of completeness with respect to their associate conceptualizations is presented. The use of such systems makes feasible the ontological insertion of new concepts, but it is necessary to re-interpret the older ones with respect to new ontological commitments. We illustrate the method extending a well-known ontology about spatial relationships, the called Region Connection Calculus. 1 Introduction Ontology Management has becomed in a critical issue in fields related with Knowledge Representation and intelligent information processing as the Semantic Web. One of the involved tasks, the most important, is the need of extending or revising ontologies. This task may be, from the point of view of companies, dangerous and expensive: every change in the ontology can affect to the overall knowledge organization of the company. Moreover it is also known that the self process of extension is hard to automatize: the tools are designed to facilitate the syntactic extension or ontology mapping. But the effect of ontology mapping on the logical reasoning may be, in general, unknown, and specially on the use of automated reasoning systems [2]. The aim of this paper is to propose a formal semantics for ontology extension (following the foundational principles given in [2] and suggested by the computer-assisted cleaning of Knowledge Databases [1]) as well as a feasible method, assisted by Automated Reasoning Systems (ARS), to extend ontologies preserving a certain type of robustness. 2 Lattice Categorical Extensions We assume throughout that the conceptualization associated to the ontology is endowed of lattice structure. Actually it is not a constraint: there are methods Partially supported by the project TIN2004-03884 of Spanish Ministry of Education and Science, cofinanced by FEDER funds. to extract lattices of concepts from data (such as the Formal Concepts Analysis, see e.g. [8]), and an ontology is easy to be extended by definition to satisfy it. Although we think about Description Logics as a language (a logical basis for ontology languages like OWL, see http://www.w3.org/TR/owl-features/), the framework is useful for First Order Logic (FOL). Alattice categorical theory is a theory that proves the lattice structure of its basic concepts. It is a reasonable requirement: the theory must certify the basic relationships among them. We aim to replace completeness by lattice categoricity to make feasible the extension of formal ontologies. Fixed a language, let C={C1,...,C n}be a set of concept symbols and let T be a theory (in the general case, definable concepts in Tcanbeassumed)andlet us consider the language LC={,⊥,≤}∪{c:c∈C}.GivenM|=T,weconsider the LC-structure L(M,C), whose universe is the set of the interpretations in Mof the concepts (is M,⊥is ∅), and ≤is the subset relation. The relationship between L(M,C)andtheselfMis based in two facts. The first one, that the lattice can be characterized by a finite set of equations E, plus a set of formulas ΘCcategorizing the lattice under completion, that is, ΘC includes the domain closure axiom, the unique names axioms and aditionally the axioms of lattice theory. Secondly, there is a natural translation Πof lattice equations into FOL formulas such that if Eis a set of equations characterizing L(M,C), then M|=Π(E). Definition 1. We say that a LC-theory Eis a lattice skeleton (l.s.) for Tif –There is M|=Tsuch that L(M,C)|=E+ΘC,and –E+ΘChas an only model (modulo isomorphism). Every consistent theory Thas a lattice skeleton (it is sufficent to categorically axiomatize the lattice associated to some model of T). Intuitively, the existence of essentially different lattice skeletons difficults the reasoning with the conceptualization associate to T. Definition 2. Tis called a lattice categorical (l.c.) theory if whatever two lattice skeletons for Tare equivalent modulo ΘC. It is easy to see that every Tconsistent has a lattice categorical extension: it is sufficent to consider a model M|=T, and next to find a set Eof equations such that ΘC+Ehas L(M,C) as only model. The theory T+Π(E)(andany consistent extension of it) is l.c. To simplify, we deal with a pair (T,E)-whereTis lattice categorical and E is a lattice sekeleton for T-thatwecallalattice categorical core (l.c.c.). Thus, (T,E) is a l.c.c. if T+Π(E) is a l.c. theory. Definition 3. Given two l.c.c. (T1,E 1),(T2,E 2)with respect to the sets of concepts C1and C2respectively, we say that (T2,E 2)is a lattice categorical extension of (T1,E 1)if L(T1,C1)⊆L(T2,C2)and L(T2,C2)|=E1. 3 Extending Ontologies In order to obtain a practical method, some of the basic (theoretical) logical principles required by the definitional methodologies of building of formal ontologies must be weakened [3]. Such principles, in their original forms, are: 1. Ontologies should be based upon a small number of primitive concepts. 2. These primitives should be given definite model theoretic semantics. 3. Axioms should only be given for the primitive concepts. 4. Categorical axiom sets should be sought. 5. The remaining vocabulary of the ontology (which may be very large), should be introduced purely by means of definitions. The three first principles are assumed, but, in order to a feasible management, the last two ones (two strong logical constraints) are weakened. The fourth one will be replaced by lattice categoricity, more manageable than logical categoricity or completeness. With respect to the last one, if we start with a basic theory, it can be hard to define any new concept/relation by means of the basic elements of the ontology. Thus, we must consider that there are ontological insertions,that is, additions of new concepts/relations not ontologically defined on the former ontology. This may produce a deep readdress of the domain analysis. The method consists of four steps, assisted by an automated theorem prover (in our case, OTTER, http://www-unix.mcs.anl.gov/AR/otter/), a model finder (MACE4, www-unix.mcs.anl.gov/AR/mace4/), and a last stage for ontological reconsideration. Starting from a lattice categorical theory: 1. First, one extends the lattice of the basic concepts of the ontology by extending the selected skeleton. 2. Next, one applies MACE4 on a possible axiomatization of the new lattice in order to obtain the new lattices. In general, the characterization of the lattice is a theory weaker than the initial ontology. 3. The third step consists of the refinement of the skeleton in order to MACE4 exhibits one only model (that is, the theory is lattice categorical). 4. Finally, it is necessary to certify (by means OTTER or hand-made) the unicity of above model. The final stage of the method is not algorithmical. It consists of an ontological interpretation of the new element, by re-interpreting (generally by refining) if necessary, the older ones. This task, nonalgorithmical in essence, is responsability of experts in the domain represented by the ontology. In fact, such re-interpretation can force us to reconsider the initial ontological commitments. 4 An Example in Qualitative Spatial Reasoning We shall apply the method for extending an ontology on Qualitative Spatial Reasoning by means of the insertion of relations on imperfect spatial information, concretely the well-known Region Connection Calculus (RCC) [6]. The DC(x, y)↔¬C(x, y)(xis disconnected from y) P(x,y)↔∀z[C(z,x)→C(z,y)] (xis part of y) PP(x,y)↔P(x, y)∧¬P(y,x)(xis proper part of y) EQ(x, y)↔P(x, y)∧P(y,x)(xis identical with y) O(x, y)↔∃z[P(z,x)∧P(z,y)] (xoverlaps y) DR(x,y)↔¬O(x, y)(xis discrete 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)(xis externally connected to y) TPP(x,y)↔PP(x, y)∧∃z[EC(z,x)∧EC(z,y)] (xis a tangential prop. part of y) NTPP(x, y)↔PP(x, y)∧¬∃z[EC(z,x)∧EC(z,y)] (xis a non-tang. prop. part of y) Fig. 1. Axioms of RCC ≡CDR PO¬P¬Pi¬DR DR≡EC DC NTPP¬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. 2. The skeleton Efor the lattice of concepts of RCC need of such extension arose, for example, when we applied RCC as a metaontological tool for analysing and repairing anomalies in ontologies [1] [5]. RCC is a mereotopological approach to spatial reasoning; the spatial entities are nonempty regular sets. The primary relation is the connection,C(x, y), with intended meaning: “the topological closures of xand yintersect” and basic axioms ∀x[C(x, x)] and ∀x, y[C(x, y)→C(y,x)] jointly with a set of definitions on the main spatial relations (fig. 1). Actually the theory has other axioms (see [6]), but these are not necessary to prove the lattice structure of the set of relations (shown in fig. 3). Thus, RCC is lattice categorical. 4.1 Isolating a Skeleton for RCC In order to isolate a skeleton without redundant formulas, we start with the lattice equations induced by the Hasse diagram of the RCC-relations. Next we sequentially remove equations of this set when such elimination does not produce other new lattices modelling the final set. The set of equations E,seethefigure 2, we obtain has an only model (is a skeleton). categorizes under completion the lattice of the RCC-spatial relationships (given in fig. 3) [5]. 4.2 Inserting New Elements The Jointly Exhaustive and Pairwise Disjoint set (JEPD) of atomic relations of the lattice (fig. 3) is denoted by RCC8. It represents the set of the most specific spatial relations in RCC8. Our aim is to insert a new relation representing undefinition, such relation must be disjoint with RCC8. 12345678 910 1211 13 14 15 16 PP PO TPP EQ EC DCTPPi NTPPi PPi PiP O CDR NTPP 0 aba ba b a b a bb a ab a b yolk egg Fig. 3. The lattice of RCC-relations (left) and the egg-yolk representation of vague regions (right) Theorem 1. There are only eight E-conservative extensions of the lattice of RCC by insertion of a new relation Dsuch that RCC8∪{D}is a JEPD set. In the proof of the theorem we use MACE4 for listing the lattice extensions, taking as input the lattice axioms, the skeleton, the unique names principles and the closure domain axiom. The system outputs eight extensions. Since MACE4 has not been formally verified to work correctly, it is necessary to certify that such models are correct, and, by finding OTTER’s proofs, to show that the list of models is exhaustive. The analysis of the extensions (fig. 4) suggests us that the new relations represent undefinition up to a degree. 4.3 Refining the Skeleton for the New Extension We are not specially interested here in a determinated extension, although there exist situations where it is necessary to select one of them (by example, when we intend to classify unaccurate data [4]). However, the refinement of the skeleton is easy: once an extension is selected. For instance, with respect to the first extension, it is sufficent to substitute the formula PP ≡TPP NTPP by the new formula PP ≡TPPI1NTPP to obtain a skeleton Efor the extension. Every extension of (RCC, E) is a l.c. extension of (RCC, E). 4.4 Final Stage: Ontological Interpretation Finally, we need to mereotopologically interpret the new relations. In [5] four different interpretations are offered, we tried to use some of them for supporting CDR O PPi PP PPi EC DCPO NTPP TPP EQ TPPi NTPPi I CDR O PPi PP PPi EC DCPO NTPP TPP EQ TPPi NTPPi I CDR O PPi PP PPi ECPO NTPP TPP NTPPiEQ TPPi DC I CDR O PPi PP PPi ECTPPiPO DCNTPP TPP EQ NTPPi I CDR DC O P PPi TPPi NTPPiEQTPPPO Pi PP NTPP EC I CDR DC PP ECNTPPPO TPP EQ O PPi PPi NTPPiTPPi I CDR PP NTPPPO TPP EQ O PPi PPi NTPPiTPPi EC DC I C PP NTPPPO TPP EQ O PPi PPi NTPPiTPPi EC DC DR I Fig. 4. The eight lattice describing the l.c. extensions of RCC by undefinition ontological cleaning tasks. In order to show how they can be interpreted in each case, we consider the classical egg-yolk interpretation of spatial vague regions [7]. Intuitively, a spatial region acompounded by two subregions, as figure 3 shows, the first, y(a)(the yolk) which represents accurate locations in a,andthe second one, e(a) bounding the unaccurate locations of a. In [7] the 48 possible spatial relations between two vague regions are shown. If we want to work with I1, for example, its vague interpretation is I1(a, b)≡PP(e(a),e(b)), while RCC relations are interpreted by the natural way. 5FinalRemarks The method described here is a logical basis for extending ontologies. Since there is a lack of formal notions -feasible in practicedescribing features about completeness in the evolution of formal ontologies, we think that our proposal can be useful to add formal semantics to several ontological transformations [5] [1], achieving in this way the logical trust. The feasibility of the method depends of two factors: the use of efficent ARS and the simplicity of the completeness notion, related with the conceptualization of the ontology. Future research lines are addressed to embrace the use of roles on spatial reasoning. References 1. J. A. Alonso-Jim´enez, J. Borrego-D´ıaz and A. M. Ch´avez-Gonz´alez, Ontology Cleaning by Mereotopological Reasoning Proc. of DEXA Workshop on Web Semantics (WebS’04), (2004). IEEE Press, pp. 132-137. 2. J. A. Alonso-Jim´enez, J. Borrego-D´ıaz, A. M. Ch´avez-Gonz´alez and F.J. Mart´ın- Mateos, Foundational challenges in Automated and Ontology Cleaning in the Semantic Web. To appear in IEEE Intelligent Systems. 3. B. Bennett, The Role of Definitions in Construction and Analysis of Formal Ontologies, in: P. Doherty, J. McCarthy, and M. Williams (eds.) Logical Formalization of Commonsense Reasoning (2003 AAAI Symposium), pp. 27-35, AAAI Press (2003). 4. J. Borrego-D´ıaz and A. M. Ch´avez-Gonz´alez, Management Undefinability in Data Through Automated Ontology Extensions, submitted (2005). 5. A. Ch´avez-Gonz´alez, Mereotopological Automated Reasoning for Ontology Cleaning, forthcoming Ph.D. thesis. 6. A. G. Cohn, B. Bennett, J. M. Gooday and N. M. Gotts. Representing and Reasoning with Qualitative Spatial Relations about Regions. Chapter 4 in O. Stock (ed.), Spatial and Temporal Reasoning, Kluwer, Dordrecth (1997). 7. A.G. Cohn and N.M. Gotts, The ’Egg-Yolk’ Representation of Regions with Indeterminate Boundaries in P. Burrough and A. M. Frank (eds), Proc. GISDATA Specialist Meeting on Geographical Objects with Undetermined Boundaries, GISDATA Series, vol. 3, Taylor and Francis, pp. 171-187 (1996). 8. G. Stumme, R. Taouil, Y. Bastide, N. Pasquier and L. Lakhal, Computing Iceberg Concept Lattices with TITANIC. Data Knowl. Eng. 42(2) pp. 189-222 (2002).