利用自动定理证明器进行数学教学中的错误诊断
人工智能
2020-02-13 v1 逻辑
摘要
Diproche系统是一个针对自然语言证明的自动证明检查器，专门适配于类似于Koepke、Schröder、Cramer等人的Naproche系统的初学者练习情境，它使用一种自动定理证明器的变体，该变体使用常见的形式谬误而非可靠的演绎规则来进行错误诊断。我们简要描述这种“反ATP（Anti-ATP）”的概念并解释其实现中使用的基本技术。
引用
@article{arxiv.2002.05083,
title = {Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics},
author = {Merlin Carl},
journal= {arXiv preprint arXiv:2002.05083},
year = {2020}
}