Skip to Main content Skip to Navigation
Conference papers

Preuves taillées en biseau

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/hal-01404935
Contributor : Martin Clochard <>
Submitted on : Tuesday, November 29, 2016 - 1:27:17 PM
Last modification on : Wednesday, September 16, 2020 - 5:26:19 PM
Long-term archiving on: : Monday, March 27, 2017 - 8:44:34 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01404935, version 1

Collections

Citation

Martin Clochard. Preuves taillées en biseau. vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France. ⟨hal-01404935⟩

Share

Metrics

Record views

293

Files downloads

141