论文标题
isabelle/hol作为教授逻辑的元语言
Isabelle/HOL as a Meta-Language for Teaching Logic
论文作者
论文摘要
证明助理是教授逻辑的重要工具。我们通过讨论在自动推理的最新课程中使用的三个形式化来支持这一主张。第一个是系统W的形式化（仅具有两个原始符号的经典命题逻辑系统），第二个是自然扣除助手（NADEA），第三个是单方面的序列微积分，它使用了我们的序列计算验证器（SECAV）。我们依次描述每个形式化，集中于我们如何在教学中使用它们，并评论从逻辑教育的角度来看有趣或有用的功能。总而言之，我们反思了所学到的教训以及它们可能带领我们接下来的地方。
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.
