Teaching Higher-Order Logic Using Isabelle

简介

我们在Isabelle证明助手中提出了一个高阶逻辑的正式化，直接构建在基础框架Isabelle/Pure之上，并且尽可能小而易读。因此，它应该为那些想要学习高阶逻辑和证明助手的人提供一个良好的介绍，而不必学习更复杂、自动化程度更高的Isabelle/HOL。为了展示我们的开发和方法，我们解释了一个样例证明，描述了我们的高阶逻辑的公理和规则，并讨论了我们在课堂环境中教授该主题的经验。
作者讲解

目前尚无作者解读视频，你可点击下方【许愿开讲】按钮，许愿作者开讲~
图表
解决问题

解决问题：论文旨在介绍如何在Isabelle证明助手中形式化高阶逻辑，并探讨在教学中的应用。
关键思路

关键思路：论文基于Isabelle/Pure框架，直接构建高阶逻辑形式化，简洁易读。这种方法可作为学习高阶逻辑和证明助手的入门教材，相比使用更多自动化的Isabelle/HOL更易于理解。
其它亮点

其他亮点：论文通过一个样例证明展示了其方法的可行性，介绍了高阶逻辑的公理和规则，并讨论了在课堂教学中的应用情况。实验设计简单，未使用数据集或开源代码。
相关研究

相关研究：最近在该领域的相关研究包括：《Higher-Order Logic and Interactive Theorem Proving》、《The Isabelle/HOL Proof Assistant for Higher-Order Logic》等。