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 >
