Re: [isabelle] Sledgehammer: veriT in Isabelle 2019



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

> On 4 Oct 2019, at 14:18, Randy Pollack <rpollack at inf.ed.ac.uk> 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.
> 
> Thanks for any help,
> --Randy
> 





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