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

[Amine Chaieb]

As long as it is not Coq this looks great. An I am sure with Jasmin's
and Sascha's  new ideas and approaches "second best" won't last very long :)


Amine.


Tobias Nipkow wrote:

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