防水：学习数学证明写作的教育软件
摘要：为了帮助学生学习如何撰写数学证明，我们开发了名为Waterproof的教育软件。Waterproof基于Coq证明助手。学生在程序中键入他们的证明时，程序会检查每个证明步骤的逻辑正确性并提供额外的引导反馈。与Coq的证明相反，Waterproof中的证明与手写的证明类似：使用受控自然语言表示证明步骤，通过强制标记的方式使证明的结构明确，并使用不等式链来证明更大的估计。为了实现这一点，我们开发了Coq库coq-waterproof。该库使用Ltac2策略语言扩展了Coq的默认策略。本文中包含很多代码片段，以增加可用的Ltac2示例数量。Waterproof已经被用于辅助教授TU/e的分析1课程多年了。学生们也开始在他们的手写证明中使用Waterproof的受控表述方式；这些句子的明确表述有助于澄清他们论证的逻辑结构。
作者：Jelle Wemmenhove, Thijs Beurskens, Sean McCarren, Jan Moraal, David Tuin, Jim Portegies
论文ID：2211.13513
分类：History and Overview
分类简称：math.HO
提交时间：2022-11-28