Re: [isabelle] SMT integration to Isabelle/HOL



Hello Shuling,

Le 17/04/2012 07:03, wangsl at ios.ac.cn 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:
<http://www.loria.fr/~fontaine/Besson1.pdf>. See
<http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html> for an
integration of such an output in Coq.

Cheers,
Chantal.





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