Re: [isabelle] SMT integration to Isabelle/HOL



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
> 
> 
> 






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