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