Proof reconstruction (preliminary version). - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1996

Proof reconstruction (preliminary version).

(1)
1

Résumé

In the field of formal methods, rewriting techniques and provers by consistency in particular appear as powerful tools for automating deduction. However, these provers suffer limitations as they only give a (non-readable) trace of their progress and a yes/no answer where the user would expect a detailed explicit proof. Therefore, we propose a general mechanism to build an explicit proof from the running of a generic class of inductionless induction provers. We then show how it applies to Bouhoula's SPIKE prover, and give examples of proofs built by this method.
Dans le domaine des méthodes formelles, les techniques de réécriture et les prouveurs par récurrence implicite sont des outils puissants pour automatiser le processus de preuve. Cependant, ces prouveurs donnent une trace du déroulement de la preuve peu compréhensible, alors que l'utilisateur lambda aimerait avoir une preuve explicite détaillée. Nous proposons un mécanisme général permettant de construire une preuve explicite à partir de la trace du déroulement d'une preuve pour une classe générique de démonstrateurs par récurrence implicite. Nous montrons comment ce procédé s'applique au prouveur SPIKE de Bouhoula, et donnons des exemples de preuves construites par cette méthode.
Fichier principal
Vignette du fichier
RR1996-26.pdf (252.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101787 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101787 , version 1

Citer

Judicael Courant. Proof reconstruction (preliminary version).. [Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p. ⟨hal-02101787⟩
25 Consultations
18 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More