Re: [isabelle] SMT integration to Isabelle/HOL
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] SMT integration to Isabelle/HOL
- From: wangsl at ios.ac.cn
- Date: Tue, 17 Apr 2012 13:14:05 +0800 (CST)
- Importance: Normal
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: SquirrelMail/1.4.8-5.el5_4.10
> Send Cl-isabelle-users mailing list submissions to
> cl-isabelle-users at lists.cam.ac.uk
> To subscribe or unsubscribe via the World Wide Web, visit
> or, via email, send a message with subject or body 'help' to
> cl-isabelle-users-request at lists.cam.ac.uk
> You can reach the person managing the list at
> cl-isabelle-users-owner at lists.cam.ac.uk
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Cl-isabelle-users digest..."
> Today's Topics:
> 1. Re: SMT integration to Isabelle/HOL (Thomas Sewell)
> Message: 1
> Date: Tue, 17 Apr 2012 12:23:29 +1000
> From: Thomas Sewell <Thomas.Sewell at nicta.com.au>
> Subject: Re: [isabelle] SMT integration to Isabelle/HOL
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <4F8CD421.4090305 at nicta.com.au>
> Content-Type: text/plain; charset=GB2312
> On 16/04/12 22:00, Tobias Nipkow wrote:
>> Am 16/04/2012 05:54, schrieb Shuling Wang:
>>> We are trying to integrate an SMT solver to Isabelle/HOL. It seems that
>>> integration of external procedures is done by defining oracles in
>>> I see that the new release of Isabelle supports SMT solvers like Z3,
>>> Yices. I would like to know that, if we implement the SMT solver in the
>>> language as Z3, and also the same input standard, can we avoid defining
>>> oracle and apply the existing oracle for Z3 directly?
>> You can share Isabelle's Z3 oracle if your input language is the same as
>> Jasmin already pointed you to the relevant files.
>> The Z3 link can also reconstruct Z3 proofs in Isabelle (thanks to
>> Sascha), which
>> is the safest way to integrate extertnal tools. If your SMT solver
>> proofs in the Z3 format, Isabelle could check them, too.
> A word of warning: the Z3 link can reconstruct Z3 proofs, but Sascha had
> to do a lot of guesswork. Z3 breaks large proofs down into component
> steps, which is very helpful. Some of these steps are still very large,
> however, and all that is given is a name (such as "lemma" or "rewrite").
> Sascha guessed what Z3 had done and picked appropriate Isabelle tools,
> which might be totally inappropriate for your tool.
> In conclusion: Z3's proof output format is far from ideal. You might be
> able to come up with a much better one yourself. I can give you some
> hints at a later point. Also, the Z3 input language Sascha picked is
> just SMTLIB/SMTLIB2.
> I would recommend you start by reading some of Sascha's papers on his
> work. See http://www4.in.tum.de/~boehmes/ (especially "Fast LCF-style
> Proof Reconstruction for Z3").
Thank you for providing the references. Very helpful.
> End of Cl-isabelle-users Digest, Vol 82, Issue 20
This archive was generated by a fusion of
Pipermail (Mailman edition) and