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

[Tobias Nipkow]

Note that Isabelle is currently applied only to HO problems. Hence there
is no(?) competition in the refute category and not much competition in
the prove category. However, I agree that we can do much better still.

Tobias

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