Reconstruction de preuves pour les formules quantifiées et ensemblistes
Résumé
La reconstruction de preuve est une technique qui combine un prouveur interactif et un prouveur automatique de manière correcte. L'utilisateur bénéficie ainsi de l'expressivité du prouveur interactif et de l'automatisation du prouveur automatique. Nous présentons une implémentation de la reconstruction de preuve entre Isabelle et Harvey.
Domaines
Informatique et langage [cs.CL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...