# Four Geometry Problems to Introduce Automated Deduction in Secondary Schools

arXiv: https://arxiv.org/abs/2202.03566 · HTML: https://mlsanity.com/paper/2202.03566/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 32 references that are in the map.
- First posted on arXiv 8 Feb 2022.

## Builds on (most cited first, 2 of 2)

- [Improving QED-Tutrix by Automating the Generation of Proofs](https://mlsanity.com/paper/1803.01468/) (2018)
- [Towards Automated Discovery of Geometrical Theorems in GeoGebra](https://mlsanity.com/paper/2007.12447/) (2020)

## Built on by (most cited first, 1 of 1)

- [A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools](https://mlsanity.com/paper/2303.05863/) (2023)

## Abstract (arXiv)

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.