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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
