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

[Tobias Nipkow]

:-)

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. ------