Email Gateway (Aug 22 2022 at 20:42): Email Gateway (Aug 22 2022 at 20:42):From: Randy Pollack <rpollack@inf.ed.ac.uk>
The Isabelle 2019 Sledgehammer document says:
If you installed an official Isabelle package, it should
already include
properly setup executables for CVC4, E, SPASS, Vampire, veriT, and Z3,
ready to use.
Indeed CVC4, E, SPASS, Vampire and Z3 work like a champ, but I can't
figure out verit:
"No such prover: verit" (also "No such prover: veriT"). I'm using a
download of the Isabelle2019 package on MacOs 10.14.6. Everything
else seems to work.
Thanks for any help,
--Randy
Email Gateway (Aug 22 2022 at 20:42):From: Lawrence Paulson <lp15@cam.ac.uk>
I downloaded and built veriT but couldn’t get it to prove the simplest theorem within sledgehammer. As I recall, the documentation says that sledgehammer was only tested on the 2014 version. I suspect it isn’t worth bothering with.
Larry
Email Gateway (Aug 22 2022 at 20:43):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Randy,
You wrote:
This is a mistake. I added veriT in the development version but it led to some errors, and so it was taken out of Isabelle before the release. I simply forgot to update the documentation.
Right now there's not much you can do with veriT. There has been some interesting work, by colleagues of mine (in CC:), notably on a tighter integration of veriT in the "smt" proof method. See
http://eptcs.web.cse.unsw.edu.au/paper.cgi?PxTP2019.6.pdf
Unfortunately we haven't yet build an Isabelle component based on the modern version of veriT. This requires compiling binaries on three platforms, which is a bit tedious, and I've lost my Windows installation in an upgrade... My goal for 2020 is to get the binaries back on track and update most of the Sledgehammer components (and include new ones, e.g. Leo-III).
Cheers,
Jasmin
Last updated: Apr 25 2024 at 04:18 UTC