Embedding RCC8D in the collective spatial logic CSLCS

Discrete mereotopology is a logical theory for the specification of qualitative spatial functions and relations defined over a discrete space, intended as a set of basic elements, the pixels, with an adjacency relation defined over it. The notions of interest are that of region, intended as an arbitrary aggregate of pixels, and of specific relations between regions. The mereotopological theory RCC8D extends the mereological theory RCC5D--a theory of region parthood for discrete spaces--with the topological notion of connection and the remaining relations (disconnection, external connection, tangential and nontangential proper parthood and their inverses). In this paper, we propose an encoding of RCC8D into CSLCS, the collective extension of the Spatial Logic of Closure Spaces SLCS. We show how topochecker, a model-checker for CSLCS, can be used for effectively checking the existence of a RCC8D relation between two given regions of a discrete space.