A Complete Axiom System for Polygonal Mereotopology of the Real Plane

This paper presents a calculus for mereotopological reasoning in which two-dimensional spatial regions are treated as primitive entities. A first order predicate language with a distinguished unary predicate c(x), function-symbols , · and – and constants 0 and 1 is defined. An interpretation for is provided in which polygonal open subsets of the real plane serve as elements of the domain. Under this interpretation the predicate c(x) is read as region x is connected and the function-symbols and constants are given their meaning in terms of a Boolean algebra of polygons. We give an alternative interpretation based on the real closed plane which turns out to be isomorphic to A set of axioms and a rule of inference are introduced. We prove the soundness and completeness of the calculus with respect to the given interpretation.