[isabelle-dev] smt2

[Jasmin Christian Blanchette]

Hi all,

As you may know, Sascha and I have been working on a new version of the "smt" proof method, called "smt2". It is effectively a clone of "smt", but with the Z3 interaction (problem generation, proof parsing, and reconstruction) rewritten from scratch, with the following short-term goals:

1. Use SMT-LIB 2 instead of 1.
2. Support newer versions of Z3 (> 4.0).
3. Produce Isar proofs from Z3 proofs.

It is still highly experimental, but our aim is to have "smt2" be in place before the next release (Isabelle2014). After the release, we would then move the old "smt" to "HOL/Library", rename it "legacy_smt", and rename "smt2" to "smt".

So far the development has taken place in a private repository. I will move it to Isabelle next week (in "src/HOL/Tools/SMT2", in session "HOL-SMT2"). To be able to connect it with Sledgehammer's Isar proof generator, the best would be to make it part of the "HOL" session, but that's for a bit later.

Cheers,

Jasmin