Elfe 系统——验证本科生的数学证明
计算机科学中的逻辑
2018-02-01 v1
摘要
Elfe 是一个用于离散数学基础证明方法教学的交互式系统。用户输入用浅白英语写成的数学文本，该文本被转换为一阶公式的特殊数据结构。由这一中间表示所隐含的某些证明义务由自动定理证明器检查，这些证明器试图证明这些义务，或在义务错误时找出反模型。验证过程的结果随后返回给用户。Elfe 用 Haskell 实现，可通过响应式 Web 界面或命令行访问。已开发关于集合、关系和函数的背景库。它已在数学学习初期的学生中进行了测试。
引用
@article{arxiv.1801.10513,
title = {The Elfe System - Verifying mathematical proofs of undergraduate students},
author = {Maximilian Doré and Krysia Broda},
journal= {arXiv preprint arXiv:1801.10513},
year = {2018}
}