Extending Qualitative Spatial Theories with Emergent Spatial Concepts: An Automated Reasoning Approach

Extending Qualitative Spatial Theories with Emergent Spatial Concepts An Automated Reasoning Approach Gonzalo A. Aranda-Corral1, Joaquı´n Borrego-D´ıaz2, and Antonia M. Ch´avez-Gonz´alez2 1 Departamento de Tecnolog´ıas delaInformaci´on. Escuela T´ecnica Superior de Ingenier´ıa - Universidad de Huelva. Crta. Palos de La Frontera s/n. 21819 Palos de La Frontera. Spain 2 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. Qualitative Spatial Reasoning is an exciting research field of the Knowledge Representation and Reasoning paradigm whose application often requires the extension, refinement or combination of existent theories (as well as the associated calculus). This paper addresses the issue of the sound spatial interpretation of formal extensions of such theories; particularly the interpretation of the extension and the desired representational features. The paper shows how to interpret certain kinds of extensions of Region Connection Calculus (RCC) theory. We also show how to rebuild the qualitative calculus of these extensions. 1 Introduction One of the main challenges in Qualitative Spatial Reasoning (QSR) is the need to combine or extend the existing theories to include new aspects in the same formalism [18,12]. In order to face the problem, several features and viewpoints must be considered. The focus here is the logical aspect of the challenge, particularly the relationship among models of initial theories and that of the new ones. A key aspect to consider in Artificial Intelligence in general is the feasibility/complexity of the reasoning process, by providing, for example, a qualitative calculus. This approach contrasts with the qualitative and nature inspired one [14]. Several of the purely logical features could be solved if a sound methodology is adopted, for example the definitional methodology for building formal ontologies [4]. It can be too rigid because of strong requirements such as logical categoricity. In contrast with this framework, in QSR the (characterization of) the class from intended models is more important than the general class of models. In fact, a sound interpretation of the revised ontology/theory for preserving those models is a key step especially if previous definitions have to be changed. For example, any extension by definition of a new concept/relationship should be supported by a Partially supported by Excelence project of Junta de Andaluc´ıa TIC 6064, cofinanced with FEDER founds. good theory about its relationship with the original theory, as well as by a nice way of expanding a representative class of models of the source theory to the new one. From this point of view, the use of automated reasoning systems can ensure the correctness of the results as well as that it has not been used spatial intuitions which are not formalized in the theory (c.f. [21] ). It is very important both the soundness of the associated calculus and the use of a spatial theory as basis for building and reasoning with ontologies [17]. The aim of the paper is to show how the assistance of automated reasoning systems (ARS) can help to classify, interpret and compute abstract extensions of QSR theories, required to accommodate new concepts and insights which Knowledge Engineering problems induces. The use of ARS provides an formal framework where contrast hypothesis, specifications and axioms. Specifically, the case of the extension of RCC theory [12,18] by insertion of an undefined relationship is analyzed. In a broad scope, the aim is to describe how rudiments of First Order Model Theory (and computational logic) can be used for increasing the knowledge on generic extensions of the QSR theory: On the one hand, by providing a formal support to the reasoning both from lattice of spatial relationships and transition tables. On the other hand, since the computing of the extensions is assisted by automated reasoning, it provides information to the designer which comes from the logical entailment. In this way the designer only has to re-interpret if necessary, elements from the older theory in order to satisfy those information requirements. This task, non algorithmic in essence, is the responsibility of experts in the domain represented by the ontology. In fact, such re-interpretation can force us to reconsider the initial ontological commitments. This paper addresses these issues. The rest of the paper proceeds as follows. Next section motivates the need of qualitative reasoning on abstract extensions of standard theories. Section 3 introduces basic features of lattice categorical extensions, a formal notion for extending theories and it recalls a result on extensions of RCC. Sections 4,5,6 represent the main contributions of the paper. In Section 4 the interpretation of the extensions by means topological pulsation is described. Section 5 shows how the transition table for the extensions from interpretation can be rebuilt. Section 6 shows other interpretation framework (egg-yolk approach). Conclusions and new insights are summarized in Section 7. 2 Interpretation of Generic Extensions The paper addresses in first place the problem of obtaining a sound interpretation (by providing a spatial meaning) of the extensions obtained by means automated reasoning; and, in the second one, it studies how from that interpretation, other tools for QSR (as transition tables) can be deduced. Formally: Definition 1. Let Ωbe a topological space and Tbe a mereotopological theory. An interpretation on Ωis an interpretation of the language of Twhose universe is Ω.T is interpretable on Ωif there exists an interpretation on Ωwhich is model of T. Roughly speaking, an interpretation is a (logical) interpretation which interprets spatial entities as open sets in the space, and relations as spatial relations, often on spatial regular regions. If an abstract extension of a standard QSR theory is obtained, it Fig.1. Semantic approach to a geodemographic class [11] is necessary to extend the standard interpretation by interpreting the new concepts or relationships as spatial regions and relations respectively. 2.1 A Motivating Example The needs of generic extensions of (classic) qualitative reasoning theories comes from the analysis of spatial relationships partially defined by different specifications. For example, in [11] authors show how to build a (semantic web) ontology from a stateof-art geodemographicsystem. Such kind of systems are composed by high-level specifications of spatio-temporal and geodemographic features. Geodemographic classes extracted from the system are underspecified by the formalization of a number of geographic, demographic and sociological restrictions that really do not define the intent of geodemographic specialist (see Fig. 1). Therefore, when automated reasoning work on specifications poor results are obtained: formal class can not soundly interpreted as geodemographicexpert desires, which really represents a vague region contained in the intersection of a number of anonymous classes. The refinement of geodemographicontologies can not be sufficient if the system can not reason with rough, generic spatial relations which provides a basic spatial calculus. The selection of QSR for refining ontologies was showed in a range of papers [6,9,2,3] in which are presented both the foundational issues as well as their applications. The paper [3] describes an intelligent interface (called Paella), based on qualitative spatial reasoning which is designed to (spatially) reason with ontology classes (see [2] for an application). The refining cycle to be applied (once extended standard qualitative reasoning to work with the new kind of spatial entities) is represented in Fig. 2. It can be considered other possibility consisting on the refinement of the definition by means of the combined use of two or more classifier systems (and the sound topology) [24]. However the qualitative nature of ontological definitions discourages this approach. Standard mereotopological interpretation leads an abstract spatial configuration which Fig.2. Augmenting reasoning cycle with extended spatial reasoning [3] has to be used by purely formal methods (because the spatial intuition may fail on these new relationships). Therefore, it needs a new formal framework where the reasoning is founded with strong logical theories on spatial reasoning, which must be topologically interpretable in turn. 2.2 The Mereotopological Theory RCC RCC theory [12], a mereotopological approach to QSR, describes topological features of the spatial relations. It has been useful in several fields of Artificial Intelligence such as Geographic Information Systems (GIS) and Spatial Databases (see e.g. [16]) It allows us both to reason on spatial regions and to interchange knowledge between ontologies and their spatial models. We consider a ground relation, the connection between two regions, which enjoys the reflexive and symmetrical properties. The meaning of connection is: the topological closures of two connected regions intersect. The set of axioms expressing the properties and definitions of the remaining relations (Fig. 3 (left) conforms the set of axioms of RCC (see [12]). On one hand, the set of the eight binary relations depicted in Fig. 3 is denoted by RCC8. These relations are jointly exhaustive and pairwise disjoint (JEPD) and RCC8 is regarded a calculus for Constraints Satisfaction Problems (CSP) (see e.g. [22]). On the other hand, there is another interesting calculus, RCC5={DR,PO,PP,PPi,EQ}. The difference between them is that while the former allows us to enrich the representation of knowledge by using frontiers of the regions, the latter do not. This fact will be discussed next. Although it has been empirically established [19] that RCC8 is more suitable than RCC5 for the representation of topological relations discriminated by humans, both of them are used here: RCC5 is appropriate for solving CSPs associate to Fig.3. Axioms of RCC (top) and RCC8 spatial relations (bottom) a mereotopological representation and RCC8 is useful to design a rich translation of a spatial representation to the ontology code. Models of RCC have been deeply studied from different viewpoints [20,22]. The study of the lattice of spatial relationships of extensions of RCC was made in [10]. The last work raise several questions about the relation between the original theory and its extensions. This can be studied from the QSR paradigm, or from the logical consequences of the extension of the theory (see e.g. [15] for the combination of RCC and reasoning about qualitative size and [9] for the same problem). 3 Background: Lattice-Categorical Extensions An essential requirement to a qualitative theory should be that if it is possible to entail the basic relationships among the concepts considered. For example, RCC entails both the relationship between the spatial defined relations (which has lattice structure) and the transition calculus [21]. Likewise the extension should satisfy the same requirement. Inspired by foundational questions on the Semantic Web [1], in [10] a formal definition of robust ontology is proposed, called lattice categorical extension [8] used for computing a range of RCC-extensions used in the paper. Alattice categorical theory is the one that proves the lattice structure of its basic relations. Formally, given a fixed language, let C={C1,...,C n}bea(finite)setof concept symbols, let Tbe a theory. Given Ma model of T,M|=T, we consider the structure L(M,C), in the language LC={,⊥,≤}∪{c1,...,c n}, whose universe are the interpretations in Mof the concepts (interpreting cias CM i), is M,⊥is ∅and ≤ is the subset relation. We assume that L(M,C)is requested to have a lattice structure for every theory we consider. The relationship between L(M,C)and the model Mitself is based on that the lattice Lcan be characterized by a finite set of equations EL, plus a set of formulas ΘC categorizing the lattice under completion, that is, ΘCincludes the domain closure axiom, the unique names axioms and, additionally, the axioms of lattice theory. Definition 2. Let Ebe a LC-theory. We say that Eis a lattice skeleton (l.s.) for a theory Tif Everifies that –There is M|=Tsuch that L(M,C)|=E∪ΘC, and –E∪ΘChas an unique model (modulo isomorphism). Every consistent theory has a lattice skeleton [10]. The existence of non equivalent l.s. makes it difficult to reason with the relations, while the existence of only one would make it easy due to the relationship among the relations is the same in any model of T. Definition 3. Tis called a lattice categorical (l.c.) theory if every pair of lattice skeletons for Tare equivalent modulo ΘC. Note also that every consistent theory Thas an extension Twhich is lattice categorical: it suffices to consider a model M|=T, and then to find a set Eof equations such that ΘC∪Ehas L(M,C)as only model. A method -assisted by ATP an MFfor obtaining the skeleton is described [10]. Finally, we can give a formalization of robust ontological extension, based in the categorical extension of the ontology: Definition 4. Given two pairs (T1,E 1),(T2,E 2)we will say that (T2,E 2)is a lattice categorical extension of (T1,E 1)with respect to the sets of concepts C1and C2respectively, if C1⊆C 2and L(T2,C2)is an E1-conservative extension of L(T1,C1). The most important feature of l.c. theories is that this allows use only the lattice relationships for reasoning with the relations. Lattice categoricity has been used for extending ontologies by decision of the user [10], motivated by data and designed by the user [8], data-driven [7] and ontology merging [9]. In [10] l.c. extensions of RCC for supporting undefinition are computed: those that insert the undefinition into RCC8 calculus, so obtaining a new JEPD set. There exist other kind of extensions designed for other uses. See [8] for details. Theorem 1. [10] There are only eight l.c. extensions of the lattice of RCC by insertion of a new relation Dsuch that RCC8∪{D}is a JEPD set. The analysis of the extensions (fig. 4) suggests us that the new relations represent undefinition up to a degree. 4 Interpreting with Pulsation/Contraction The above result is an example of a purely logical result obtained by automated reasoning. As it is commented the method ensures the correctness of the result. It is necessary to complete the study by interpreting (if possible) the new elements (and the reinterpreting the older ones). This way it qualifies the designer to use it as QSR theory. In order to obtain specific interpretations, it need to work with concrete spaces. In this section we illustrate this idea by using R(Ω)as the set of regular sets of the topological space Ω. Fig.4. The eight lattice describing the l.c. extensions of RCC by a undefinition relation Definition 5. Apulsation on a topological space Ω=(X,T)is a map σ:R(Ω)−→ R(Ω)such that the closure of σ(X)contains that of X;X⊂σ(X). The pair (Ω,σ) where Ωis nontrivial, connected and regular is a topological space with pulsation. The interpretation on these spaces is based on considering the pairs (x, σ(x)). Theorem 2. Seven of the eight extensions from theorem 1 are interpretable in topological spaces with pulsation. Proof. We denote by RΩ(R∈RCC) the natural interpretation of Rin the topological space Ω. For the sake of simplicity, we make use of the following conventions, Rσ(a, b):=R(σ(a),σ(b)) and RCC8σ:=  R∈RCC8 Rσ Let (Ω,σ)be a topological space with pulsation σ.Ωkis defined like the structure on the language of RCC +{Ik}where k∈{1,2,3,4,5,7,8}, and for every R∈R RCC, the interpretation of Rin Ωkis obtained by combination of regions. It only shows two of such interpretations. The others explanations are similar. L1:RΩ1=RΩif R∈R RCC {NTPP,TPP},TPPΩ1=TPPΩ∩TPPσ, NTPPΩ1=NTPPΩ∩NTPPσand I1 Ω1=(TPPΩ∩(RCC8σ{TPPσ}))∪(NTPPΩ∩(RCC8σ{NTPPσ})) L3:RΩ3=RΩif R∈R RCC {TPPi,NTPPi},TPPi Ω3=TPPi Ω∩TPPi σ, NTPPi Ω3=NTPPi Ω∩NTPPi σand I3 Ω3=(TPPi Ω∩(RCC8σ{TPPi σ}))∪(NTPPi Ω∩(RCC8σ{NTPPi σ})) The relation I6does not have interpretation on pulsation. It has to use contraction. Definition 6. Acontractionin a topologicalspace Ω=(X,T)is a map σ:R(Ω)−→ R(Ω)such that (ξ(A)) ⊂Afor each Awith nonempty inner. The pair (Ω,ξ)where Ω is nontrivial, connected is called a topological space with contraction. Theorem 3. I6is interpretable in a topological space with contraction Fig.5. Interpretation of the relations by undefintion (I6by contraction.The rest by pulsation) Proof. Given (Ω,ξ)define Ω6the structure of the language RCC +{I6}as follows: –RΩ6=RΩif R∈{C, DR, EC, DC} –RΩ6=RΩ∩Oξif R∈R RCC {C, DR, EC, DC} –I6Ω6=OΩ∩DRξ Fig. 5 summarizes the interpretations. In fact, it verifies: Theorem 4. The set of interpretations Ωk,k∈{1,2,...,8}defined above entails the lattice structure Lkdepicted in the Fig. 4. It suffices to check exhaustively the properties of the reticle according to the corresponding interpretation. The details of such long and tedious process are omitted. Corollary 1. The set RCC8+{Ik}is a JEPD set under the interpretation Ωk,for k={1,2,...,8}. The interpretations correspond, in essence, to a skeleton of every possible extension of RCC. The skeleton (the set of lattice equations characterizing the lattice) can be obtained by using a model finder (MACE4 in our case), but the calculus is out of the scope of this paper. 5 Building the New Transition Tables One of the advantages of interpreting l.c. extensions is that it allows to build a transition table for the new theory, particularly in the case of the news JEPDs. As for RCC8, it is Table 1. Composition table for the extension corresponding to L1 possible to provethe transition table for the new JEPD sets RCC8+Ik,k ={1,...,8}. To illustrate the method, the table for RCC8+{I1}is computed. Table 1 shows the transition table for RCC8+{I1}. The part of the table that corresponds(fits) to the composition of relations RΩ 1,R Ω 2 where R1,R 2∈RCC8, coincides with the table we obtain for RCC8, except: –If from the composition of two relations R1,R 2in RCC8is obtained TPP or NTPP (or both of them),then it will appear TPP or NTPP (or both of them), besides the relation I1. –As a consequence of that, if in the composition table of RCC8the result of composing two relations is RCC8, then, the result is the set RCC8+{I1},whichwe have denoted as RCC8[I1]. In table 2 it shows an example of calculus. 6 Interpretation in the “egg-yolk” Approach In this section another interpretation, in the egg-yolk paradigm [13] is studied. This is naturally related with the pulsation one. A complete picture of the relationship between undefinition relations is given (as well as with RCC5) instead of a separate interpretation for each one. In egg-yolk paradigm, regions (which we call e-y regions)have undetermined boundaries (a ‘vague region’), and they are represented by a pair of concentric regions with determinate boundaries (‘crisp regions’), which provide limits (not necessarily the tightest limits possible) on the range of indeterminacy. In this paradigm