[isabelle] Isabelle winner in the CASC HO division!
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Isabelle winner in the CASC HO division!
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Thu, 28 Jun 2012 22:33:34 +0200
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:13.0) Gecko/20120614 Thunderbird/13.0.1
It is a pleasure to pass on this piece of news from the CASC (CADE ATP System
Competition) that took place at IJCAR in Manchester today:
Jasmin Blanchette's two Isabelle-based entries in the category of automated
higher-order provers came in first and second:
This is Jasmin's short description of his two entries:
Two versions of Isabelle participate in CASC, where they compete against the
automatic provers LEO-II, Satallax, and TPS. One is simply called "Isabelle" and
includes "simp", "blast", "auto", "fast", "best", "force", "fastforce", "meson",
"smt" (with CVC3 and Z3), Sledgehammer (with E, SPASS, Vampire, and Z3), and
Nitpick (for exhaustively checking finite problems) -- the last three tools are
invoked without proof reconstruction. The second Isabelle version,
"Isabelle-HOT", is for demonstration only (i.e. it cannot get us a trophy): It
includes LEO-II and Satallax as Sledgehammer backends.
This archive was generated by a fusion of
Pipermail (Mailman edition) and