基于Coq的塔斯基 mereogeometry 公理化
A Coq-based Axiomatization of Tarski's Mereogeometry
AI总结：
本文基于Coq语言，对塔斯基的mereogeometry进行公理化，通过类型论方法提供更清晰的基础，用三个公理替代四个，并支持空间推理与莱斯内维斯基系统兼容。
摘要：
在过去的十年中，定性空间推理领域对mereogeometry（一种由塔斯基发起的理论）重新产生了兴趣。mereogeometry依赖于mereology（莱斯内维斯基的关于部分与整体的理论），并进一步扩展了几何原始概念和适当的定义。然而，大多数方法（i）脱离了莱斯内维斯基原始的mereology，不假设通常的集合作为基础；（ii）将mereology的逻辑能力限制为仅仅部分-整体关系的理论；（iii）需要引入连接关系。此外，塔斯基的奠基性论文显示出不清晰的基础，我们主张mereogeometry如塔斯基所引入的，更适合扩展莱斯内维斯基的整个理论。为此，我们更深入地研究了一种类型论表示空间，更接近莱斯内维斯基的原始思想，并用Coq语言表达。我们证明了（i）它可以有更清晰的基础；（ii）它可以用三个公理而不是四个公理来建立；（iii）它可以作为空间推理的基础，完全符合莱斯内维斯基的系统。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
