A Model for Tarski’s Geometry of Solids

Tarski’s Geometry of Solids built on top of Mereology


This software is provided « as is » and is without warranty of any kind. The authors of this software do not warrant, guarantee or make any representations regarding the use or results of use of this software in terms of reliability, accuracy or fitness for purpose. You assume the entire risk of direct or indirect, consequential or inconsequential results from the correct or incorrect usage of this software even if the authors have been informed of the possibilities of such damage. Neither the authors, the Université Savoie Mont Blanc, nor anybody connected to this software in any way can assume any responsibility.

General Information

The library of Mereology can be directly applied for a new specification of Tarski’ geometry of solids which has been proposed as a method for axiomatizing geometry using the notion of sphere (a.k.a. balls) as primitive instead of usual point based theories.  The file created by R. Dapoigny and P. Barlatier whose purpose is to propose a model of Tarki’s is expressed in Dependent Type Theory (Coq) and based on characteristic functions to formulate appropriate definitions. It focuses on proofs and usability of the model in formal ontologies. Our approach using mereological expressions for solids and points relies only on singular names which restricts quantification on them and as such, it promotes the use of automated theorem provers such as those included with CoqHammer. A first geometric connective (the between relation) has already been added, leaving the user the ability to add its own connectives.


  • Coq (> v8.12)