KDTL MEREO

Accord

Ce logiciel est fourni « en l’état » et sans garantie d’aucune sorte. Les auteurs de ce logiciel ne garantissent en aucune façon ni la bonne exécution, ni la bonne génération de données en utilisant ce logiciel, que ce soit en termes de fiabilité, précision ou d’aptitude à l’emploi. Vous assumez entièrement les risques directs ou indirects, qui peuvent ou non résulter de l’utilisation correcte ou non de ce logiciel, même si les auteurs ont été informés des possibilités d’un tel dommage. Ni les auteurs, ni l’Université Savoie Mont Blanc, ni aucune autre personne reliée à ce logiciel de près ou de loin ne peuvent assumer cettte responsabilité d’aucune manière.

En téléchargeant, puis en installant ce logiciel, vous acceptez les termes de cet accord. Si vous ne l’acceptez pas, ne continuez pas avec le téléchargement.

Information générale

Lesniewski_Mereology est une librairie Coq crée par R. Dapoigny et P. Barlatier qui contient une alternative à la théorie des ensembles de Stanislaw Lesniewski. Elle fait partie d’un projet utilisant le langage Coq et appelé KDTL (Knowledge-based Dependently Typed Language) pour construire une alternative aux logiques de description. La théorie développée ici, repose sur l’analyse détaillée dans l’ouvrage « Un développement des systèmes logiques de Stanislaw Lesniewski » de Denis Miéville (1984). Elle présente trois niveaux dépendants, la logique (aka Protothétique), l’ontologie de Lesniewski (LO) et la méréologie. Chacun des niveaux contient un nombre minimal d’axiomes, des définitions protothétiques et ontologiques ainsi qu’un certain nombre de théorèmes et leur démonstration (preuves en logique intuitionniste).

Exigences

  • Coq (v8.4 ou supérieur)

Installation