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

Lesniewski’s Mereology is a Coq library created by R. Dapoigny and P. Barlatier whose main objective is to provide a tractable model of Stanislaw Lesniewski’s Mereology. For that purpose, the developed theory relies on Clay’s formulation of mereology based on characteristic functions to construct appropriate sets. Using a single axiom for partial order we prove  that this axiom is equivalent to the single axiom of mereology and then that it has a boolean model without zero. In addition, we have extended the model based on definitions in order to get rid of axioms and to allow for incremental modelling of applications. Furthermore, the base theory has been also proved in Isabelle/HOL with full automation.


  • Coq (> v8.9)