Skip to Main content Skip to Navigation
Reports

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

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/inria-00212213
Contributor : Clément Hurlin <>
Submitted on : Tuesday, January 22, 2008 - 3:24:13 PM
Last modification on : Thursday, March 5, 2020 - 4:51:36 PM
Long-term archiving on: : Thursday, September 27, 2012 - 5:38:54 PM

File

mr2.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

68

Files downloads

166