A Model for Mereology

Monadic Second-Order Mereology


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_v5.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 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 Monadic second order structure based on definitions in order to get rid of axioms and to allow for an incremental modelling of applications. The library is available in two files. The file Mereology_on_Onto_sets_v5.vo is the library file to be included in the header in order to use its content. The file Mereology_on_Onto_sets_v5.v contains the source code. Notice that since these files implement automation, they require the additional software CoqHammer v1.3.


  • Coq (> v8.12)