Total: 1
Qualitative spatial representation approaches which rely on Goodman-style predicative mereological theories and on a pseudo-topology, often causes some problems either for their use as a meta-information for knowledge conceptualization in advanced geometric reasoning, since they lack Euclidean geometry and fully-fledged topological spaces in the classical sense. Therefore, this paper seeks to extend 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 lambda-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 Lesniewski’s mereology, and despite the fact that lambda-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.