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