[Club2] Dry run -- Indonesia

[Jasmin Christian Blanchette]

Hi all,

I will be holding three talks at LPAR/IWIL in Indonesia in October and will rehearse these here. Two of the three talks have significant overlap with previous talks which most of you have seen, so these are highly optional.

---

Wed Sept. 22, 14:00, Zuse (01.11.018)
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
(with Koen Claessen; LPAR)

Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.

---

Wed Sept. 29, 14:00, Turing (00.09.055)
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod
(System Description; LPAR)

Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. 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. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.

---

Wed Sept. 29, 14:00, Turing (00.09.055)
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
(with Larry Paulson; IWIL)

Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.

---

Jasmin