Proof reconstruction for first-order logic and set-theoretical constructions
Clément Hurlin · 2006
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. 1