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 first extended for a 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. We have proved that geometry can be interpreted within topology by introducing the notion of saturated interior point from which open sets, interior, boundary and topological complement are defined. The file created by R. Dapoigny and P. Barlatier is expressed in Dependent Type Theory (Coq) and based on characteristic functions to formulate appropriate definitions. It relies on singular and plural names, restricts quantification on them and therefore, promotes the use of automated theorem provers such as those included with CoqHammer.
Requirements
- Coq (> v8.12)
Installation
- Click here to download the extended topological version of Tarski’s geometry of solids.
- 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.