[isabelle-dev] FYI: Isabelle at CASC

[Tobias Nipkow]

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

http://www.amazon.co.uk/Ultimate-Hammer-Collection-Disc-Box/dp/B000HN31KQ

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

Tobias

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