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 metadatas

https://hal.inria.fr/hal-01975446
Contributor : Bruno Barras <>
Submitted on : Wednesday, January 9, 2019 - 3:42:27 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM

File

Rapport-walid-moustaoui.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01975446, version 1

Citation

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

Share

Metrics

Record views

117

Files downloads

286