A Topological Rewriting of Tarski's Mereogeometry
Patrick Barlatier, Richard Dapoigny
TL;DR
The paper tackles the limitations of qualitative spatial reasoning by building a unified, point-free framework that derives topological reasoning from Leśniewski's mereology and Tarski's geometry of solids within the Coq dependently typed setting. By extending the $\lambda$-MM library with interior, boundary, and closure, it shows mereological classes correspond to regular open sets, enabling a topology on named entities and a clean interpretation of open regions. It then embeds Tarski's geometry as a topological subspace, formalizes points as filters of concentric balls, and proves three original postulates along with the $T_2$ (Hausdorff) property, yielding a topology of regions that aligns with Euclidean intuition ($\mathbb{R}^3$) via a conjectured homeomorphism. The approach promises enhanced expressiveness for GIS, spatial ontologies, architectural validation, and autonomous navigation, and offers a foundation for neuro-symbolic AI by supplying a robust symbolic scaffold for spatial reasoning.
Abstract
Qualitative spatial models based on Goodman-style mereology and pseudo-topology often pose problems for advanced geometric reasoning, as they lack true Euclidean geometry and fully developed topological spaces. We address this issue by extending an existing formalization grounded in a dependent type theory using the Coq proof assistant, together with a Whitehead-like point-free interpretation of Tarski's geometry. More precisely, we build on a library called lambda-MM to formalize Tarski's geometry of solids by investigating an algebraic formulation of topological relations on top of the mereological framework. Since Tarski's work is rooted in Lesniewski's mereology, and given that lambda-MM currently provides only a partial implementation of Tarski's geometry, the first part of the paper completes this framework by proving that mereological classes correspond to regular open sets. This yields a topology of individual names that can be extended with Tarski's geometric primitives. Unlike classical approaches in qualitative logical theories, we adopt a solution that derives a full topological space from mereology together with a geometric subspace, thereby increasing the expressiveness of the theory. In the second part, we show that Tarski's geometry forms a subspace of this topology in which regions correspond to restricted classes. We also prove three of Tarski's original postulates, reducing his axiomatic system, and extend the theory with the T2 (Hausdorff) property and additional definitions.