Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
This work addresses the problem of integrating automated deduction into secondary education for students and teachers, but it is incremental as it focuses on specific cases rather than a broad solution.
The paper tackles the challenge of introducing automated deduction in secondary schools by proposing a lesson plan using four geometry problems, demonstrating that the subject can be taught despite curriculum and teacher knowledge gaps.
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 about the subject and the difficulty of tackling the task by automatic means. Despite those difficulties we claim that the subject of automated deduction in geometry can be introduced, by addressing it in particular cases: simple to manipulate by students and teachers and reasonably easy to be dealt by automatic deduction tools. The subject is discussed by addressing four secondary schools geometry problems: their rigorous proofs, visual proofs, numeric proofs, algebraic formal proofs, synthetic formal proofs, or the lack of them. For these problems we discuss a lesson plan to address them with the help of Information and Communications Technology, more specifically, automated deduction tools.