English

Automatized Evaluation of Formalization Exercises in Mathematics

Logic 2020-07-10 v2 Artificial Intelligence

Abstract

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.

Keywords

Cite

@article{arxiv.2006.01800,
  title  = {Automatized Evaluation of Formalization Exercises in Mathematics},
  author = {Merlin Carl},
  journal= {arXiv preprint arXiv:2006.01800},
  year   = {2020}
}
R2 v1 2026-06-23T16:00:10.099Z