数学形式化练习的自动化评价
Automatized Evaluation of Formalization Exercises in Mathematics
University of Konstanz（康斯坦茨大学）
摘要：
我们描述了两个系统，支持初学者的学生在获得基本技能，在表达语句的形式主义的一阶谓词逻辑;第一，称为“数学听写”，提出了用户的任务，正式一个给定的自然语言句子，而第二，称为“游戏的定义”，挑战用户给出一个正式的描述一组几何图案显示给他们。在这两种情况下，都会进行自动检查。
英文摘要：
We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math dictations", presents users with the task of formalizing a given natural-language sentence, while the second, called "Game of Def", challenges users to give a formal description of a set of a geometric pattern displayed to them. In both cases, an automatic checking takes place.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
