[isabelle-dev] [Fwd: Isabelle, refute and nitpick]

[Amine Chaieb]

Second best??? But who is roaring ahead?


Amine.

Tobias Nipkow wrote:

> :-)
>
> Tobias
>
> -------- Original-Nachricht --------
> Betreff: Isabelle, refute and nitpick
> Datum: Tue, 3 Mar 2009 02:32:44 -0500 (EST)
> Von: geoff at cs.miami.edu
> Antwort an: geoff at cs.miami.edu
> An: Tobias Nipkow <Tobias.Nipkow at informatik.tu-muenchen.de>,  Jasmin
> Blanchette <jasmin.blanchette at gmail.com>
>
> Hi Tobias, Jasmin,
>
> Just a short note to let you know that the automatic Isabelle-refute system
> has been very useful in the TPTP world. It has found countermodels that
> have
> revealed several bugs in problem encodings, and also pointed to deeper
> theoretical issues in Chris Benzmuller's encoding of modal logic into
> higher-order logic. I'm looking forward to Isabelle 2009, so we can create
> a version of the system with strategy scheduling of refute and nitpick.
>
> Cheers,
>
> Geoff
>
> P.S. Soon I'll be send you all the results of our testing of Isabelle on
> the new higher-order TPTP. It looks like it's the second best system! I
> hope you will enter it into the new THF division of CASC at CADE-22.
>
> Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
> Department of Computer Science            Email : geoff at cs.miami.edu
> University of Miami                       Phone : +1 305 2842158/2842268
> (Director of Undergraduate Studies)       FAX   : +1 305 2842264
> ----- "My cat" is not a float. Every string should learn to swim. ------
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>