Re: [isabelle] SMT integration to Isabelle/HOL

Hello Shuling,

Le 17/04/2012 07:03, wangsl at a écrit :
> So we consider at first picking a unified input language and output
> language for it, like SMTLIB standard, and thus may save some effort
> when integrating it to Isabelle. But we will now consider this more
> carefully for the sake of later reconstruction proof in Isabelle.

I want to point to you that there is a proposal for a unified output
language for SMT solver that has been proved to be easy to integrate to
interactive theorem provers:
<>. See
<> for an
integration of such an output in Coq.


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