Tarski’s Geometry of Solids built on top of Mereology
This work has given rise to an article in the international journal Logic and Logical Philosophy and its content can be accessed online here.
Agreement
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. It relies only on singular names which restricts quantification on them and therefore, it promotes the use of automated theorem provers such as those included with CoqHammer.
We provide two codes corresponding respectively to two definitions for points, the first follows Tarski’s definition while the second uses saturated spheres and collective classes. Point definition corresponding to Tarski’s description:
∀ A A’. η A (Point A’) := η A’ balls ∧ η A (Concent A’)
Point definition corresponding to the paper version:
∀ A. η A Point := η A (stat_subsphere Gspace) ∧ η A (kl (Concent A))
All applications rely on one of these definition. A first geometric connective (the between relation) has already been added, leaving the user the ability to add its own connectives.
Requirements
- Coq (> v8.12)
Installation
- Click here to download Tarski’s geometry of solids with original definition of point.
- Click here to download Tarski’s geometry of solids with the alternative definition of point.
- Unzip the file content (e.g. with 7-zip) in your local directory.
- Start Coq.
- Open a new file and extend the code above with your own functions.