学习如何证明：从 Coq 证明助手到教科书风格
计算机科学中的逻辑
2018-03-06 v1 系统与控制
摘要
我们开发了一种教授计算机科学学生如何证明的替代方法。首先，教学生使用 Coq 证明助手证明定理。在第二步（更困难）中，学生将把所获技能迁移到教科书证明领域。本文中我们给出第二步的一种实现。Coq 中的证明具有高度形式化，而教科书证明仅具中等形式化。因此我们的关键思想是将形式化程度上从 Coq 水平到教科书证明分若干小步降低。为此我们引入 Coq 与教科书证明之间的三种证明风格，称为逐行注释、弱化的逐行注释，以及结构忠实证明。尽管本文多为概念性内容，我们也报告了将我们的方法投入实践的体验。
引用
@article{arxiv.1803.01466,
title = {Learning how to Prove: From the Coq Proof Assistant to Textbook Style},
author = {Sebastian Böhne and Christoph Kreitz},
journal= {arXiv preprint arXiv:1803.01466},
year = {2018}
}
备注
In Proceedings ThEdu'17, arXiv:1803.00722