Re: [isabelle] Sledgehammer: veriT in Isabelle 2019



Dear Randy,

You wrote:

> 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.

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





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