论文标题
数学中形式练习的自动化评估
Automatized Evaluation of Formalization Exercises in Mathematics
论文作者
论文摘要
我们描述了两个系统，用于支持初学者在表达一阶谓词逻辑形式主义中表达陈述的基本技能。第一个称为“数学命令”，向用户介绍了对给定的自然语言句子形式化的任务，而第二个称为“ of def的游戏”的任务挑战用户对向他们显示的一组几何模式进行正式描述。在这两种情况下，都会进行自动检查。
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.
