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

[Jasmin Blanchette]

> On 20 Oct 2020, at 12:47, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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.

Let me clarify. veriT is still, just like Z3, an external tool. Whether proofs reconstructed using veriT (via the syntax "by (smt (verit) ...)") should be allowed in the distribution or not, and similarly in the AFP, is a political decision I cannot make. veriT has a much smaller and more stable code base and is developed by close colleagues in Liège and Nancy, but we might still prefer not to rely on it for the distribution. Or we might say that the presence of two solvers with the same input format (Z3 and veriT) confers a certain robustness, although this is not entirely true regarding quantifier instantiation.

On the positive side, veriT outputs detailed proofs (like Z3 but unlike CVC4), which are parsed by Isabelle and yield these "semi-intelligible Isar monsters". Some users find that they can fish out useful bits from them, if not use them as is; others find them too broken or ugly. Improving the situation here is high on my agenda for Sledgehammer, because it's generally the key to proof reconstruction for stronger ATPs (e.g. HO).

Finally, there has been a lot of work by the CVC4 developers lately on proof production. They conveniently adopted the veriT file format, which means we might have Isar proofs for them soon (finally), and perhaps even an integration in the smt method ("by (smt (cvc4) ...)").

We'll try to remember to update the NEWS as we go. For the next release, just having properly tested up-to-date binaries of the latest and greatest ATPs would be a nice target.

Jasmin