:-) 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. ------
