问Isabelle/HOL与HOL-Z和ZETA
EN

Stack Overflow用户

提问于 2021-11-01 16:03:05

回答 1查看 61关注 0票数 1

我看过一些文章，描述了如何使用工具HOL-Z和ZETA在Isabelle/HOL中使用Z符号。我找不到这些工具，它们曾经发布过吗？有没有其他方法可以将Isabelle与Z符号一起使用？

发布于 2021-11-07 16:08:24

如果您准备用Isabelle/HOL替换其中一个HOL theorem provers (它也采用低循环格式方法来保证可靠性)，那么您应该考虑ProofPower，它也在HOL中嵌入了Z符号。ProofPower-Z已用于大型工业实例多年，特别是用于放电验证条件，以显示Ada源代码的正确性。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/69799547

复制

相似问题

问Isabelle/HOL与HOL-Z和ZETAEN