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

[Tobias Nipkow]

Not sure, possibly Leo II. No other ITP is in the competition.

Tobias

Amine Chaieb schrieb:
> 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
>>