Proof reconstruction (preliminary version).
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.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...