3 crucial points for the use of formal methods are expressiveness, automation and soundness. Yet, neither interactive nor automatic tools bring these three qualities together. Proof reconstruction, a technique which combines an interactive and an automatic tool is a possible answer to this challenge. In this talk, we describe an implementation of proof reconstruction for first-order logic and set-theoretical constructions between Isabelle and haRVey.
The article can be found there.