[isabelle-dev] FYI: Isabelle at CASC

Jasmin Blanchette jasmin.blanchette at gmail.com
Thu Mar 17 20:50:58 CET 2011

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:


Details on the ISA category (a division of LTB, Large Theories presented in Batches) are here:


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.


More information about the isabelle-dev mailing list