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

[Tobias Nipkow]

We two are not going, as far as I can see. But I have already motivated
somebody...

Tobias

Lawrence Paulson schrieb:
> As Isabelle contains no specifically higher order theorem proving
> components, this is an amazing result. It would be great to see Isabelle
> entered at CASC. Are any of us going to CADE this year?
> Larry
> 
> On 3 Mar 2009, at 08:22, 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
>>