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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...