Study For Qualitative Spatial Logic Based On Direction Relation

Recently, spatial information is more and more important in different regions. As an aspect of spatial reasoning, the representation and modeling of spatial knowledge is very important. Logic method is one of the main methods to study on spatio-temporal knowledge research; modal logic is a language which is used to express knowledge.The relations with spatial property between spatial objects are called spatial relations. In modal logic of single aspect of spatial information, most of previous work is based on topologic relations. However, because most of them considering simple regions, they have defects of representation ability. Direction relation is one important aspect of spatial relations and widely used. The logic based on direction relations has low complexity. It is not only effective to express natural space abstractly, but also can express meaningful spatial statements. As for directional relations we mention Venema's compass logic and Morales'spatial propositional neighborhood logic (SpPNL for short). In compass logic, propositional variables are interpreted as points in the Euclidean two-dimensional space. In SpPNL, the object they considered is the minimum bounding rectangle (MBR for short). Compass logic is undecidable whereas SpPNL is semi-decidable.Based on SpPNL, we propose a spatial logic named SpPNL(D) by adding modalities D and U to SpPNL, for spatial reasoning through directional relations. We constructed the axiom system of spatial neighborhood logic, studied the express ability, decidability, and deducing system for it.The main work of this paper is as follows:Firstly, we show a short introduction about the significance of this paper. We analyzed and summarized the development of spatial logic in recent years, presented the trend of spatial logic, and found the problem of it. Secondly, we introduced the model of direction relations. We review the developing process of modal logic, show the possible worlds semantic of modern modal logic, and introduce the representative systems of modern modal logic. We show the topologic relations and direction relations in spatial relations. Then, we propose four logic frames: van Benthem minimal rectangle structure, van Benthem pre-rectangle structure, minimal rectangle structure, and pre-rectangle structure. These structures are based on direction relations, and proposed by Allen interval algebra and minimal bound rectangle. We introduced spatial logic SpPNL and some concept of tableau algorithm.Thirdly, we introduce the semantic and syntax of SpPNL(D), propose the axiom system of the logic, and prove that the logic is complete and decidable.This paper shows the semantic and syntax of SpPNL(D), and construct the axiom system of that. We show the condition of abstract spatial frames, prove a representation theorem for abstract spatial frames. Considering van Benthem minimal rectangle structure and other structures, we proved these structures can transform one another by Segerberg's bulldozing and other methods. The logic is complete in pre-rectangle structure through Sahlqvist's complete theorem. What's more, because all pre-rectangle structures can be enumerated, the logic is decidable. At last, we have inclusion that SpPNL(D) is complete and decidable, which is important in spatial reasoning.Fourthly, we introduce the express ability of SpPNL(D). We study the expressive power of SpPNL(D), and show that it is able to express meaningful spatial statements. We compare the logic with the well-known algebraic spatial reasoning system called rectangle algebra. There are 25 basic relations that can be directly expressed in the logic. We divide the leaving relations into two groups, partially indirect relations and indirect relations. We express the two relation groups by simulating nominal. Despite the logic is simplicity, it is powerful enough to solve any rectangle algebra constraint network.Fifth, we devise a sound and complete tableaux-based deduction system for the logic. Description logics are closely related to modal logics, yet they have been developed independently. We give a tableau algorithm for SpPNL(D) reference to the description logic ALCNIR+, a description logic with transitive and inverse roles. We proved the algorithm is soundness and completeness. By the tableaux algorithms, well-formed formula can be proved the satisfiability.Sixth, we devised and implemented tableau algorithm system, and accomplished ig by MFC technology. The system proved that the tableau algorithm is able to deduce correctly and accomplishable.The spatial logics based on direction relations, although the express ability is powerful, most of which are not decidable. The compass logic is undecidable, and spatial propositional neighborhood logic is semi-decidable. We propose a spatial logic named SpPNL(D) by adding modalities D and U to SpPNL, for spatial reasoning through directional relations. The modal logic SpPNL(D) introduced in this paper, despite it is simplicity, is powerful enough to solve any rectangle algebra constraint network. Compare to SpPNL, it has simpler expressing form. We prove the represent theorem by showing the conditions of abstract spatial frame. Our logic and SpPNL are logics based on Allen interval algebra, expressing and reasoning the objects on bi-Euclid space. SpPNL is semi-decidable while SpPNL(D) is decidable. We can study other characters of logic such as complexity based on decidability. In a word, the study result of this paper can be applied to represent the meanful spatial informations, it have both theoretical and practical benefits.