A Coq-based Axiomatization of Tarski's Mereogeometry
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914166048030720 |
|---|---|
| author | Barlatier, Patrick Dapoigny, Richard |
| author_facet | Barlatier, Patrick Dapoigny, Richard |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_16705 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Coq-based Axiomatization of Tarski's Mereogeometry Barlatier, Patrick Dapoigny, Richard Logic in Computer Science Logic F.4.1; F.4.2; I.2.3; I.2.4 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. |
| title | A Coq-based Axiomatization of Tarski's Mereogeometry |
| topic | Logic in Computer Science Logic F.4.1; F.4.2; I.2.3; I.2.4 |
| url | https://arxiv.org/abs/2511.16705 |