Topology as an extension of Mereology
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 expressing a classical version of topology using additional definitions such as the interior, boundary and closure. The file created by R. Dapoigny and P. Barlatier proposes a model of Topology expressed in Dependent Type Theory (Coq) and based on characteristic functions to formulate the above definitions. It focuses on proofs and usability of the model in formal ontologies. Our approach relies only on singular names which restricts quantification on them and therefore, it promotes the use of automated theorem provers such as those included in CoqHammer.
Requirements
- Coq (> v8.12)
Installation
- Click here to download the extension of Mereology to Topology.
- 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.