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

Tarski_Mereogeometry is a Coq library created by R. Dapoigny and P. Barlatier whose purpose is to implement the mereogeometry of Stanislaw Lesniewski. It is the second part of a project using the Coq language and called KDTL (Knowledge-based Dependently Typed Language) to build an alternative to Description Logics. The primary objective is to provide a basis for spatial reasoning without using any connection primitive as in mereotopology. The developed library is a theoretical construct which relies on three axioms and on a small set of definitions. The last axiom of Tarski’s version is provable from definitions according to the Lesniewski’s spirit. 


  • Coq (> v8.4)