Reconstruction de preuves pour les formules quantifiées et ensemblistes

Clément Hurlin 1
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Type de document :
Rapport
[Travaux universitaires] 2006, pp.29-VII
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00212213
Contributeur : Clément Hurlin <>
Soumis le : mardi 22 janvier 2008 - 15:24:13
Dernière modification le : jeudi 11 janvier 2018 - 16:24:59
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 17:38:54

Fichier

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

Identifiants

  • HAL Id : inria-00212213, version 1

Collections

Citation

Clément Hurlin. Reconstruction de preuves pour les formules quantifiées et ensemblistes. [Travaux universitaires] 2006, pp.29-VII. 〈inria-00212213〉

Partager

Métriques

Consultations de la notice

44

Téléchargements de fichiers

114