[isabelle] Isabelle winner in the CASC HO division!



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:

http://www.cs.miami.edu/~tptp/CASC/J6/RealTimeResults.html

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.

Congratulations Jasmin!
Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.