Proof reconstruction for first-order logic and set-theoretical constructions
Résumé
Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit of the expressiveness of the first tool and the automation of the latter. We present an implementation for proof reconstruction for first-order logic and set-theoretical constructions between Isabelle and haRVey.
Domaines
Logique en informatique [cs.LO]
Loading...