Skip to Main content Skip to Navigation
Master thesis

Encyclopédie en ligne de démonstrations formelles

Walid Moustaoui 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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.
Document type :
Master thesis
Complete list of metadata
Contributor : Bruno Barras Connect in order to contact the contributor
Submitted on : Wednesday, January 9, 2019 - 3:42:27 PM
Last modification on : Friday, April 30, 2021 - 9:53:39 AM


Files produced by the author(s)


  • HAL Id : hal-01975446, version 1


Walid Moustaoui. Encyclopédie en ligne de démonstrations formelles. Logique en informatique [cs.LO]. 2018. ⟨hal-01975446⟩



Record views


Files downloads