【发布时间】：2021-11-08 00:08:24
【问题描述】：
我看到一些论文描述了如何使用工具 HOL-Z 和 ZETA 在 Isabelle/HOL 中使用 Z 表示法。我找不到这些工具，它们曾经发布过吗？还有其他方法可以将 Isabelle 与 Z 表示法一起使用吗？
【问题讨论】：
-
从未听说过这些。你能提供一篇论文的链接吗？可以直接联系论文作者吗？
标签： isabelle z-notation
【发布时间】：2021-11-08 00:08:24
【问题描述】：
如果您准备将 Isabelle/HOL 替换为 HOL theorem provers 之一（它也采用 LCF 方法来实现稳健性），那么您应该考虑 ProofPower，它还在 HOL 中嵌入了 Z 表示法。 ProofPower-Z 多年来一直用于大型工业示例，特别是排放验证条件以显示 Ada 源代码的正确性。
【讨论】：
-
我听说过 ProofPower 并对其进行了研究。它使用带有特殊字符的标记语言，但我更喜欢纯 ASCII 标记，最好完全基于 LaTeX。
-
无论您告诉 ProofPower 使用 UTF-8 还是它自己的定制字符编码，您始终可以使用 %...% 序列编写 ASCII 标记。这些与 LaTeX 序列有一些相似之处 - 映射可以在文件
/etc/sievekeyword 中找到。请注意，这些转义也可用于 ML 名称，这使得 PPML 与 SML 不同。就个人而言，我发现 Unicode 字符更具可读性。考虑 ⓩ∀ x : ℤ ⦁ 0 ≤ x⌝ 与 %SZT%%forall% x : %bbZ% %spot% 0 %leq% x%>%。 -
谢谢你的提示。我已经习惯了 \begin{szt}\forall x : \num @ 0 \leq x \end{szt}。也许我可以在调用 ProofPower 工具之前定义一些宏和预处理。