[isabelle-dev] Status of HOL/SMT
makarius at sketis.net
Tue Dec 4 15:36:07 CET 2012
On Tue, 4 Dec 2012, Jasmin Blanchette wrote:
> In general, we should try to reduce our exposure to SMT proofs in
> Isabelle (and keep it to 0 in the AFP). That "SMT_Examples" use them is
> fine, but any "smt" call that can be replaced by something else in other
> places, e.g. "Multivariate_Analysis", should be done in the long term.
> It's something where the Sledgehammer Isar proof generation framework
> should help at some point (e.g. in one year from now) -- once we're done
> with the ATP side we'll see what can be done with SMT proofs.
Multivariate_Analysis is a bit odd in many ways, not just spurious use of
smt. I usually see this as an opportunity for gradual clean-up, providing
good tools for that, which can be used in other situations as well.
For you it is better Sledgehammer/SMT support to inline better proof
For me it is something like plain-old auto-indentation and reformatting in
Isabelle/jEdit to get the theory sources into a sane state, where they can
be read and edited normally. Some weeks ago I've already fine-tuned my
buffer overview column to make it work smoothly with these unusually large
More information about the isabelle-dev