Using Temporal Logic for Spatial Reasoning: Spatial Propositional Neighborhood Logic

It is widely accepted that spatial reasoning plays a central role in artificial intelligence, for it has a wide variety of potential applications, e.g., in robotics, geographical information systems, medical analysis and diagnosis. As noticed by many authors, spatial and temporal reasoning have a close connection. In this paper we propose a new, semi-decidable, modal logic for spatial reasoning through directional relations, which is able to express meaningful spatial statements. Spatial propositional neighborhood logic can be polynomially reduced to a decidable temporal logic based on time intervals preserving, at least, valid formulas. Thanks to such a reduction, we are able to reuse a sound and complete tableaux method in order to reason with spatial propositional neighborhood logic; to the best of our knowledge, there are practically no previous attempts of devising automatic reasoning methods for spatial reasoning