NICTA Embedded Systems Public Seminar

Sledgehammer and Nitpick: Proofs and Refutations for Isabelle/HOL

Jasmin Blanchette, PhD student in Tobias Nipkow's theorem proving group at TU Munich, Germany

Time/Venue

Thursday, 6 Jan 2011, 14:00

NICTA, Neville Roach Laboratory, Level 1 Seminar Room West, 223 Anzac Parade (Building L5), Kensington NSW 2052

Abstract

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.

Biography:

Jasmin Blanchette is a Ph.D. student in Tobias Nipkow's theorem proving group at TU Munich. He developed Nitpick and is Sledgehammer's maintainer. Prior to his involvement with theorem proving (and refuting), he worked as a C++ programmer and documentation manager for the Norwegian company Trolltech (now Nokia), makers of the Qt GUI framework.