[isabelle-dev] [Fwd: Isabelle, refute and nitpick]
nipkow at in.tum.de
Tue Mar 3 10:19:27 CET 2009
Not sure, possibly Leo II. No other ITP is in the competition.
Amine Chaieb schrieb:
> Second best??? But who is roaring ahead?
> Tobias Nipkow wrote:
>> -------- 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
>> 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.
>> 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
More information about the isabelle-dev