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_Mereology is a Coq library created by R. Dapoigny and P. Barlatier whose purpose is to implement the alternative to Set Theory of Stanislaw Lesniewski. It is part of an ongoing project using the Coq language and called KDTL (Knowledge-based Dependently Typed Language) to build an alternative to Description Logics. The developed theory is close to the analysis of Denis Miéville (1984) in his book “Un développement des systèmes logiques de Stanislaw Lesniewski”. It is a theoretical construct which relies on three dependent levels, logic (a.k.a. Protothetic), the Lesniewski Ontology (LO) and mereology. Each level incorporates a minimal collection of axioms, protothetic and ontological definitions and a set of theorems together with their intuitionist proofs. 


  • Coq (> v8.4)