[isabelle-dev] [Spam] NEWS: update of external provers

[Jasmin Blanchette]

Hi Larry,

> I was wanting to know exactly the same thing. In particular, will sledgehammer suggest it now? And does it give us a version of the smt method more robust than the existing one?

That's the goal, but for this to happen, a few small changes (as well as some testing) have to take place. Having the new binaries is the first step. We're (Martin, Mathias, and I) are well aware of the 15 Dec. deadline.

See also this paper draft for some empirical data:

	https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf <https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf>

The nice thing about veriT is that it has more complete instantiation techniques than Z3 -- in fact, more or less the same as implemented in CVC4. This should boost the reconstruction success rate of proofs founds by CVC4.

Jasmin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201019/deb94da5/attachment.htm>