arXiv subjects

Patrick Barlatier

Publications and source records attributed to Patrick Barlatier.

3 recordsLinked to original sources

arXiv2026

From Regional Topology to Point-Class Topology in Tarski's Geometry of Solids

Tarski's geometry of solids reconstructs point-like entities from concentric families of spherical regions rather than taking points as primitive. We formalize this reconstruction in Coq within a nominal mereological framework inspired by Le\'sniewski, and study how the regional geometry of solids induces a topology on reconstructed point-classes without adding new point individuals. Three of Tarski's postulates concerning solids and interior points, P2--P4, are derived as theorems. We refine Tarski's interior-point notion and define a regional interior operator satisfying the four Kuratowski interior axioms, together with a boundary operation and an encoding of RCC8 relations. We then pass to the setoid of ball representatives modulo same_center. Each ball generates a stable basic point-plural GBasicPointSet(Q), and these plurals form a basis for a metatheoretic topology on reconstructed point-classes. This topology is Hausdorff under Tarski's separation axiom Three_points and non-discrete under the local richness hypothesis BallCenterBundle. Finally, geometric neighbourhoods yield a closure operator GClosurePoint satisfying the four Kuratowski closure axioms and respecting extensional point-set equality. The formalization thus verifies the passage from a regional topology of solids to a Hausdorff topology and neighbourhood closure on reconstructed point-classes.

math.LO↗

arXiv2025

A Coq-based Axiomatization of Tarski's Mereogeometry

During the last decade, the domain of Qualitative Spatial Reasoning, has known a renewal of interest for mereogeometry, a theory that has been initiated by Tarski. Mereogeometry relies on mereology, the Lesniewski's theory of parts and wholes that is further extended with geometrical primitives and appropriate definitions. However, most approaches (i) depart from the original Lesniewski's mereology which does not assume usual sets as a basis, (ii) restrict the logical power of mereology to a mere theory of part-whole relations and (iii) require the introduction of a connection relation. Moreover, the seminal paper of Tarki shows up unclear foundations and we argue that mereogeometry as it is introduced by Tarski, can be more suited to extend the whole theory of Lesniewski. For that purpose, we investigate a type-theoretical representation of space more closely related with the original ideas of Lesniewski and expressed with the Coq language. We show that (i) it can be given a more clear foundation, (ii) it can be based on three axioms instead of four and (iii) it can serve as a basis for spatial reasoning with full compliance with Lesniewski's systems.

cs.LO↗

arXiv2025

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 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.

math.LO↗