[isabelle] SMT integration to Isabelle/HOL



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.