Sciweavers

CADE
2011
Springer
12 years 5 months ago
Extending Sledgehammer with SMT Solvers
Abstract. Sledgehammer is a component of Isabelle/HOL that employs firstorder automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically s...
Jasmin Christian Blanchette, Sascha Böhme, La...