Sciweavers

CADE
2010
Springer
14 years 1 months ago
Sledgehammer: Judgement Day
Abstract. Sledgehammer, a component of the interactive theorem prover Isabelle, finds proofs in higher-order logic by calling the automated provers for first-order logic E, SPASS a...
Sascha Böhme, Tobias Nipkow