[isabelle-dev] Nitpick counterexample generator now available

[Tobias Nipkow]

lemma "k dvd n ==> k dvd (n+1::nat)"
nitpick

But even with SAT4J I get

Nitpicking~

Nitpick found no counterexample.

Of course this is not ideal nitpick country, but still...

Tobias

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
> datatypes.
> 
> You can download Nitpick from
> 
> http://www4.in.tum.de/~blanchet/nitpick-1.0.0.tgz
> 
> 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
> 
> http://www4.in.tum.de/~blanchet/nitpick-1.0.0/Nitpick/Manual/nitpick.pdf
> 
> 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.
> 
> Thanks,
> 
> Jasmin
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev