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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
