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