伊莎贝尔2017 --入门
我正在试着学习使用Isabelle/HOL。我想，“嘿，由一些开发它的人写的教程会很棒”，所以看了看https://isabelle.in.tum.de/doc/tutorial.pdf，它的发布日期是2018年8月15日。然而，在尝试通过示例工作时，我在文本中发现了类似以下内容：
“经典的Isabelle用户界面是David Aspinall的Proof General / Emacs。这本书很少提到Proof General，它有自己的文档。”(第iii页)
如果发生任何奇怪的情况，我们建议您要求Isabelle通过Proof General菜单项Isabelle > Settings > Show Types显示所有类型信息(有关详细信息，请参阅第1.5节)。(第5页)
问题是，证明通用似乎不再与伊莎贝尔(见Isabelle2016 and Proof General)。我不明白为什么教程会基于过时的软件，但我真正的问题是：
“在Isabelle 2017中，有没有什么地方可以让我学会做最简单的事情呢？”
回答 1
Stack Overflow用户
发布于 2018-12-14 01:08:45
截至2018年，唯一支持Isabelle的IDE是Isabelle/jEdit，它包含在可以从Isabelle网站下载的发行版中。有一个实验性的VSCode插件正在积极开发中，但我建议暂时使用Isabelle/jEdit。
你找到的教程在网站上被列为“旧手册”之一。它在许多方面已经严重过时，不应该再使用了。发布日期可能没有意义，因为它是生成PDF的日期，而不是编写文本的日期。一些人游说将该教程从网站上完全删除，您的经验似乎证实了我们确实应该这样做。
开始学习伊莎贝尔的最好方法之一可能是‘Concrete Semantics’这本书(免费在线版本)。它的前半部分基本上是对Isabelle/HOL的介绍，并有很多练习。在Isabelle网站上还有‘Programming and Proving’教程，它几乎与“具体语义”的前半部分完全相同。
但是，它侧重于计算机科学中的应用(编程语言的语义和一些函数式编程)。我不确定是否有关于如何在Isabelle中做数学的好教程；无论如何，对于初学者来说，在定理证明器中数学往往更难做，因为与非正式论文推理的差距更大。因此，即使你最终对形式化数学感兴趣，我也推荐“具体语义学”。
顺便说一句:您提到了Isabelle2017，但实际上没有理由使用它来代替Isabelle2018，这是撰写本文时的最新版本。
https://stackoverflow.com/questions/53766579
复制相似问题
腾讯云开发者
