Automatized Evaluation of Formalization Exercises in Mathematics
This addresses the challenge of teaching formal logic skills to students in mathematics, but it is incremental as it builds on existing educational tools with automated feedback.
The paper tackles the problem of helping beginner students learn first-order predicate logic by introducing two systems: 'math dictations' for formalizing natural-language sentences and 'Game of Def' for describing geometric patterns, both with automatic checking.
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.