Email Gateway (Aug 18 2022 at 20:16): Email Gateway (Aug 18 2022 at 20:16):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Apr 18 2024 at 16:19 UTC