Exporting an Arithmetic Library from Dedukti to HOL

Abstract : Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT∀ βδ logic, an extension of the Simple Type Theory that has been encoded in the logical framework Dedukti. We show that this new logic is a good candidate to export proofs to other provers. As an example, we show how this logic has been encoded into Dedukti and how we used it to export proofs to the HOL family provers via OpenTheory.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01668250
Contributeur : François Thiré <>
Soumis le : mardi 19 décembre 2017 - 22:40:49
Dernière modification le : jeudi 11 janvier 2018 - 06:20:14

Fichier

sttforall-fscd.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01668250, version 1

Citation

François Thiré. Exporting an Arithmetic Library from Dedukti to HOL. 2017. 〈hal-01668250〉

Partager

Métriques

Consultations de la notice

26

Téléchargements de fichiers

4