Modèle décidable de la Méréologie



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

Mereology_on_Onto_sets_v2.vo is a Coq library created by R. Dapoigny and P. Barlatier whose main objective is to provide a consistent structure for Mereology. For that purpose, the developed structure relies on the Monadic Second Order (MSO) translation of the basic part of Lesniewski’s Ontology and based on characteristic functions to construct appropriate sets. Using Clay’s single axiom for partial order, we prove  that this axiom is equivalent to the single axiom of mereology and then that the latter has a boolean model without zero. We have extended the MSO structure based on definitions in order to get rid of axioms and to allow for incremental modelling of applications. Furthermore, the base theory has also been proved in Isabelle/HOL for full automation.


  • Coq (> v8.9)