Encyclopédie en ligne de démonstrations formelles - Archive ouverte HAL Access content directly
Master Thesis Year : 2018

Encyclopédie en ligne de démonstrations formelles

(1)
1

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.
Fichier principal
Vignette du fichier
Rapport-walid-moustaoui.pdf (4.28 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01975446 , version 1 (09-01-2019)

Identifiers

  • HAL Id : hal-01975446 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More