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

[Lawrence Paulson]

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