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