[isabelle-dev] FYI: Isabelle at CASC

[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