Dedukti:un vérificateur de preuves universel

Ali Assaf (1) , Raphaël Cauderlier (1) , Ronan Saillard (2, 1)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 CRI - Centre de Recherche en Informatique

Dedukti est un vérificateur de types pour le λΠ-calcul modulo, un formalisme alliant types dépendants et réécriture qui permet d’exprimer et de vérifier les preuves de nombreux systèmes logiques.Nous proposons d’utiliser Dedukti comme un vérificateur de preuves universel en traduisant HOL, Coq et FoCaLize vers Dedukti.

Domaines: Théorie et langage formel [cs.FL]; Logique en informatique [cs.LO]

Ali Assaf, Raphaël Cauderlier, Ronan Saillard. Dedukti:un vérificateur de preuves universel. Journées nationales GDR - GPL - CIEL - AFADL, Apr 2013, Nancy, France. ⟨hal-01086609⟩