HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions

Clément Hurlin Amine Chaib Pascal Fontaine 1 Stephan Merz 1 Tjark Weber
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit from the expressiveness of the first tool and the automation of the latter. We present an implementation of proof reconstruction for first-order logic and set-theoretical constructions between the interactive theorem prover Isabelle and the automatic SMT prover haRVey.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00186638
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Saturday, November 10, 2007 - 2:47:17 PM
Last modification on : Friday, February 4, 2022 - 3:22:38 AM

Identifiers

  • HAL Id : inria-00186638, version 1

Collections

Citation

Clément Hurlin, Amine Chaib, Pascal Fontaine, Stephan Merz, Tjark Weber. Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions. The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13. ⟨inria-00186638⟩

Share

Metrics

Record views

101