*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] SMT integration to Isabelle/HOL*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 16 Apr 2012 20:13:51 +0900*In-reply-to*: <002501cd1b84$9c19c520$d44d4f60$@ac.cn>*References*: <002501cd1b84$9c19c520$d44d4f60$@ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120329 Thunderbird/11.0.1

Just a remark: I'm pretty sure that Isabelle/HOL does not use oracles to integrate SMT solvers. The reason is that this would mean to base Isabelle/HOL's correctness on the correctness of external tools (which does not fit the usual "small trusted kernel" philosophy). The integration has to be roughly of the following shape: Isabelle asks an SMT solver to give a proof for some statement. The SMT solvers tries to do so, and if successful gives a certificate of some form. Isabelle reads back this certificate using a verified routine (i.e., logical inferences go through the trusted kernel) and if successful accepts the result. E.g., in the case of sledgehammer (which integrates first-order provers into Isabelle) the certification mechanism is to replay the found proof using a fully verified (i.e., "written in Isabelle") first-order prover. (I am a bit sloppy about the details, but I guess the general picture is correct.) cheers chris On 04/16/2012 12:54 PM, Shuling Wang wrote: > 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? > > > > I find that our use of Isabelle/HOL needs to go to the ML level, e.g., > defining tactics, and SMT integration mentioned above. But it is very > difficult for me to understand the ML implemental theories of Isabelle/HOL. > Can you please give me some directions to learn them, or any documents > especially about the oracle and tactics faculties of Isabelle? > > > > Looking forward to your reply. Thanks. > > > > Best, > > > > > > Wang Shuling > > Institute of Software > > Chinese Academy of Sciences > > > > > > Best, > > > > > > 王淑灵 Wang Shuling > > Institute of Software > > Chinese Academy of Sciences > > >

**Follow-Ups**:**Re: [isabelle] SMT integration to Isabelle/HOL***From:*Jasmin Blanchette

**References**:**[isabelle] SMT integration to Isabelle/HOL***From:*Shuling Wang

- Previous by Date: [isabelle] SMT integration to Isabelle/HOL
- Next by Date: Re: [isabelle] SMT integration to Isabelle/HOL
- Previous by Thread: [isabelle] SMT integration to Isabelle/HOL
- Next by Thread: Re: [isabelle] SMT integration to Isabelle/HOL
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list