[isabelle-dev] Nitpick counterexample generator now available
nipkow at in.tum.de
Fri Feb 27 10:40:49 CET 2009
lemma "k dvd n ==> k dvd (n+1::nat)"
But even with SAT4J I get
Nitpick found no counterexample.
Of course this is not ideal nitpick country, but still...
Jasmin Christian Blanchette schrieb:
> I am pleased to announce the first release of Nitpick, a Kodkod (Alloy)
> based counterexample generator for Isabelle/HOL on which I've been
> working since October. (The name Nitpick is shamelessly stolen from an
> obsolete MIT tool.) The tool is similar to Refute in principle but it
> scales better and produces more genuine counterexamples for inductive
> You can download Nitpick from
> It requires a recent snapshot of Isabelle2009. The package contains
> everything you need: Nitpick (.thy + SML), Kodkod (Java), and a SAT
> solver (Java). To install it, just type './build'. The manual is
> included in the package and is also available at
> The plan is to release Nitpick 1.1 to the wider public alongside the
> Isabelle2009 "winter" release, and then to incorporate it directly in
> Isabelle from then on.
> Please let me know if you have any feedback or bug reports concerning
> Nitpick, or if you find typos in the manual.
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev