BriefGPT.xyz
Apr, 2024
利用Isabelle教授高阶逻辑
Teaching Higher-Order Logic Using Isabelle
HTML
PDF
Simon Tobias Lund, Jørgen Villadsen
TL;DR
我们在Isabelle证明助手中对高阶逻辑进行了形式化处理，直接构建在Isabelle/Pure的基础框架上，旨在尽可能简洁易读，为对高阶逻辑和证明助手感兴趣但不想学习更复杂的Isabelle/HOL与较重自动化的人提供了良好的入门。通过展示我们的开发和方法，我们解释了一个样例证明，描述了高阶逻辑的公理和规则，并讨论了在课堂环境中教授这一主题的经验。
Abstract
We present a
formalization
of
higher-order logic
in the
isabelle proof assistant
, building directly on the foundational framework
→