Encyclopédie en ligne de démonstrations formelles
Abstract
Logipedia is an online encyclopedia of formal demonstrations in Dedukti as well as demonstrations translated from Dedukti to other languages (such as Coq, Matita, PVS, Lean, OpenTheory). A formal demonstration is a finite sequence of propositions such as we have :
— Axioms
— Parameters
— Theorems
And sometimes definitions in the context of concrete demonstrations So the purpose of Logipedia is to store all this data, as well as their translation to other languages. And to post them through a website. To meet these expectations, I imported first of all the data in a database MongoDB. Then I created a dynamic website making several queries to the database to be able to display all the demonstrations.
Logipedia est une encyclopédie en ligne qui contient des démonstrations formelles exprimées en Dedukti ainsi que le traductions de ces démonstrations dans autres langages (tels Coq, Matita, PVS, Lean, OpenTheory). Une démonstration formelle est une séquence finie de propositions que chacune est déduite des prédédents par règle logique. Une librairie de démonstrations
contient
— des Théorèmes et leurs démonstrations,
— des Axiomes,
mais aussi
— des Paramètres,
— et des Définitions.
Donc le but de Logipedia est de stocker toutes ces données, ainsi que leurs traductions vers d’autres langages. Et de les afficher à travers un site web. Pour répondre à ces attentes, j’ai tout d’abord importé les données dans une base de données MongoDB. Puis j’ai créé un site web dynamique effectuant plusieurs requêtes vers la base de données pour pouvoir afficher toutes les démonstrations.
Origin : Files produced by the author(s)