Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
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\"oder, 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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all theorem provers, especially the ones base…
Automated Theorem ProvingTowards Ranking Geometric Automated Theorem Provers
The field of geometric automated theorem provers has a long and rich history, from the early AI approaches of the 1960s, synthetic provers, to today algebraic and synthetic provers. The geometry automated deduction are…
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate a…
Automated Theorem ProvingMathematical ProofsMaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper describes the tool and the methods used in …
SchedulingA Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, how…
Automated Theorem ProvingDeep Reinforcement Learningreinforcement-learningReinforcement Learning+1