Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.

Lawrence C. Paulson, Jasmin Christian Blanchette

Browse the full LPAR paper archive.