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_DST_structurev1.v is a Coq library created by R. Dapoigny and P. Barlatier whose main objective is to provide a consistent structure of Mereology. For that purpose, the developed structure relies on the Distributive Set Theory (DST) expressed in Dependent Type Theory 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 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)