[isabelle-dev] FYI: Isabelle at CASC

Tobias Nipkow nipkow at in.tum.de
Thu Mar 17 22:00:31 CET 2011

Just in case you are still wonderig which Hammer Jasmin has in mind:


We are currently preparing a new film release, "The Proof of Dracula", 
and I expect you can guess which ATP will play the lead.


Am 17/03/2011 20:50, schrieb Jasmin Blanchette:
> Hi all,
> The secret is out. There will be a first-order ISA category at the CASC (CADE ATP System Competition) in Breslau in August, with a generous prize thanks to Tobias:
> http://www.cs.miami.edu/~tptp/CASC/23/
> Details on the ISA category (a division of LTB, Large Theories presented in Batches) are here:
> http://www.cs.miami.edu/~tptp/CASC/23/Design.html
> The ISA problems were generated using Sledgehammer and contain between 100 and 5000 axioms (!). The hope is that all the ATP developers who tweak their ATPs for CASC will now be biased in favour of our favourite Hammer, by which I don't mean M.C. Hammer.
> Jasmin
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list