Axiomatizing Discrete Spatial Relations

Qualitative spatial relations are used in artificial intelligence to model commonsense notions such as regions of space overlapping, touching only at their boundaries, or being separate. In this paper we extend earlier work on qualitative relations in discrete space by presenting a bi-intuitionistic modal logic with universal modalities, called UBiSKt. This logic has a semantics in which formulae are interpreted as subgraphs. We show how a variety of qualitative spatial relations can be defined in UBiSKt. We make essential use of a sound and complete axiomatisation of the logic and an implementation of a tableau based theorem prover to establish novel properties of these spatial relations. We also explore the role of UBiSKt in expressing spatial relations at more than one level of detail. The features of the logic allow it to represent how a subgraph at a detailed level is approximated at a coarser level.