Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics

2020/02/12 by Carl, Merlin
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2002.05083

Abstract

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.

Related

• Top-down Automated Theorem Proving (Notes for Sir Timothy)
• Automatic verification and interactive theorem proving
• Evidence Algorithm and System for Automated Deduction: A Retrospective View
• A Survey on Theorem Provers in Formal Methods
• Automatic Proof Checking and Proof Construction by Tactics