我正在为Isabelle2013/HOL寻找免费提供的优质教程和文档(除了谷歌和挖掘之后的明显的教程和文档).你能推荐一下吗？
一些可能有助于您入门的文档:
之前的事实教程是Nipkow,Paulson和Wenzel 的高阶逻辑证明助手.本文档介绍了Isabelle/HOL作为函数式编程语言,以及如何使用Isabelle/HOL中可用的大多数常用证明机制的指南.这是一个很好的起点;
一个较新的教程是Nipkow 在Isabelle/HOL中的编程和证明.它涵盖了与前一个文档相同的一些材料,并不是那么深入,而是使用更现代的技术在Isabelle/HOL中进行校样.它可能是Isabelle/HOL的"快速启动".
Nipkow和Klein 免费提供的书籍Concrete Semantics在执行编程语言证明的背景下介绍了Isabelle/HOL.如果您对Isabelle/HOL的兴趣与程序验证有关,那么本书将是一个良好的开端.
一般情况下,大多数(但不是全部)良好的参考指南都与Isabelle文档页面本身相关联.但请注意,因为有些文件已经很老了,不太可能再相关了(虽然这些文件已被标记为这样).
网上还有大量的幻灯片和讲义,例如新南威尔士大学或爱丁堡大学,但这些可能更好地用作补充,因为它们往往缺乏讲座中提供的背景和重要细节.