将 smtlib2 模型转换为 COQ
我
有一个由 smtlib2 格式的工具生成的复杂模型。而且我发现很难用SMT slover来证明SMT问题。所以我想把这个模型翻译成COQ，并用不同的方式证明它。
有没有 COQ 库、插件、工具可以做到这一点？ 谢谢
All
I have a complicated model generated by tool in smtlib2 format. And I found it is hard to prove the SMT problem with SMT slover. So I want to translate this model to COQ and prove it in a different way.
Is there any COQ lib, plugin, tools can do this?
Thanks
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论