Extending Sledgehammer with SMT Solvers

Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson

Document: DOI PDF

Abstract: Sledgehammer is a component of Isabelle/HOL that employs first-order 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.

Bibtex entry:

@inproceedings{
   author    = {Jasmin Christian Blanchette and Sascha B{\"o}hme and
                Lawrence C. Paulson},
   title     = {Extending {Sledgehammer} with {SMT} Solvers},
   booktitle = {Automated Deduction},
   editor    = {Nikolaj B{\o}rner and Viorica Sofronie-Stokkermans},
   series    = {Lecture Notes in Computer Science},
   publisher = {Springer},
   volume    = 6803,
   year      = 2011,
   pages     = {116--130},
}