Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be done by knowing, beforehand, the possible ways to solve a problem. Hence the need for an automated theorem prover that provide proofs as they would be written by a student. To achieve this objective, logic programming is a natural tool due to the similarity of its reasoning with a mathematical proof by inference. In this paper, we present the core ideas we used to implement such a prover, from its encoding in Prolog to the generation of the complete set of proofs. However, when dealing with educational aspects, there are many challenges to overcome. We also present the main issues we encountered, as well as the chosen solutions.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Improving QED-Tutrix by Automating the Generation of Proofs
The idea of assisting teachers with technological tools is not new. Mathematics in general, and geometry in particular, provide interesting challenges when developing educative softwares, both in the education and comput…
Automated Theorem ProvingFour Geometry Problems to Introduce Automated Deduction in Secondary Schools
The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject of rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers ab…
Interactive, Intelligent Tutoring for Auxiliary Constructions in Geometry Proofs
Geometry theorem proving forms a major and challenging component in the K-12 mathematics curriculum. A particular difficult task is to add auxiliary constructions (i.e, additional lines or points) to aid proof discovery.…
Automated Theorem ProvingA Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools
The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automate…
Retrieval-augmented Generation to Improve Math Question-Answering: Trade-offs Between Groundedness and Human Preference
For middle-school math students, interactive question-answering (QA) with tutors is an effective way to learn. The flexibility and emergent capabilities of generative large language models (LLMs) has led to a surge of in…
MathQuestion AnsweringRAGRetrieval+1