Re: [isabelle] SMT integration to Isabelle/HOL



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

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