Four Geometry Problems to Introduce Automated Deduction in Secondary Schools

Pedro Quaresma
(CISUC / Department of Mathematics, University of Coimbra, Portugal)
Vanda Santos
(CIDTFF / University of Aveiro and CISUC, Portugal)

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.

In João Marcos, Walther Neuper and Pedro Quaresma: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (ThEdu'21), (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021, Electronic Proceedings in Theoretical Computer Science 354, pp. 27–42.
Published: 8th February 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: