A complete axiom system for polygonal mereotopology of the real plane (Q1277333)

This paper proposes a calculus for mereotopological reasoning in which 2-dimensional spatial regions are treated as primitive entities. The syntactical foundation is the (first-order) language \({\mathcal L}\) of Boolean algebras with a distinguished predicate \(c(x)\). Two formal models for the mereotopological language \({\mathcal L}\) are presented: In an interpretation \({\mathcal R}\) for \({\mathcal L}\) the polygonal open subsets of the real plane \(\mathbb{R}^2\) serve as elements of the domains; and the predicate \(c(x)\) is read as ``region \(x\) is connected''. (Function-symbols +, \(\cdot\) and \(-\) and constants 0 and 1 are given their meaning in terms of a Boolean algebra of polygons.) Another interpretation \({\mathcal S}\) for \({\mathcal L}\) is based on the closed plane \(\mathbb{R}^2\cup \{\infty\}\), under the usual topology. This model \({\mathcal S}\) is isomorphic to \({\mathcal R}\). The mereotopological calculus \({\mathcal C}\) is determined by a set of (eleven) axioms and rules of inference stated in the language \({\mathcal L}\). The main part of this paper is to show that the axiom system \({\mathcal C}\) is sound and complete with respect to the given interpretations \({\mathcal R}\) and \({\mathcal S}\). These properties of the axiom system \({\mathcal C}\) are useful for theoretical aspects and for applications of the mereotopology. For such theoretical expositions see, among others, papers by \textit{B. L. Clarke} [Note Dame J. Formal Logic 22, 204-218 (1981; Zbl 0438.03032) and ibid. 26, 61-75 (1985; Zbl 0597.03005)] and \textit{I. Pratt} and \textit{O. Lemon} [ibid. 38, 225-245 (1997; Zbl 0897.03014)] and relevant conference-reports.