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.
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and