Sciweavers

Share
CADE
2011
Springer

Extending Sledgehammer with SMT Solvers

9 years 2 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 selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach. Remarkably, the best SMT solver performs better than the best ATP on most of our benchmarks.
Jasmin Christian Blanchette, Sascha Böhme, La
Added 13 Dec 2011
Updated 13 Dec 2011
Type Journal
Year 2011
Where CADE
Authors Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson
Comments (0)
books