> On 20 Oct 2020, at 12:47, Lawrence Paulson <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
