Re: [isabelle] SMT integration to Isabelle/HOL



> 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
> 	https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
> 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:
>>> Hello,
>>>
>>>
>>>
>>> We are trying to integrate an SMT solver to Isabelle/HOL. It seems that
>>> the
>>> integration of external procedures is done by defining oracles in
>>> Isabelle.
>>> I see that the new release of Isabelle supports SMT solvers like Z3,
>>> CVC,
>>> Yices. I would like to know that, if we implement the SMT solver in the
>>> same
>>> language as Z3, and also the same input standard, can we avoid defining
>>> the
>>> oracle and apply the existing oracle for Z3 directly?
>> You can share Isabelle's Z3 oracle if your input language is the same as
>> Z3.
>> 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
>> outputs
>> proofs in the Z3 format, Isabelle could check them, too.
>>
>> Tobias
> 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.
> Yours,
> Thomas.
>
>
>
> End of Cl-isabelle-users Digest, Vol 82, Issue 20
> *************************************************
>







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.