Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
This addresses the challenge of providing automated feedback for novice learners in mathematics education, though it appears incremental as it builds on existing systems like Naproche.
The paper tackles the problem of diagnosing mistakes in beginner mathematics students' proofs by introducing the Diproche system, which uses an automated theorem prover modified to employ common formal fallacies instead of sound deduction rules, resulting in a tool adapted for educational exercises.
The Diproche system, an automated proof checker for natural language proofs specifically adapted to the context of exercises for beginner's students similar to the Naproche system by Koepke, Schröder, Cramer and others, uses a modification of an automated theorem prover which uses common formal fallacies intead of sound deduction rules for mistake diagnosis. We briefly describe the concept of such an `Anti-ATP' and explain the basic techniques used in its implementation.