Four Geometry Problems to Introduce Automated Deduction in Secondary Schools

TL;DR

This paper explores how automated deduction systems can be integrated into secondary school geometry education by analyzing four representative problems and proposing lesson plans utilizing ICT tools, despite existing challenges.

Contribution

It demonstrates that introducing automated deduction in secondary schools is feasible through specific problems and tailored lesson plans, overcoming curriculum and knowledge barriers.

Findings

Automated deduction can be applied to secondary school geometry problems.

Four representative problems illustrate the approach's potential.

Lesson plans incorporating ICT tools facilitate teaching automated deduction.

Abstract

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.