[Club2] Sledgehammer and Nitpick: Proofs and Refutations for Isabelle/HOL

[Jasmin Christian Blanchette]

Hi all,

I will be holding a talk about Sledgehammer and Nitpick on January 6 at NICTA (an island of work in a sea of vacation). I will rehease on Wednesday morning from 10:30 to 11:15 in Turing. This talk is mostly a rehash of talks you've seen several times already, but it would be nice if one or two of you could come (in addition to Dongchen) to give feedback.


Sledgehammer and Nitpick: Proofs and Refutations for Isabelle/HOL

In this talk, I will present two subsystems of Isabelle/HOL that find proofs and counterexamples via a translation to first-order logic, sketching how they work under the hood and giving hints on how to get the most out of them.

Sledgehammer 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 reconstructs the proof in Isabelle. We recently extended Sledgehammer to invoke SMT (satisfiability modulo theories) solvers as well.

Nitpick is a counterexample generator that builds on Kodkod, a SAT-based first-order relational model finder (and Alloy's backend). Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets.


Thanks!

Jasmin