Re: [isabelle] SMT integration to Isabelle/HOL
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.lix.polytechnique.fr/~keller/Recherche/smtcoq.html> for an
integration of such an output in Coq.
This archive was generated by a fusion of
Pipermail (Mailman edition) and