我正在为 Isabelle2013/HOL 寻找免费且高质量的教程和文档（除了在谷歌搜索和挖掘之后显而易见的教程和文档）。你能推荐一些吗？
问问题
679 次
1 回答
6
一些可以帮助您入门的文档：
之前的实际教程是Nipkow、Paulson 和 Wenzel的 A Proof Assistant for Higher-Order Logic。本文档介绍了 Isabelle/HOL 作为一种函数式编程语言，以及如何使用 Isabelle/HOL 中可用的大多数常见证明机制的指南。这是一个很好的起点；
一个较新的教程是Nipkow在 Isabelle/HOL 中的编程和证明。它涵盖了与之前的文档相同的一些材料，并且没有那么深入，但使用了更现代的技术在 Isabelle/HOL 中进行证明。作为 Isabelle/HOL 的“快速入门”，它可能很有用。
Nipkow 和 Klein所著的免费书籍Concrete Semantics在对编程语言进行证明的背景下介绍了 Isabelle/HOL。如果您对 Isabelle/HOL 的兴趣与程序验证有关，那么这本书将是一个好的开始。
一般来说，大多数（但不是全部）好的参考指南都链接到Isabelle 文档页面本身。但是请注意，因为那里的一些文件已经很老了，而且不太可能不再相关（尽管这些文件已被标记为此类文件）。
网上也有大量的幻灯片和讲义，例如新南威尔士大学或爱丁堡大学，但这些可能更好地用作补充，因为它们通常缺乏讲座中提供的上下文和重要细节。
于 2013-11-12T00:02:22.820 回答