A Topological Rewriting of Tarski's Mereogeometry

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 an underlying type theory using the Coq language, together with the Whitehead-like point-free Tarski's geometry. More precisely, we leverage an available library called λ-MM to formalize Tarski's geometry of solids by investigating an algebraic formulation of topological relations on top of the library. Given that Tarski's work is grounded in Leśniewski's mereology, and despite the fact that λ-MM barely implements Tarski's geometry, the first part of the paper supplements their work by proving that mereological classes correspond to regular open sets. It forms a topology of individual names extensible with Tarski's geometric primitives. Unlike classical approaches used in qualitative logical theories, we adopt a solution that enables the specification of a topological space from mereology and a geometric subspace, thereby enhancing the theory's expressiveness. Then, in a second part, we prove that Tarski's geometry forms a subspace of the previous topology in which regions are restricted classes. We prove three postulates of Tarski's work reducing his axiomatic system and extend the theory with the T2 (Hausdorff) property and additional definitions. Note. This is the full version of the paper accepted at AAAI-26. The arXiv version includes the complete list of authors. https://www.univ-smb.fr/listic/technologies/logiciels/modeles-decidables-pour-laspecification-d-ontologies/extending-tarskis-mereo-geometry-with-topologicaldefinitions/