isabelle - Isabelle/HOL 与 HOL-Z 和 ZETA
问题描述
我看过一些论文，描述了如何使用工具 HOL-Z 和 ZETA 将 Z 表示法与 Isabelle/HOL 一起使用。我找不到这些工具，它们曾经发布过吗？还有其他方法可以将 Isabelle 与 Z 表示法一起使用吗？
解决方案
如果您准备将 Isabelle/HOL 替换为HOL 定理证明器之一（它也采用 LCF 方法来实现稳健性），那么您应该考虑ProofPower，它也在 HOL 中嵌入了 Z 表示法。ProofPower-Z 多年来一直用于大型工业示例，特别是放电验证条件以显示 Ada 源代码的正确性。
推荐阅读
- c# - 如何强制 Resharper 考虑条件编译符号
- c# - 从方法 c# 返回数据
- azure - 在 VSTS/Azure DevOps 上构建时出现“npm run build”错误
- python - 用户输入未保存到库存列表中
- visual-studio-code - VSCode - 我可以更改截屏视频的字体/高度吗？
- c# - 尝试在 c# 中进行重新加载延迟但遇到错误
- python - 如何循环时间戳并创建df
- java - 与 Guava HashBiMap 和 synchronizedBiMap 同步
- javascript - 带传单的 Javascript 开关盒
- excel - Excel散点图中的动态序列数