Preuves taillées en biseau

Martin Clochard 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Nous présentons une extension que nous avons introduite dans la logique de l'outil Why3, dans le but de décrire les étapes de raisonnement à effectuer pour décharger une obligation de preuve. Cette extension prend la forme de deux nouveaux connecteurs, que nous appelons des indicateurs de coupure. Nous montrons que l'ajout de ces deux connecteurs permet d'encoder les étapes de raisonnement d'une preuve à l'intérieur d'une formule. En particulier, cet ajout donne la possibilité d'utiliser directement la syntaxe des formules comme langage de preuve. Cette approche apporte un mécanisme léger de preuve déclarative dans un environnement où les prouveurs sont utilisés comme des boîtes noires. De plus, ce mécanisme permet une restriction de la portée des lemmes intermédiaires, évitant ainsi la saturation des prouveurs automatiques.
Type de document :
Communication dans un congrès
vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France. vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), 〈http://jfla.inria.fr/2017/〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01404935
Contributeur : Martin Clochard <>
Soumis le : mardi 29 novembre 2016 - 13:27:17
Dernière modification le : jeudi 15 juin 2017 - 09:08:46
Document(s) archivé(s) le : lundi 27 mars 2017 - 08:44:34

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01404935, version 1

Citation

Martin Clochard. Preuves taillées en biseau. vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France. vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), 〈http://jfla.inria.fr/2017/〉. 〈hal-01404935〉

Partager

Métriques

Consultations de
la notice

157

Téléchargements du document

70