Back to Search Start Over

Traduire l'univers des mathématiques en Dedukti, sans univers

Authors :
Ledein, Amélie
Butte, Elliot
Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)
Inria Saclay - Ile de France
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF)
Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Laboratoire Méthodes Formelles (LMF)
Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)
Timothy Bourke
Delphine Demange
Source :
JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.172-189
Publication Year :
2023
Publisher :
HAL CCSD, 2023.

Abstract

National audience; Ces dernières années, le nombre d'assistants à la preuve, de prouveurs automatiques et de vérificateurs de preuve n'a cessé de croître. L'un d'entre eux, le framework logique Dedukti, a pour objectif de rendre ces outils formels interopérables, c'est-à-dire rendre possible la réutilisation des preuves d'un outil A dans un outil B. Un autre outil formel, Metamath, a la particularité d'être à la 4e place dans la liste des systèmes possédant le plus grand nombre de preuves parmi la liste des 100 théorèmes à prouver de Freek Wiedijk, tout en étant constitué de très peu de fonctionnalités : pas de type dépendant, pas de polymorphisme, ni de notion d'univers. Afin d'agrémenter le nombre de preuves qu'il est possible de traduire dans Dedukti, nous présentons Mathiilde, un traducteur automatique de Metamath vers Dedukti. Comme ce traducteur peut utiliser deux encodages différents de Metamath vers Dedukti, nous discutons les avantages et les inconvénients du point de vue de l'interopérabilité.

Subjects

Subjects :
[INFO]Computer Science [cs]

Details

Language :
French
Database :
OpenAIRE
Journal :
JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, JFLA 2023-34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.172-189
Accession number :
edsair.od.......165..6b217ba8d9fdd81211ba7a1598d829e3