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

[Lawrence Paulson]

This sounds terrific. With smt at the moment being essentially forbidden anywhere in the distribution, an SMT result from sledgehammer only means “yes it is a theorem”, and having to replace a single smt line by something 10 times as long is always painful.

Larry

> On 19 Oct 2020, at 17:25, Jasmin Blanchette <j.c.blanchette at vu.nl> wrote:
> 
> 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
> 
> 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.
>